[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