>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
