Makarius wrote: > Nonetheless, it is still possible to use "isabelle ghc" without stack: > you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the > Isabelle settings mechanism to override ISABELLE_GHC with the > stack-based tools.
After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about a missing GHC setup, since there's no fallback on a custom $ISABELLE_GHC. I've added such a fallback in the attached patch, does that look reasonable? Cheers, Bertram
diff -r 0a9688695a1b lib/Tools/ghc --- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghc -- "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" "$@" else echo "Cannot execute ghc: missing Isabelle GHC setup" >&2 exit 127 diff -r 0a9688695a1b lib/Tools/ghci --- a/lib/Tools/ghci Thu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghci Thu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghci "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" --interactive "$@" else echo "Cannot execute ghci: missing Isabelle GHC setup" >&2 exit 127
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
