Stream: Coq devs & plugin devs

Topic: OCaml variants in Docker-Coq


view this post on Zulip Enrico Tassi (Dec 09 2020 at 16:18):

now 4 different ocaml flavors for each coq version

I did not know that. But, I'm asking myself, do Coq users really care that much about ocaml variants? Why would a random Coq project want to test against 4 ocaml variants? Coq projects don't typically use ocaml directly, no?

view this post on Zulip Enrico Tassi (Dec 09 2020 at 16:21):

I mean, I think it is up to the CI of Coq to test that Coq and some plugins work with all supported ocaml versions. Users should ideally be hidden this complexity (exactly as they don't see which gcc is doing the linking of ocaml, just to make an example)

view this post on Zulip Jason Gross (Dec 09 2020 at 16:24):

Regarding variants of OCaml, I should probably start testing fiat-crypto with more variants of OCaml, given that we need to compile code generated by Coq's extraction, and the compilation hits performance bugs in newer versions of OCaml

view this post on Zulip Enrico Tassi (Dec 09 2020 at 16:27):

There are always specific needs. Here we are talking about the "standard" docker image people use by following the coq community tutorials.
If you need something specific, you can always build your own docker images, or CI scripts.

view this post on Zulip Karl Palmskog (Dec 09 2020 at 16:58):

@Enrico Tassi my experience is that Coq users at least care a lot more about OCaml than anything to do with native-compile or many other obscure features of Coq. The OCaml version is important in all projects using extraction and all plugin projects. For example, we had the coq-ffi project which for a while did not build with anything less than 4.10.0, for which there was no Docker image.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:10):

Hem, "ffi" does look quite tied to OCaml, maybe it is not the best example.
I believe math-comp or corn or unimath could not care less, I guess it is also the case for all "pure .v" projects.

If you really need to test 20 variants of ocaml why don't one puts the complexity on ocaml's docker? I mean, you can use 1 docker image to run Coq (and compile your extracted code on that ocaml if you like), and use other 20 docker images (from ocaml) to try the compilation of the extracted sources on all variants of ocaml.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:11):

Aren't there docker images for ocaml? (I don't know)

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:18):

Yes there are.

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:19):

Nobody is talking about testing 20 variants. You are stretching things quite a lot.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:26):

Sure. But if you turn a linear problem into a quadratic one "by coupling design" I'm sure the number of 20 images will be easily reached.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:31):

That is #images = 4-ocaml * 2-native * #Coq (and you can't really decouple coq and native).
Anyway, I'm not the one doing the docker images nor using native compute, so anything works for me.

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:33):

Ah, I had misunderstood. I thought you were talking about 20 variants of OCaml.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:34):

I was not clear, sorry. I hope it makes more sense now.

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:35):

We're indeed well past 20. Just have a look at the list here: https://hub.docker.com/r/coqorg/coq

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:35):

(Though some tags are synonyms.)

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:36):

It seems for coq master and 8.13+beta we have:

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:38):

fixed

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:38):

maybe latest=4.11 ?

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:38):

Yes.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:38):

Erik said 4

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:39):

fixing again

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:39):

The point of 4.05 is to be the oldest support version and the point of 4.11 is to be a moving target for the latest supported version.

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:40):

The point of 4.07 is that it has been quite recommended for Coq.

view this post on Zulip Théo Zimmermann (Dec 09 2020 at 17:41):

And the point of 4.10 was to respond to user demand (for coqffi) and to provide a relatively recent version of OCaml which would not be a moving target like latest.

view this post on Zulip Enrico Tassi (Dec 09 2020 at 17:50):

Ideally any Coq project should work with a version of Coq no matter which compiler we used to build Coq.
If you have an .ml part, then you should only use features supported by the version Coq declares as minimal.

If you want to test the output of extraction, this is very legitimate, it should be decorrelated to the ocaml version used to compile Coq.
I guess the extraction component should declare which versions of OCaml it targets, and that set should include (for simplicity) the compiler we use for Coq itself. But you don't need to compile Coq with OCaml X in order to test the extracted code on OCaml X, which seems to be the constraint enforced/granted by the current setup.

view this post on Zulip Karl Palmskog (Dec 09 2020 at 17:54):

4.05.0 is a terrible version to depend on. It has given us enormous grief in the opam archive.

view this post on Zulip Karl Palmskog (Dec 09 2020 at 17:57):

so personally, I find it unreasonable to say that we should all have our projects that include OCaml code build with 4.05.0

view this post on Zulip Enrico Tassi (Dec 09 2020 at 18:15):

This makes sense, the version of OCaml picked for compiling Coq should be one with no major problems. I think we use 4.07 in the platform because it seems to be a local optimum.

But maybe I misunderstand your comment. Are you suggesting to drop 4.05 from docker (as unusable anyway)?

view this post on Zulip Karl Palmskog (Dec 09 2020 at 18:30):

if it were up to me, I would drop 4.05.0 from everywhere

view this post on Zulip Erik Martin-Dorel (Dec 10 2020 at 00:46):

@Enrico Tassi

Enrico Tassi said:

maybe latest=4.11 ?

no: the coqorg/base:latest base image was the initial naming of the dual switches images (with 4.05.0 + 4.07.1+flambda) and these images will be removed one week after I'll have announced the migration on Discourse.

FYI I have already updated the wiki documentation to this aim:
see https://github.com/coq-community/docker-coq/wiki#supported-tags

and if that might "reassure" @Karl Palmskog, the plan is indeed to switch away from 4.05.0 as a default (but still keep 4.05.0 as an available switch − 4.05.0 or a more recent version of OCaml of course, if Coq bumps this minimal supported version of OCaml anytime soon!)

view this post on Zulip Théo Zimmermann (Dec 10 2020 at 08:20):

@Erik Martin-Dorel I think what was discussed was not latest but ocaml-latest actually. BTW, why is there both a latest and a latest-flambda?

view this post on Zulip Erik Martin-Dorel (Dec 10 2020 at 15:17):

Hi @Théo Zimmermann good question, actually these tags synonyms should have not been here in the first place. Just ignore them, they were here since Monday, they not documented in the docker-coq wiki, and I will remove these.

To be more precise, on https://hub.docker.com/r/coqorg/coq/:
the line
dev, dev-ocaml-latest, dev-ocaml-latest-flambda
should just read
dev
(and this line itself corresponds to a legacy dual switch image that is preserved for now for backward compatibility, and that will be removed in one week)

view this post on Zulip Erik Martin-Dorel (Dec 10 2020 at 17:06):

this issue is now fixed (I removed the extraneous tags -ocaml-latest / -ocaml-latest-flambda and updated the Docker Hub README)


Last updated: Oct 15 2021 at 19:03 UTC