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?
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)
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
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.
@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.
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.
Aren't there docker images for ocaml? (I don't know)
Yes there are.
Nobody is talking about testing 20 variants. You are stretching things quite a lot.
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.
#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.
Ah, I had misunderstood. I thought you were talking about 20 variants of OCaml.
I was not clear, sorry. I hope it makes more sense now.
We're indeed well past 20. Just have a look at the list here: https://hub.docker.com/r/coqorg/coq
(Though some tags are synonyms.)
It seems for coq master and 8.13+beta we have:
maybe latest=4.11 ?
Erik said 4
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.
The point of 4.07 is that it has been quite recommended for Coq.
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
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.
4.05.0 is a terrible version to depend on. It has given us enormous grief in the opam archive.
so personally, I find it unreasonable to say that we should all have our projects that include OCaml code build with 4.05.0
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)?
if it were up to me, I would drop 4.05.0 from everywhere
Enrico Tassi said:
maybe latest=4.11 ?
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:
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!)
@Erik Martin-Dorel I think what was discussed was not
ocaml-latest actually. BTW, why is there both a
latest and a
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/:
dev, dev-ocaml-latest, dev-ocaml-latest-flambda
should just read
(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)
this issue is now fixed (I removed the extraneous tags
-ocaml-latest-flambda and updated the Docker Hub README)
Last updated: Nov 29 2023 at 17:01 UTC