[isabelle-dev] NEWS: Isabelle/PIDE modules for Haskell
*** System *** * Session directory $ISABELLE_HOME/src/Tools/Haskell provides some source modules for Isabelle tools implemented in Haskell, notably for Isabelle/PIDE. This refers e.g. to current Isabelle/438e1a11445f. There is more and more material emerging: as direct ports from Isabelle/ML using the our canonical naming conventions and functional programming style. I writing these sources with VSCode and the extension "Haskell Language Server" 0.0.24, see also https://github.com/haskell/haskell-ide-engine After several days of tinkering it now works fairly well for me, even with friendly hints via hlint. Unfortunately I failed to reproduce the installation on my mobile machine. This reminds a bit of ancient times with vi and emacs, before Isabelle/PIDE/jEdit. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
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
Re: [isabelle-dev] NEWS: support for GHC
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