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