[isabelle-dev] OCaml 4.06.0 drops nums.cma
makarius at sketis.net
Thu Mar 14 16:02:45 CET 2019
On 14/03/2019 15:38, Lars Hupel wrote:
>> 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).
Where "automatic" means that a single Isabelle administrator (e.g. the
local user) decides to invoke "isabelle ocaml_setup" and do other
Isabelle administration in parallel. Afterwards the ISABELLE_OCAML
settings will be correctly provided by the etc/settings scripts, without
any further automatisms that can fail in strange ways.
> For the error to be triggered I believe it is sufficient to have been
> executed "isabelle opam_setup" once.
This is not sufficient, and I have no time right now to look at the details.
For the moment I have merely disabled Isabelle OPAM and OCaml as follows
That is rather brutal, but allows me to continue with the current tip
More information about the isabelle-dev