[isabelle-dev] NEWS: support for GHC

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