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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev