[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

>> 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.

I would doubt that since ocamlexec is modelled following the existing
scripts ocamlc and ocaml; the only candidates for irregular activities
would be ocamlfind and ocamlopt themselves, which would be strange.

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

OK, this might at least explain the reproducible failure above.

Let's see what we get after the next iteration.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190314/5faff612/attachment.sig>