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

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

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

> 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

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

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

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 >

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

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

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 >

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

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

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

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

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

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