[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Manuel Eberl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190314/5dc42a39/attachment-0002.html>