[isabelle-dev] NEWS: support for GHC

Bertram Felgenhauer bertram.felgenhauer at googlemail.com
Thu Nov 8 11:30:29 CET 2018


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
-------------- next part --------------
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


More information about the isabelle-dev mailing list