# HG changeset patch
# User wenzelm
# Date 1539806402 -7200
# Node ID 9d70340b565ca731b255cf4947dc9d921a68f064
# Parent  806be481aa574082aebf5ffa0870b28ab5dd478b# Parent  108beabc1bc6f777f71dee70e6714d870b46234f
merged

diff -r 806be481aa57 -r 9d70340b565c Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Oct 17 21:00:53 2018 +0200
+++ b/Admin/components/components.sha1	Wed Oct 17 22:00:02 2018 +0200
@@ -4,6 +4,7 @@
 97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
 9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
 a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
+f92cff635dfba5d4d77f469307369226c868542c  cakeml-2.0.tar.gz
 e7ffe4238b61a3c1ee87aca4421e7a612e09b836  ci-extras-1.tar.gz
 70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
@@ -189,6 +190,7 @@
 53123dc011b2d4b4e8fe307f3c9fa355718ad01a  postgresql-42.1.1.tar.gz
 3a5d31377ec07a5069957f5477a4848cfc89a594  postgresql-42.1.4.tar.gz
 e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40  postgresql-42.2.2.tar.gz
+231b33c9c3c27d47e3ba01b399103d70509e0731  postgresql-42.2.5.tar.gz
 f132329ca1045858ef456cc08b197c9eeea6881b  postgresql-9.4.1212.tar.gz
 8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
@@ -226,6 +228,7 @@
 27aeac6a91353d69f0438837798ac4ae6f9ff8c5  sqlite-jdbc-3.23.1.tar.gz
 8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
 2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
+fdc415284e031ee3eb2f65828cbc6945736fe995  stack-1.9.1.tar.gz
 1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
 601e08d048d8e50b0729429c8928b667d9b6bde9  sumatra_pdf-2.3.2.tar.gz
 14d46c2eb1a34821703da59d543433f581e91df3  sumatra_pdf-2.4.tar.gz
diff -r 806be481aa57 -r 9d70340b565c Admin/components/main
--- a/Admin/components/main	Wed Oct 17 21:00:53 2018 +0200
+++ b/Admin/components/main	Wed Oct 17 22:00:02 2018 +0200
@@ -16,9 +16,10 @@
 postgresql-42.2.5
 scala-2.12.7
 smbc-0.4.1
-ssh-java-20161009
 spass-3.8ds-1
 sqlite-jdbc-3.23.1
+ssh-java-20161009
+stack-1.9.1
 vampire-4.2.2
 xz-java-1.8
 z3-4.4.0pre-2
diff -r 806be481aa57 -r 9d70340b565c Admin/haskell/stack/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/haskell/stack/README	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,12 @@
+This is stack 1.9.1 -- the Haskell Tool Stack.
+
+See also https://www.haskellstack.org and executables from
+https://github.com/commercialhaskell/stack/releases as follows:
+
+  * x86_64-linux: stack-1.9.1-linux-x86_64-static.tar.gz
+  * x86_64-darwin: stack-1.9.1-osx-x86_64.tar.gz
+  * x86_64-windows: stack-1.9.1-windows-x86_64.tar.gz
+
+
+    Makarius
+    17-Oct-2018
diff -r 806be481aa57 -r 9d70340b565c Admin/haskell/stack/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/haskell/stack/settings	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_STACK="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/stack"
diff -r 806be481aa57 -r 9d70340b565c NEWS
--- a/NEWS	Wed Oct 17 21:00:53 2018 +0200
+++ b/NEWS	Wed Oct 17 22:00:02 2018 +0200
@@ -95,6 +95,11 @@
 dynamically according the state of ISABELLE_OPAM_ROOT concerning
 ISABELLE_OCAML_VERSION.
 
+* Support for Glasgow Haskell Compiler via command-line tools "isabelle
+ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
+Existing settings variable ISABELLE_GHC is maintained dynamically
+according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
+
 
 
 New in Isabelle2018 (August 2018)
diff -r 806be481aa57 -r 9d70340b565c etc/settings
--- a/etc/settings	Wed Oct 17 21:00:53 2018 +0200
+++ b/etc/settings	Wed Oct 17 22:00:02 2018 +0200
@@ -142,12 +142,22 @@
 
 
 ###
+### Haskell
+###
+
+ISABELLE_STACK_ROOT="$ISABELLE_HOME_USER/stack"
+
+ISABELLE_STACK_RESOLVER="lts-12.13"
+
+ISABELLE_GHC_VERSION="ghc-8.4.3"
+
+
+###
 ### Misc settings
 ###
 
 ISABELLE_GNUPLOT="gnuplot"
 
-#ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_MLTON="/usr/bin/mlton"
 #ISABELLE_SMLNJ="/usr/bin/sml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff -r 806be481aa57 -r 9d70340b565c lib/Tools/ghc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ghc	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke Glasgow Haskell Compiler within the Isabelle environment
+
+isabelle_stack ghc -- "$@"
diff -r 806be481aa57 -r 9d70340b565c lib/Tools/ghc_setup
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ghc_setup	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: setup Glasgow Haskell Compiler setup via Stack
+
+isabelle_stack setup --resolver "$ISABELLE_STACK_RESOLVER" &&
+  isabelle_stack ghci --ghci-options --version
diff -r 806be481aa57 -r 9d70340b565c lib/Tools/ghc_stack
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ghc_stack	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke Haskell Tool Stack within the Isabelle environment
+
+isabelle_stack "$@"
diff -r 806be481aa57 -r 9d70340b565c lib/Tools/ghci
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ghci	Wed Oct 17 22:00:02 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke GHC interaction within the Isabelle environment
+
+isabelle_stack ghci "$@"
diff -r 806be481aa57 -r 9d70340b565c lib/Tools/ocaml_setup
--- a/lib/Tools/ocaml_setup	Wed Oct 17 21:00:53 2018 +0200
+++ b/lib/Tools/ocaml_setup	Wed Oct 17 22:00:02 2018 +0200
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: OCaml setup via OPAM
+# DESCRIPTION: setup OCaml setup via OPAM
 
 if [ -d "$ISABELLE_OPAM_ROOT" ]
 then
diff -r 806be481aa57 -r 9d70340b565c lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Wed Oct 17 21:00:53 2018 +0200
+++ b/lib/scripts/getfunctions	Wed Oct 17 22:00:02 2018 +0200
@@ -37,6 +37,18 @@
 }
 export -f isabelle_opam
 
+#GHC management via Stack
+function isabelle_stack()
+{
+  if [ -z "$ISABELLE_STACK" ]; then
+    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
+    return 127
+  else
+    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"
+  fi
+}
+export -f isabelle_stack
+
 #robust invocation via ISABELLE_JDK_HOME
 function isabelle_jdk ()
 {
diff -r 806be481aa57 -r 9d70340b565c lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Oct 17 21:00:53 2018 +0200
+++ b/lib/scripts/getsettings	Wed Oct 17 22:00:02 2018 +0200
@@ -99,14 +99,23 @@
   ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
 fi
 
-#OCaml
-if [ -z "$ISABELLE_OCAML" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
+#enforce ISABELLE_OCAML
+if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
   ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml"
 fi
-if [ -z "$ISABELLE_OCAMLC" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
+
+#enforce ISABELLE_OCAMLC
+if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
   ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
 fi
 
+#enforce ISABELLE_GHC
+if [ -d "$ISABELLE_STACK_ROOT" ]; then
+  if [ -f "$(isabelle_stack path --programs)/$ISABELLE_GHC_VERSION/ghc" ]; then
+    ISABELLE_GHC="$ISABELLE_HOME/lib/Tools/ghc"
+  fi
+fi
+
 #enforce JAVA_HOME
 if [ -d "$ISABELLE_JDK_HOME/jre" ]
 then