[isabelle-dev] NEWS: support for GHC

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