Re: [isabelle-dev] NEWS: support for GHC
This is the updated situation according to Isabelle/c1a27fce2076: *** System *** * Support for managed installations of Glasgow Haskell Compiler and OCaml via the following command-line tools: isabelle ghc_setup isabelle ghc_stack isabelle ocaml_setup isabelle ocaml_opam The global installation state is determined by the following settings (and corresponding directory contents): ISABELLE_STACK_ROOT ISABELLE_STACK_RESOLVER ISABELLE_GHC_VERSION ISABELLE_OPAM_ROOT ISABELLE_OCAML_VERSION After setup, the following Isabelle settings are automatically redirected (overriding existing user settings): ISABELLE_GHC ISABELLE_OCAML ISABELLE_OCAMLC The old meaning of these settings as locally installed executables may be recovered by purging the directories ISABELLE_STACK_ROOT / ISABELLE_OPAM_ROOT. I have also started experimenting with the following in $ISABELLE_HOME_USER/etc/settings: ISABELLE_STACK_ROOT="$HOME/.stack" ISABELLE_OPAM_ROOT="$HOME/.opam" The Isabelle scripts should ensure that the specified versions are used, independently of other versions that a user might have installed already. In any case, both "stack" and "opam" stack-up considerable material: it is easy to fill 5-15 GB of disk space after working some time. Only docker requires even more space. 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: > On 08/11/2018 14:59, Bertram Felgenhauer wrote: > >> > >> I've misunderstood the problem. You intend to invoke old-style > >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > > > This may be premature, but I foresee that now that `isabelle ghc` > > and `isabelle ghci` exist, we will have scripts that use them. > > There is indeed some confusion here. > > My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained > by the odd recursive setup: in the stack situation, $ISABELLE_GHC points > to lib/Tools/ghc, and some mistake in the configuration could lead to > infinite recursion of sub-processes (potential bombing of the OS). > > It is probably better to leave the meaning of ISABELLE_GHC (and > ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle > ghc" tool entry points: these auxiliary scripts should go into > $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular > Isabelle tools. Sounds good to me. Cheers, Bertram ___ 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 08/11/2018 14:59, Bertram Felgenhauer wrote: >> >> I've misunderstood the problem. You intend to invoke old-style >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > This may be premature, but I foresee that now that `isabelle ghc` > and `isabelle ghci` exist, we will have scripts that use them. There is indeed some confusion here. My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained by the odd recursive setup: in the stack situation, $ISABELLE_GHC points to lib/Tools/ghc, and some mistake in the configuration could lead to infinite recursion of sub-processes (potential bombing of the OS). It is probably better to leave the meaning of ISABELLE_GHC (and ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle ghc" tool entry points: these auxiliary scripts should go into $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular Isabelle tools. I have now also learned that "ghci" is just "ghc --interactive", so there is no point to treat it too prominently. 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: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: > > Makarius wrote: > >> 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. > > > > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about > > a missing GHC setup, since there's no fallback on a custom > > $ISABELLE_GHC. I've added such a fallback in the attached patch, > > does that look reasonable? > > I've misunderstood the problem. You intend to invoke old-style > $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. This may be premature, but I foresee that now that `isabelle ghc` and `isabelle ghci` exist, we will have scripts that use them. > So just the usual question: What are remaining uses of this? Why not > uninstall the "system ghc" and only use stack? I don't think that the desire of using an existing ghc installation is unusual. I'm not sure how common maintaining a ghc installation without stack is these days, but ghc + cabal-install are still quite sufficient for Haskell development. I don't care much about disk space, but I do resent stack's propensity for downloading huge tarballs without even prompting; my bandwidth is often limited. So I try hard to avoid that particular tool. > My impression is that up-to-date Haskell projects are all using stack by > default. My desire is to be able to override the default, not to change it. Cheers, Bertram ___ 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 08/11/2018 12:16, Makarius wrote: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: >> Makarius wrote: >>> 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. >> >> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about >> a missing GHC setup, since there's no fallback on a custom >> $ISABELLE_GHC. I've added such a fallback in the attached patch, >> does that look reasonable? > > I've misunderstood the problem. You intend to invoke old-style > $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > So just the usual question: What are remaining uses of this? Why not > uninstall the "system ghc" and only use stack? It should be possible to > direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting > out remaining problems on that side. > > My impression is that up-to-date Haskell projects are all using stack by > default. A remaining use of "unmanaged" ghc is actually ocaml: I would like to keep these tools as uniform as possible, see also current a41f49148525. Unfortunately, OPAM is not as advanced as stack yet, e.g. it does not quite work on Windows so the Cygwin ocaml is still needed. We could move the other way and discontinue the meaning of $ISABELLE_GHC and $ISABELLE_OCAMLC as actual executables: the settings would merely indicate the presence of these tools, e.g. for options [condition = ISABELLE_GHC] in session ROOT entries. It probably would require some changes of the Codegen setup, because that wants to see a single environment variable instead of a command-line fragment like "isabelle ghc" or "isabelle ocamlc". 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 08/11/2018 11:30, Bertram Felgenhauer wrote: > Makarius wrote: >> 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. > > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about > a missing GHC setup, since there's no fallback on a custom > $ISABELLE_GHC. I've added such a fallback in the attached patch, > does that look reasonable? I've misunderstood the problem. You intend to invoke old-style $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. So just the usual question: What are remaining uses of this? Why not uninstall the "system ghc" and only use stack? It should be possible to direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting out remaining problems on that side. My impression is that up-to-date Haskell projects are all using stack by default. 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: > 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. After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about a missing GHC setup, since there's no fallback on a custom $ISABELLE_GHC. I've added such a fallback in the attached patch, does that look reasonable? Cheers, Bertram diff -r 0a9688695a1b lib/Tools/ghc --- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghc -- "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" "$@" else echo "Cannot execute ghc: missing Isabelle GHC setup" >&2 exit 127 diff -r 0a9688695a1b lib/Tools/ghci --- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghci "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" --interactive "$@" else echo "Cannot execute ghci: missing Isabelle GHC setup" >&2 exit 127 ___ 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
Re: [isabelle-dev] NEWS: support for GHC
On 22/10/2018 14:05, Lars Hupel wrote: The binary provided by Homebrew does not exhibit that problem. I have no other information beyond that. I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. Interestingly enough, I get Poly/ML warnings of the form: 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608) failed (error code=3) 14:11:19 *** error: can't allocate region 14:11:19 *** set a breakpoint in malloc_error_break to debug This is an Apple bug. It produces this message if it can't allocate memory in certain situations. That's a perfectly normal case and other operating systems just silently, and correctly, return zero from malloc. Poly/ML deals with that. Just ignore it. David ___ 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 22/10/2018 15:05, Lars Hupel wrote: > > I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. > > Interestingly enough, I get Poly/ML warnings of the form: > > 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608) > failed (error code=3) > 14:11:19 *** error: can't allocate region > 14:11:19 *** set a breakpoint in malloc_error_break to debug > > This happens during the build of "HOL-Decision_Procs", which succeeds > regardless: > > 14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu > time, factor 1.91) This is a normal feature of memory management on macOS. After all these years, David Matthews might eventually want to look if it is still required these days: for that he merely needs regular SSH access to some test machine. 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
> The binary provided by Homebrew does not exhibit that problem. I have no > other information beyond that. I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. Interestingly enough, I get Poly/ML warnings of the form: 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608) failed (error code=3) 14:11:19 *** error: can't allocate region 14:11:19 *** set a breakpoint in malloc_error_break to debug This happens during the build of "HOL-Decision_Procs", which succeeds regardless: 14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu time, factor 1.91) The timestamp suggests that this happens close to the end of the session; although no heap image has to be saved for that session. I'll run some more experiments to figure out if this is spurious or not. ___ 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
> Can you actually explain the problem and its solution? The problem appears to be that the official Stack binaries do not work consistently on El Capitan. The machine I've tried them on is fully updated and has no special software setup. The binary provided by Homebrew does not exhibit that problem. I have no other information beyond that. ___ 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 21/10/2018 17:34, Lars Hupel wrote: >> On an El Capitan system, this produces the following error: > > The problem can alternatively be solved by installing Homebrew's stack > version and declaring > > ISABELLE_STACK="/usr/local/bin/stack" > > in ~/.isabelle/etc/settings. Can you actually explain the problem and its solution? 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 an El Capitan system, this produces the following error: The problem can alternatively be solved by installing Homebrew's stack version and declaring ISABELLE_STACK="/usr/local/bin/stack" in ~/.isabelle/etc/settings. ___ 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
> * 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. Just a side remark: I have tried »isabelle ghc_setup« and »isabelle_ocaml_setup« and they work like a charm. Florian signature.asc Description: OpenPGP digital signature ___ 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 21/10/2018 13:25, Lars Hupel wrote: >> * 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. > > On an El Capitan system, this produces the following error: > > $ uname -a > Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29 > 20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64 > > $ ./bin/isabelle ghc_setup > /Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569 > Illegal instruction: 4 env STACK_ROOT="$(platform_path > "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@" Maybe there is something wrong with the hardware or the system installation. It works fine on all Macs that are part of the official isabelle-dev test infrastructure. See also Admin/PLATFORMS (Isabelle/c360f3b603f8): x86_64-darwin Mac OS X 10.10 Yosemite (macbroy31 MacBookPro6,2) Mac OS X 10.11 El Capitan (macbroy2 MacPro4,1) macOS 10.12 Sierra (macbroy30 MacBookPro6,2) macOS 10.13 High Sierra (!?) macOS 10.14 Mojave (!?) This also shows that 10.13 and 10.14 are presently not covered: there has been a general decline in Mac support in recent years. Isabelle on macOS presently hinges on a somewhat pathetic Mac Mini that I have at home. It would be great to recover some old vigor concerning isabelle-dev platform coverage: via regular OS installations with regular SSH access. Maybe even with nightly build_history measurements via isabelle_cronjob (not Jenkins). 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
> * 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. On an El Capitan system, this produces the following error: $ uname -a Darwin macisa1.in.tum.de 15.6.0 Darwin Kernel Version 15.6.0: Mon Aug 29 20:21:34 PDT 2016; root:xnu-3248.60.11~1/RELEASE_X86_64 x86_64 $ ./bin/isabelle ghc_setup /Users/hupel/workspace/isabelle/lib/scripts/getfunctions: line 1: 31569 Illegal instruction: 4 env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@" ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: support for GHC
*** 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. The Haskell "stack" looks much more solid than OPAM. It works on Windows without further ado, using native x86_64-windows personality. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
