--- a/NEWS Mon Oct 08 12:52:28 2018 +0200
+++ b/NEWS Mon Oct 08 15:42:43 2018 +0200
@@ -25,7 +25,6 @@
(legacy feature since Isabelle2016).
-
*** HOL ***
* Simplified syntax setup for big operators under image. In rare
@@ -90,6 +89,12 @@
presence of structurally broken sources: full consolidation of theories
is no longer required.
+* Support for OCaml via command-line tools "isabelle ocaml_setup",
+"isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing
+settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained
+dynamically according the state of ISABELLE_OPAM_ROOT concerning
+ISABELLE_OCAML_VERSION.
+
New in Isabelle2018 (August 2018)
--- a/etc/settings Mon Oct 08 12:52:28 2018 +0200
+++ b/etc/settings Mon Oct 08 15:42:43 2018 +0200
@@ -138,6 +138,8 @@
ISABELLE_OPAM_ROOT="$ISABELLE_HOME_USER/opam"
+ISABELLE_OCAML_VERSION="4.05.0"
+
###
### Misc settings
@@ -147,7 +149,5 @@
#ISABELLE_GHC="/usr/bin/ghc"
#ISABELLE_MLTON="/usr/bin/mlton"
-#ISABELLE_OCAML="/usr/bin/ocaml"
-#ISABELLE_OCAMLC="/usr/bin/ocamlc"
#ISABELLE_SMLNJ="/usr/bin/sml"
#ISABELLE_SWIPL="/usr/bin/swipl"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml within the Isabelle environment
+
+isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_opam Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml Package Manager within the Isabelle environment
+
+isabelle_opam "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocaml_setup Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: OCaml setup via OPAM
+
+isabelle_opam init --no-setup --compiler="$ISABELLE_OCAML_VERSION" "$@"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/ocamlc Mon Oct 08 15:42:43 2018 +0200
@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: invoke OCaml compiler within the Isabelle environment
+
+isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
--- a/lib/scripts/getsettings Mon Oct 08 12:52:28 2018 +0200
+++ b/lib/scripts/getsettings Mon Oct 08 15:42:43 2018 +0200
@@ -99,6 +99,14 @@
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
fi
+#OCaml
+if [ -z "$ISABELLE_OCAML" -a -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
+ ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
+fi
+
#enforce JAVA_HOME
if [ -d "$ISABELLE_JDK_HOME/jre" ]
then