Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

> 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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

On 13/03/2019 20:49, Florian Haftmann wrote: > Are there any issues remaining on this thread after > http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? I get this failure on my regular Ubuntu 18.04: *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Finite_Map")

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

> I get this failure on my regular Ubuntu 18.04: > > *** Failed to load theory "HOL-Library.Library" (unresolved > "HOL-Library.Finite_Map") > *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" > ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml > *** At command

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

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? Manuel On 14/03/2019

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

>> Are there any issues remaining on this thread after >> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? > > I get this failure on my regular Ubuntu 18.04: > > *** Failed to load theory "HOL-Library.Library" (unresolved > "HOL-Library.Finite_Map") > *** Code check failed for OCaml:

Re: [isabelle-dev] [Isabelle-ci] Build failure in Isabelle+AFP (slow)

I'm note sure what's going on here. It appears to be a spontaneous dropout of the OCaml environment, sporadically: in session Native_Word, theory ~~/afp/thys/Native_Word/Bits_Integer.thy seems to success, whereas in e.g. Iptables_Semantics it fails. I did not experience anything like that on

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

> 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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

On 14/03/2019 20:03, Lars Hupel wrote: > > It initially failed because the OCaml people rely on "m4", which > apparently is not installed by default on modern Ubuntu systems. None of these ancient build tools are available by default on any current OS: m4, make, etc. are all evil in some sense.

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

OK. This is running now in testboard: The corresponding changeset is . I have discarded my changeset now, because Florian has pushed an alternative solution. Here