[isabelle-dev] NEWS: support for GHC

[Makarius]

On 07/11/2018 16:32, Bertram Felgenhauer wrote:
> 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.

The directory $ISABELLE_STACK_ROOT should be actually somewhat  bigger:
up to 5 GB for all the library modules. On Windows there is another
directory to take care of, according to "stack path programs".

I do prefer using up disk space and get a well-defined installation in
return. (I am presently working with someone building a Haskell-based
tool that is connected to Isabelle: the very first problem we had to
overcome was "cabal dependency hell". With stack it worked out nicely on
the spot, even on Windows and Mac OS X.)

Nonetheless, it is still possible to use "isabelle ghc" without stack:
you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
Isabelle settings mechanism to override ISABELLE_GHC with the
stack-based tools.


> 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...

This should be more robust in current Isabelle/8bfa615ddde4 (the
relevant change is c911716d29bb).

You need to run "isabelle ghc_setup" once again to ensure that the extra
file "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" is present --
otherwise it will fall back on old-style ISABELLE_GHC defaults despite
the presence of $ISABELLE_STACK_ROOT.


	Makarius