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