Following https://coq.discourse.group/t/fomalisation-of-bell-and-lapadula-model/1175, out of curiosity I tried building old Coq versions with the oldest OCaml compiler available in opam (3.07) but it failed for all the versions I tried (7.3, 7.4 and the HEAD of v8.0 and v8.1). I was especially surprised by the last failure since the required OCaml version is precisely 3.07 (3.06 for v8.0). Both v8.0 and v8.1 fail with:
OCAMLOPT lib/compat.ml4 File "lib/compat.ml4", line 52, characters 0-42: Unbound exception constructor Compat.Exc_located
7.4 fails with:
The implementation parsing/pcoq.ml4 does not match the interface parsing/pcoq.cmi: Modules do not match: ... The field `glexer' is required but not provided
And 7.3 fails with:
File "parsing/pcoq.mli", line 24, characters 6-22: The type constructor Gramext.g_symbol expects 1 argument(s), but is here applied to 0 argument(s)
For 7.3, I guess it's truly not comptible with OCaml 3.07 but for 7.4-8.1 it looks like a camlp4 issue... Any idea?
I actually just thought about providing Coq platform for older versions of Coq (well not that old) since I think it might simplify porting of older packages if older versions of Coq would be easy to install in a separate switch. I guess @Théo Zimmermann also thinks that this might make sense. What is the opinion of others? What are other strategies to reduce Coq related bit rot.
I'm not sure what you mean by "platform" in the case of old versions. Relatively recent versions of Coq (down to 8.3) are already relatively easy to install thanks to opam.
Well the Windows installer with a majority of the packages exists since 8.6. Building single opam packages is usually fine but building several dependent packages can be tricky because the dependencies in opam are not always accurate.
@Théo Zimmermann I'd say this is due to the camlp4 version being too modern?
If there is interest, we could always update these branches to build with modern OCaml's, that should be easier, at the last for the ml part.
Emilio Jesús Gallego Arias said:
Théo Zimmermann I'd say this is due to the camlp4 version being too modern?
Unfortunately, it happens even with the version of camlp4 that comes bundled with OCaml 3.07.
do those compilers/toolchains pass the respective testsuites?
what I learned from https://github.com/ocaml/opam/issues/4448 (and I'm sure there's tons more risks):
(but I'm not betting this is _the_ problem)
I think it might be possible to create switches which have their own gcc and make older ocamls depend on this. It might require some hacks - like first creating an empty switch without OCaml, then first add the conf-gcc package and then OCaml - but it might also work out of teh box.
According to http://old-releases.ubuntu.com/ubuntu/dists/warty/universe/binary-amd64/, the version of Coq on Ubuntu 4.10 (Warty Warthog) was 7.3, so you could try spinning up a VM or a chroot with Ubuntu 4.10 from http://old-releases.ubuntu.com/releases/warty/ and then access the old packages as in https://superuser.com/a/339572/59575 or perhaps https://askubuntu.com/a/1123049/223605. This should hopefully make it possible to see what version of ocaml, camlp4, etc, is needed for compilation.
it seems very likely that the problem is GCC and specifically the linker, which seems to be called by the OCaml compiler and camlp4 quite often
Despite my message, I’ll be amazed if GCC turns out to cause those errors, and I’d love to see the explanations! It’d be an amazing blog post (tho of course nobody has time for it)
Last updated: Sep 25 2023 at 12:01 UTC