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 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 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 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-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,

[isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Makarius
Over the decades we have accumulated funny quotation forms in Isabelle syntax that are often hard to explain to new users (also to old users). In particular, what are the remaining uses of {* ... *}? It should already be superseded by cartouches. There is also "isabelle update_cartouches" to get

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] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Lawrence Paulson
> On 8 Nov 2018, at 20:32, Makarius wrote: > > In particular, what are the remaining uses of {* ... *}? I didn’t even know that existed. But I use (*...*) to enclose arbitrary text or comment material out. ___ isabelle-dev mailing list

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Peter Lammich
I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ... from my side there are no uses of this quotation remaining that I'd know ofHowever, (* *) is still very important for informally andquickly commenting things out, also in inner

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Gerwin.Klein
We probably still have a few occurrences of these, but no problem phasing them out. Cheers, Gerwin On 09.11.2018, at 10:03, Peter Lammich mailto:lamm...@in.tum.de>> wrote: I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ...

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. > >