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