Stream: Coq users

Topic: Building old Coq versions


view this post on Zulip Théo Zimmermann (Dec 30 2020 at 12:58):

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?

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 13:04):

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.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 13:44):

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.

view this post on Zulip Michael Soegtrop (Dec 30 2020 at 14:30):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 30 2020 at 16:34):

@Théo Zimmermann I'd say this is due to the camlp4 version being too modern?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 30 2020 at 16:34):

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.

view this post on Zulip Théo Zimmermann (Dec 30 2020 at 16:44):

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.

view this post on Zulip Paolo Giarrusso (Dec 31 2020 at 02:43):

do those compilers/toolchains pass the respective testsuites?

view this post on Zulip Paolo Giarrusso (Dec 31 2020 at 02:46):

what I learned from https://github.com/ocaml/opam/issues/4448 (and I'm sure there's tons more risks):

view this post on Zulip Paolo Giarrusso (Dec 31 2020 at 02:49):

view this post on Zulip Paolo Giarrusso (Dec 31 2020 at 02:51):

(but I'm not betting this is _the_ problem)

view this post on Zulip Michael Soegtrop (Dec 31 2020 at 09:25):

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.

view this post on Zulip Jason Gross (Jan 01 2021 at 02:45):

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.

view this post on Zulip Karl Palmskog (Jan 01 2021 at 13:41):

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

view this post on Zulip Paolo Giarrusso (Jan 01 2021 at 18:05):

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: Feb 04 2023 at 21:02 UTC