[isabelle-dev] OCaml 4.06.0 drops nums.cma

Lars Hupel hupel at in.tum.de
Thu Mar 14 15:38:42 CET 2019


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

My understanding of the problem is as follows: Florian has thankfully
upgraded the code generator to emit code for OCaml 4.06+ with zarith.
However, it is still unclear how to install zarith systematically (i.e.
thread-safe but automatic).

For the error to be triggered I believe it is sufficient to have been
executed "isabelle opam_setup" once.

Cheers
Lars



More information about the isabelle-dev mailing list