--- 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
--- 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
--- /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
--- /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"
--- 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)
--- 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"
--- /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 -- "$@"
--- /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
--- /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 "$@"
--- /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 "$@"
--- 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
--- 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 ()
{
--- 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