[isabelle-dev] NEWS: support for GHC

Makarius makarius at sketis.net
Thu Nov 8 20:50:30 CET 2018


This is the updated situation according to Isabelle/c1a27fce2076:


*** System ***

* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:

  isabelle ghc_setup
  isabelle ghc_stack

  isabelle ocaml_setup
  isabelle ocaml_opam

The global installation state is determined by the following settings
(and corresponding directory contents):

  ISABELLE_STACK_ROOT
  ISABELLE_STACK_RESOLVER
  ISABELLE_GHC_VERSION

  ISABELLE_OPAM_ROOT
  ISABELLE_OCAML_VERSION

After setup, the following Isabelle settings are automatically
redirected (overriding existing user settings):

 ISABELLE_GHC

 ISABELLE_OCAML
 ISABELLE_OCAMLC

The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
ISABELLE_OPAM_ROOT.



I have also started experimenting with the following in
$ISABELLE_HOME_USER/etc/settings:

  ISABELLE_STACK_ROOT="$HOME/.stack"
  ISABELLE_OPAM_ROOT="$HOME/.opam"

The Isabelle scripts should ensure that the specified versions are used,
independently of other versions that a user might have installed already.

In any case, both "stack" and "opam" stack-up considerable material: it
is easy to fill 5-15 GB of disk space after working some time. Only
docker requires even more space.


	Makarius




More information about the isabelle-dev mailing list