[isabelle-dev] OCaml 4.06.0 drops nums.cma

Makarius makarius at sketis.net
Thu Mar 14 14:10:38 CET 2019

On 13/03/2019 20:49, Florian Haftmann wrote:
> Are there any issues remaining on this thread after
> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?

I get this failure on my regular Ubuntu 18.04:

*** Failed to load theory "HOL-Library.Library" (unresolved
*** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
*** At command "export_code" (line 1428 of

ocamlexec appears to reconfigure the OPAM installation insided
Isabelle/ML, but this is conceptually wrong as I explained already.

Also note that ISABELLE_OPAM_ROOT is always provided, even it that is
not active.

The general model is this:

  * Administrative tools like "isabelle ocaml_setup" or "isabelle
ghc_setup" provide a local installation with sufficient information in
the target directory, such that etc/settings can work out the resulting
underlying platform, without running any installation tools again.

  * The Isabelle/ML world only refers to these settings as consolidated
executables that don't change their own installation when invoked: many
invocations will run in parallel. Moreover this must not assume that it
is actually based on opam or stack: old-style manual installation of
ocaml/ocamlc or ghc is still allowed (we've had this discussion some
month ago concerning stack: it is just too heavy to be the only way to
refer to ghc).


More information about the isabelle-dev mailing list