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