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
