--- a/NEWS Thu Mar 14 13:54:31 2019 +0000
+++ b/NEWS Thu Mar 14 19:06:40 2019 +0100
@@ -124,13 +124,11 @@
Minor INCOMPATIBILITY.
* Code generation for OCaml: Zarith superseedes Nums as library for
-integer arithmetic. Use the following incantation to obtain a suitable
-component setup:
+integer arithmetic. It is included in the default setup after
isabelle ocaml_setup
- isabelle ocaml_opam install zarith
-
-Minor INCOMPATIBILITY
+
+Minor INCOMPATIBILITY.
* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
--- a/lib/Tools/ocaml_setup Thu Mar 14 13:54:31 2019 +0000
+++ b/lib/Tools/ocaml_setup Thu Mar 14 19:06:40 2019 +0100
@@ -4,9 +4,13 @@
#
# DESCRIPTION: setup OCaml via OPAM
+set -e
+
if [ -d "$ISABELLE_OPAM_ROOT" ]
then
isabelle_opam switch "$ISABELLE_OCAML_VERSION"
else
isabelle_opam init --no-setup --compiler="$ISABELLE_OCAML_VERSION"
fi
+
+isabelle_opam install zarith