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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
