I don't understand what is going on here. I thought I had to set ISABELLE_OCAML manually for this kind of code export to even do something. From what I can tell, I did /not/ set ISABELLE_OCAML on my machine, but I still get that error. Or did that behaviour change somehow?
Manuel On 14/03/2019 15:24, Lars Hupel wrote: >> 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") > Same error also on Jenkins. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
