[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

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
"HOL-Library.Finite_Map")
*** 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
"~~/src/HOL/Library/Finite_Map.thy")


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
ISABELLE_OCAML / ISABELLE_OCAMLC or ISABELLE_GHC settings for the
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).


	Makarius