Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
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

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
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. > >

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
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,

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
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

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
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

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
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.

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
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`

Re: [isabelle-dev] NEWS: support for GHC

2018-11-07 Thread 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

Re: [isabelle-dev] NEWS: support for GHC

2018-11-07 Thread Bertram Felgenhauer
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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-22 Thread David Matthews
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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-22 Thread Makarius
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 ***

Re: [isabelle-dev] NEWS: support for GHC

2018-10-22 Thread Lars Hupel
> 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: ***

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> 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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Makarius
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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> 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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Florian Haftmann
> * 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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Makarius
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

Re: [isabelle-dev] NEWS: support for GHC

2018-10-21 Thread Lars Hupel
> * 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