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 it

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

Here the current matter of affairs: * 0c0f7b4a72bf introduces a dedicated setting for regarding ocamlexec, hence there should be no invocations of it if no opam setup is present. * 036037573080 takes up the idea that zarith is already part of the initial opam bootstrap. Again, I was not able to

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 15:30, Manuel Eberl 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 the perspective Isabelle/ML, only the presence of settings like ISABELLE_OCAML or ISABELLE_GHC is decisiv

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

> 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

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 15

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 "expor

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] 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

Are there any issues remaining on this thread after http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? Cheers, Florian Am 24.06.18 um 22:29 schrieb Makarius: > On 07/06/18 15:22, Lars Hupel wrote: >>> Does this minimal approach make any sense, and solve the imminent >>> administr

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

On 07/06/18 15:22, Lars Hupel wrote: >> Does this minimal approach make any sense, and solve the imminent >> administrative problems? In particular without a decision yet about >> ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC? > > I tend to agree. Let's fix OCaml to 4.05.0 and we can

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

> Does this minimal approach make any sense, and solve the imminent > administrative problems? In particular without a decision yet about > ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC? I tend to agree. Let's fix OCaml to 4.05.0 and we can figure out a good way to upgrade after the

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

> So I would like to focus: > * What (upcoming) maintenance challenges are we facing? There are many applications in the AFP that link generated code to larger developments. For example, Julian Brunner recently updated the CAVA model checker because it is not tested systematically (e.g. nightly),

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

On 07/06/18 11:41, Florian Haftmann wrote: > > How significant is Isabelle as an integrative platform for OCaml? So far: insignificant. > So I would like to focus: > * What (upcoming) maintenance challenges are we facing? > * Are there particular applications out there which suggest more > inte

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

>>> So we could provide "isabelle opam" as wrapper for something like "opam >>> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle >>> opam_init" for the specific compiler version setup. Our component wiring >>> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for t

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

On 07/06/18 09:49, Lars Hupel wrote: >> So we could provide "isabelle opam" as wrapper for something like "opam >> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle >> opam_init" for the specific compiler version setup. Our component wiring >> would also provide ISABELLE_OCAML a

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

> So we could provide "isabelle opam" as wrapper for something like "opam > --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle > opam_init" for the specific compiler version setup. Our component wiring > would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the > res

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

> In practice "their" version means a version in distant past that was the > current one when the author was working on the session. The reason why I suggested it was to avoid one more burden on Isabelle developers: whoever updates the bundled OCaml version, must also adapt whatever arrangements d

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

On 06/06/18 11:39, Lars Hupel wrote: >> The opam executables only require a few MB. The result in >> ~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair >> investment to evade the "dynamic version hell", and normal Isabelle >> users won't have to see it. >> >> So we could provide

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

> I have now experimented a bit with opam-1.2.2 on Linux, Mac OS X, > Windows/Cygwin64. It appears to work quite well, e.g. like this: > > ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0 > > The opam executables only require a few MB. The result in > ~/.isabelle/opam above

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

On 30/05/18 11:15, Lars Hupel wrote: >> The best way maybe is to introduce a dedicated isabelle tool »ocamlc« >> which uses an environment parameter ISABELLE_OCAML as path prefix to >> ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc >> montage in ML. > > Yes, but we would s

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

> The best way maybe is to introduce a dedicated isabelle tool »ocamlc« > which uses an environment parameter ISABELLE_OCAML as path prefix to > ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc > montage in ML. Yes, but we would still need to figure out how to "peg" a partic

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

> No matter whether we decide to stick with Num or migrate to Zarith, the > code generator needs to be updated to not link against "nums.cma" directly: > > val compile_cmd = > "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^ > " -I " ^ File.bash_path path ^ > " nums.

[isabelle-dev] OCaml 4.06.0 drops nums.cma

I've been trying to figure out why some recent updates broke code checking (both in the distribution and the AFP) for OCaml. It turns out that the "nums.cma" module that we rely on for big integer arithmetic got removed from the standard library. This problem will affect anyone on rolling releases