[isabelle-dev] NEWS: support for GHC
Bertram Felgenhauer
bertram.felgenhauer at googlemail.com
Wed Nov 7 16:32:58 CET 2018
Makarius wrote:
> *** System ***
>
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
>
>
> This refers to Isabelle/1722cc56d22e.
Is there a way to use a system ghc with `isabelle ghc` and
`isabelle ghci`? I want to avoid the 145MB download and extra
installation of ghc if possible.
Note in particular that setting ISABELLE_GHC now has a peculiar
effect on `isabelle ghc`. Without the environment variable, the
command complains:
Cannot execute ghc: missing Isabelle GHC setup
However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
then the same command starts downloading ghc via stack...
> isabelle ghc
Preparing to install GHC (tinfo6) to an isolated location.
This will not interfere with any system-level installation.
Preparing to download ghc-tinfo6-8.4.4 ...^C
Given the size of the download I find this unsatisfactory
(145 MB is still big for mobile plans.)
Cheers,
Bertram
More information about the isabelle-dev
mailing list