# HG changeset patch
# User wenzelm
# Date 1553109330 -3600
# Node ID 110fff287217a8200e90ac81476999c1ea98846d
# Parent  c90678ad942d3bef7732d9212a6bfc98d5c44122
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);

diff -r c90678ad942d -r 110fff287217 NEWS
--- 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.
 
diff -r c90678ad942d -r 110fff287217 lib/scripts/getsettings
--- 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
diff -r c90678ad942d -r 110fff287217 lib/scripts/ocamlc
--- 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
diff -r c90678ad942d -r 110fff287217 lib/scripts/ocamlexec
--- 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
diff -r c90678ad942d -r 110fff287217 lib/scripts/ocamlfind
--- /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
diff -r c90678ad942d -r 110fff287217 src/HOL/Library/code_test.ML
--- 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 *)
diff -r c90678ad942d -r 110fff287217 src/HOL/ROOT
--- 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
diff -r c90678ad942d -r 110fff287217 src/Tools/Code/code_ml.ML
--- 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))]))