access OCaml tools and libraries via ISABELLE_OCAMLFIND;
authorwenzelm
Wed Mar 20 20:15:30 2019 +0100 (4 weeks ago)
changeset 69926110fff287217
parent 69925 c90678ad942d
child 69927 f387618d9053
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);
NEWS
lib/scripts/getsettings
lib/scripts/ocamlc
lib/scripts/ocamlexec
lib/scripts/ocamlfind
src/HOL/Library/code_test.ML
src/HOL/ROOT
src/Tools/Code/code_ml.ML
     1.1 --- a/NEWS	Wed Mar 20 16:55:21 2019 +0100
     1.2 +++ b/NEWS	Wed Mar 20 20:15:30 2019 +0100
     1.3 @@ -127,12 +127,11 @@
     1.4  * Code generation for OCaml: proper strings are used for literals.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 -* Code generation for OCaml: Zarith superseedes Nums as library for
     1.8 -integer arithmetic.  It is included in the default setup after
     1.9 -
    1.10 -  isabelle ocaml_setup
    1.11 -
    1.12 -Minor INCOMPATIBILITY.
    1.13 +* Code generation for OCaml: Zarith supersedes Nums as library for
    1.14 +proper integer arithmetic. The library is located via standard
    1.15 +invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable).
    1.16 +The environment provided by "isabelle ocaml_setup" already contains this
    1.17 +tool and the required packages. Minor INCOMPATIBILITY.
    1.18  
    1.19  * Code generation for Haskell: code includes for Haskell must contain
    1.20  proper module frame, nothing is added magically any longer.
    1.21 @@ -284,6 +283,11 @@
    1.22  presence of structurally broken sources: full consolidation of theories
    1.23  is no longer required.
    1.24  
    1.25 +* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND,
    1.26 +which needs to point to a suitable version of "ocamlfind" (e.g. via
    1.27 +OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and
    1.28 +ISABELLE_OCAMLC are no longer supported.
    1.29 +
    1.30  * Support for managed installations of Glasgow Haskell Compiler and
    1.31  OCaml via the following command-line tools:
    1.32  
    1.33 @@ -308,12 +312,12 @@
    1.34  
    1.35    ISABELLE_GHC
    1.36  
    1.37 -  ISABELLE_OCAML
    1.38 -  ISABELLE_OCAMLC
    1.39 +  ISABELLE_OCAMLFIND
    1.40  
    1.41  The old meaning of these settings as locally installed executables may
    1.42  be recovered by purging the directories ISABELLE_STACK_ROOT /
    1.43 -ISABELLE_OPAM_ROOT.
    1.44 +ISABELLE_OPAM_ROOT, or by resetting these variables in
    1.45 +$ISABELLE_HOME_USER/etc/settings.
    1.46  
    1.47  * Update to Java 11: the latest long-term support version of OpenJDK.
    1.48  
     2.1 --- a/lib/scripts/getsettings	Wed Mar 20 16:55:21 2019 +0100
     2.2 +++ b/lib/scripts/getsettings	Wed Mar 20 20:15:30 2019 +0100
     2.3 @@ -99,19 +99,9 @@
     2.4    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
     2.5  fi
     2.6  
     2.7 -#enforce ISABELLE_OCAML
     2.8 -if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
     2.9 -  ISABELLE_OCAML="$ISABELLE_HOME/lib/scripts/ocaml"
    2.10 -fi
    2.11 -
    2.12 -#enforce ISABELLE_OCAMLC
    2.13 -if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
    2.14 -  ISABELLE_OCAMLC="$ISABELLE_HOME/lib/scripts/ocamlc"
    2.15 -fi
    2.16 -
    2.17 -#enforce ISABELLE_OCAMLEXEC
    2.18 +#enforce ISABELLE_OCAMLFIND
    2.19  if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then
    2.20 -  ISABELLE_OCAMLEXEC="$ISABELLE_HOME/lib/scripts/ocamlexec"
    2.21 +  ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind"
    2.22  fi
    2.23  
    2.24  #enforce ISABELLE_GHC
     3.1 --- a/lib/scripts/ocamlc	Wed Mar 20 16:55:21 2019 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,13 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Makarius
     3.7 -#
     3.8 -# Invoke ocamlc via "opam".
     3.9 -
    3.10 -if [ -e "$ISABELLE_OPAM_ROOT/config" ]
    3.11 -then
    3.12 -  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
    3.13 -else
    3.14 -  echo "Cannot execute ocamlc: missing Isabelle OCaml setup" >&2
    3.15 -  exit 127
    3.16 -fi
     4.1 --- a/lib/scripts/ocamlexec	Wed Mar 20 16:55:21 2019 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,13 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Makarius; Florian Haftmann
     4.7 -#
     4.8 -# Invoke command in OCaml environment setup by "opam".
     4.9 -
    4.10 -if [ -e "$ISABELLE_OPAM_ROOT/config" ]
    4.11 -then
    4.12 -  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- "$@"
    4.13 -else
    4.14 -  echo "Cannot execute: missing Isabelle OCaml setup" >&2
    4.15 -  exit 127
    4.16 -fi
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/lib/scripts/ocamlfind	Wed Mar 20 20:15:30 2019 +0100
     5.3 @@ -0,0 +1,13 @@
     5.4 +#!/usr/bin/env bash
     5.5 +#
     5.6 +# Author: Makarius; Florian Haftmann
     5.7 +#
     5.8 +# Invoke ocamlfind via "opam".
     5.9 +
    5.10 +if [ -e "$ISABELLE_OPAM_ROOT/config" ]
    5.11 +then
    5.12 +  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlfind "$@"
    5.13 +else
    5.14 +  echo "Cannot execute ocamlfind: missing Isabelle OCaml setup" >&2
    5.15 +  exit 127
    5.16 +fi
     6.1 --- a/src/HOL/Library/code_test.ML	Wed Mar 20 16:55:21 2019 +0100
     6.2 +++ b/src/HOL/Library/code_test.ML	Wed Mar 20 20:15:30 2019 +0100
     6.3 @@ -442,7 +442,7 @@
     6.4  (* driver for OCaml *)
     6.5  
     6.6  val ocamlN = "OCaml"
     6.7 -val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
     6.8 +val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
     6.9  
    6.10  fun mk_driver_ocaml _ path _ value_name =
    6.11    let
    6.12 @@ -467,7 +467,7 @@
    6.13  
    6.14      val compiled_path = Path.append path (Path.basic "test")
    6.15      val compile_cmd =
    6.16 -      "\"$ISABELLE_HOME/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
    6.17 +      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^
    6.18        " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
    6.19        File.bash_path code_path ^ " " ^ File.bash_path driver_path
    6.20  
    6.21 @@ -478,7 +478,7 @@
    6.22    end
    6.23  
    6.24  fun evaluate_in_ocaml ctxt =
    6.25 -  evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
    6.26 +  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLFIND, "ocamlfind executable")) ocamlN ctxt
    6.27  
    6.28  
    6.29  (* driver for GHC *)
     7.1 --- a/src/HOL/ROOT	Wed Mar 20 16:55:21 2019 +0100
     7.2 +++ b/src/HOL/ROOT	Wed Mar 20 20:15:30 2019 +0100
     7.3 @@ -276,7 +276,7 @@
     7.4      Code_Test_GHC
     7.5    theories [condition = ISABELLE_MLTON]
     7.6      Code_Test_MLton
     7.7 -  theories [condition = ISABELLE_OCAMLC]
     7.8 +  theories [condition = ISABELLE_OCAMLFIND]
     7.9      Code_Test_OCaml
    7.10    theories [condition = ISABELLE_SMLNJ]
    7.11      Code_Test_SMLNJ
     8.1 --- a/src/Tools/Code/code_ml.ML	Wed Mar 20 16:55:21 2019 +0100
     8.2 +++ b/src/Tools/Code/code_ml.ML	Wed Mar 20 20:15:30 2019 +0100
     8.3 @@ -889,7 +889,7 @@
     8.4          make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
     8.5            (*extension demanded by OCaml compiler*),
     8.6          make_command = fn _ =>
     8.7 -          "\"$ISABELLE_OCAMLEXEC\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
     8.8 +          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
     8.9        evaluation_args = []})
    8.10    #> Code_Target.set_printings (Type_Constructor ("fun",
    8.11      [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))