access OCaml tools and libraries via ISABELLE_OCAMLFIND;
OPAM setup is optional: it requires odd development tools that are not available in default OS installations (e.g. make, m4);
--- a/NEWS Wed Mar 20 16:55:21 2019 +0100
+++ b/NEWS Wed Mar 20 20:15:30 2019 +0100
@@ -127,12 +127,11 @@
* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.
-* Code generation for OCaml: Zarith superseedes Nums as library for
-integer arithmetic. It is included in the default setup after
-
- isabelle ocaml_setup
-
-Minor INCOMPATIBILITY.
+* Code generation for OCaml: Zarith supersedes Nums as library for
+proper integer arithmetic. The library is located via standard
+invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
+The environment provided by "isabelle ocaml_setup" already contains this
+tool and the required packages. Minor INCOMPATIBILITY.
* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
@@ -284,6 +283,11 @@
presence of structurally broken sources: full consolidation of theories
is no longer required.
+* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
+which needs to point to a suitable version of "ocamlfind" (e.g. via
+OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
+ISABELLE_OCAMLC are no longer supported.
+
* Support for managed installations of Glasgow Haskell Compiler and
OCaml via the following command-line tools:
@@ -308,12 +312,12 @@
ISABELLE_GHC
- ISABELLE_OCAML
- ISABELLE_OCAMLC
+ ISABELLE_OCAMLFIND
The old meaning of these settings as locally installed executables may
be recovered by purging the directories ISABELLE_STACK_ROOT /
-ISABELLE_OPAM_ROOT.
+ISABELLE_OPAM_ROOT, or by resetting these variables in
+$ISABELLE_HOME_USER/etc/settings.
* Update to Java 11: the latest long-term support version of OpenJDK.
--- a/lib/scripts/getsettings Wed Mar 20 16:55:21 2019 +0100
+++ b/lib/scripts/getsettings Wed Mar 20 20:15:30 2019 +0100
@@ -99,19 +99,9 @@
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
fi
-#enforce ISABELLE_OCAML
-if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
- ISABELLE_OCAML="$ISABELLE_HOME/lib/scripts/ocaml"
-fi
-
-#enforce ISABELLE_OCAMLC
-if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
- ISABELLE_OCAMLC="$ISABELLE_HOME/lib/scripts/ocamlc"
-fi
-
-#enforce ISABELLE_OCAMLEXEC
+#enforce ISABELLE_OCAMLFIND
if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then
- ISABELLE_OCAMLEXEC="$ISABELLE_HOME/lib/scripts/ocamlexec"
+ ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind"
fi
#enforce ISABELLE_GHC
--- a/lib/scripts/ocamlc Wed Mar 20 16:55:21 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Invoke ocamlc via "opam".
-
-if [ -e "$ISABELLE_OPAM_ROOT/config" ]
-then
- isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
-else
- echo "Cannot execute ocamlc: missing Isabelle OCaml setup" >&2
- exit 127
-fi
--- a/lib/scripts/ocamlexec Wed Mar 20 16:55:21 2019 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius; Florian Haftmann
-#
-# Invoke command in OCaml environment setup by "opam".
-
-if [ -e "$ISABELLE_OPAM_ROOT/config" ]
-then
- isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- "$@"
-else
- echo "Cannot execute: missing Isabelle OCaml setup" >&2
- exit 127
-fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/ocamlfind Wed Mar 20 20:15:30 2019 +0100
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius; Florian Haftmann
+#
+# Invoke ocamlfind via "opam".
+
+if [ -e "$ISABELLE_OPAM_ROOT/config" ]
+then
+ isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlfind "$@"
+else
+ echo "Cannot execute ocamlfind: missing Isabelle OCaml setup" >&2
+ exit 127
+fi
--- a/src/HOL/Library/code_test.ML Wed Mar 20 16:55:21 2019 +0100
+++ b/src/HOL/Library/code_test.ML Wed Mar 20 20:15:30 2019 +0100
@@ -442,7 +442,7 @@
(* driver for OCaml *)
val ocamlN = "OCaml"
-val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
+val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
fun mk_driver_ocaml _ path _ value_name =
let
@@ -467,7 +467,7 @@
val compiled_path = Path.append path (Path.basic "test")
val compile_cmd =
- "\"$ISABELLE_HOME/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
+ "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^
" -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
File.bash_path code_path ^ " " ^ File.bash_path driver_path
@@ -478,7 +478,7 @@
end
fun evaluate_in_ocaml ctxt =
- evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
+ evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt
(* driver for GHC *)
--- a/src/HOL/ROOT Wed Mar 20 16:55:21 2019 +0100
+++ b/src/HOL/ROOT Wed Mar 20 20:15:30 2019 +0100
@@ -276,7 +276,7 @@
Code_Test_GHC
theories [condition = ISABELLE_MLTON]
Code_Test_MLton
- theories [condition = ISABELLE_OCAMLC]
+ theories [condition = ISABELLE_OCAMLFIND]
Code_Test_OCaml
theories [condition = ISABELLE_SMLNJ]
Code_Test_SMLNJ
--- a/src/Tools/Code/code_ml.ML Wed Mar 20 16:55:21 2019 +0100
+++ b/src/Tools/Code/code_ml.ML Wed Mar 20 20:15:30 2019 +0100
@@ -889,7 +889,7 @@
make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
(*extension demanded by OCaml compiler*),
make_command = fn _ =>
- "\"$ISABELLE_OCAMLEXEC\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
+ "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))