[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

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
in $ISABELLE_HOME_USER/etc/settings:

  ISABELLE_OPAM_ROOT=""
  ISABELLE_OCAML=""
  ISABELLE_OCAMLC=""

That is rather brutal, but allows me to continue with the current tip
version.


	Makarius