Upgrade OCaml

[liyishuai]

4.07.1 is not so "edge" anymore.
Consider bumping COMPILER_EDGE to 4.08+?
The latest version is 4.10.0.

[erikmd]

Hi @liyishuai, thanks for opening this.

4.07.1 is not so "edge" anymore.

everything is relative ;-)

But indeed the COMPILER_EDGE switch may deserve an update. Actually the last time I had taken a look to bump to 4.08, one such update was not possible due to "ocaml" constraints in the opam packages of Coq.

Now, we get for the Coq versions mentioned in the wiki:

$ for v in 8.4.6 8.5.3 8.6.1 8.7.2 8.8.2 8.9.1 8.10.2 8.11.0; do \
  echo coq."$v"; opam show coq."$v" | grep \"ocaml\"; done

coq.8.4.6
depends:      "ocaml" {>= "3.11.2" & < "4.03"}
coq.8.5.3
depends:      "ocaml" {>= "3.12.1" & < "4.06.0"} "camlp5" "num" "conf-findutils" {build}
coq.8.6.1
depends:      "ocaml" {>= "4.01.0" & < "4.06.0"}
coq.8.7.2
depends:      "ocaml" {>= "4.02.3" & < "4.10"}
coq.8.8.2
depends:      "ocaml" {>= "4.02.3" & < "4.10"}
coq.8.9.1
depends:      "ocaml" {>= "4.02.3" & < "4.10"}
coq.8.10.2
depends:      "ocaml" {>= "4.05.0" & < "4.10"}
coq.8.11.0
depends:      "ocaml" {>= "4.05.0" & < "4.10"}

Coq 8.7+ should then be compatible with 4.09.0+flambda.

So if you update your PR #5 to use 4.09.0+flambda, I'll be happy to merge it in a couple of days (not immediately as I'm quite busy this week and this update will require proper announcement, given a number of docker-coq users have hard-coded "4.07.1+flambda" in their CI script instead of relying on the \$COMPILER_EDGE env. variable suggested here).

[liyishuai]

I've updated the PR.
Yes I'm among the users not aware of COMPILER_EDGE variable and hard-code OCaml versions. Documentation is essential.

[erikmd]

@liyishuai

Documentation is essential.

Yes − it was already documented here: https://github.com/coq-community/docker-coq/wiki

Note: The switches identifiers are available as environment variables in the images, see the related CI setup / Remarks section

but I guess we could elaborate a bit more on this remark, indeed (e.g. to explicitly recommend doing opam switch \${COMPILER_EDGE}; eval \$(opam env) rather than opam switch 4.07.0+flambda)

[erikmd]

but I guess we could elaborate a bit more on this remark, indeed (e.g. to explicitly recommend doing opam switch \${COMPILER_EDGE}; eval \$(opam env) rather than opam switch 4.07.0+flambda)

So @liyishuai I've added another note at the end of this section:
https://github.com/coq-community/docker-coq/wiki#supported-tags

[erikmd]

as a follow-up of the discussion in #5, after @liyishuai's comment:

We can first add some new tags (immediately), and announce that existing tags are subject to changes (that may alias to the added tags) in the future.

all things considered, this could be a working solution;
to sum up the plan:

1. for the moment we keep the 2-switches current images (with 4.05.0, 4.07.1+flambda)

2. for the images requested by @liyishuai with OCaml 4.09, we could rely on a new base image coqorg/base:4.09.0-flambda (that is currently being built, cf. this new branch 4.09.0-flambda)

3. using that new base image, we'll be able to distribute images tagged e.g. coqorg/coq:8.8-4.09, coqorg/coq:8.9-4.09, coqorg/coq:8.10-4.09, coqorg/coq:8.11-4.09, (or coqorg/coq:8.8-ocaml-4.09, coqorg/coq:8.9-ocaml-4.09, coqorg/coq:8.10-ocaml-4.09, coqorg/coq:8.11-ocaml-4.09) for coqorg/coq users that really want the latest OCaml switch that is compatible with Coq 8.8+.

4. ultimately, we could split the images currently containing 2-switches, e.g. coqorg/coq:8.7 → coqorg/coq:8.7 (switch=4.05.0) + coqorg/coq:8.7-4.07 (switch=4.07.1+flambda), which BTW will have two upsides:

   • the size of all images will be divided by 2;
   • for the coqorg/coq users, it will be much easier to choose the 4.07.1+flambda image in the first place (no need for opam switch \$COMPILER_EDGE; eval \$(opam env) any longer)

   the main drawback is that this will increase the "combinatorics" of the repo, so I'm afraid this 4th item wouldn't scale currently with coqorg/coq still used as a Docker-Hub automated-build. So IMO it should be undertaken only after an infrastructure change for coqorg/coq and coqorg/mathcomp, e.g. similar to what I suggested in [external issue] compilation error using coqorg/coq:dev with opam unpin coq; opam upgrade bignums#36 (comment). I'm willing to have a look at this in the upcoming days. Anyway I guess that in the very end, coqorg/base could stay as is, as an automated build.

[For the moment, the step 2 only is on-going, but I'd like to wait for some feedback of @Zimmi48 / @ejgallego before undertaking step 3 above…]

[Zimmi48]

This plan looks good to me, and indeed generating the images on GitLab CI might make things more practical. As for the name, I'm in favor of going for the explicit ocaml-.

[erikmd]

Also, in my last comment I only mentioned the stable versions of Coq (with suffix -ocaml-4.09), but @liyishuai also talked about coqorg/coq:dev-ocaml-4.09: #5 (comment)

This is also feasible and I can easily setup a nightly build for this image as well by updating the corresponding cron task, but note that as long as the nightly builds will be built directly in Docker Hub (with the single worker available in our Docker Hub organization), a potential issue with having >=2 different images for coq.dev is that if a Coq PR is merged between say 00:00 and 02:00 Paris Time, maybe the two images coqorg/coq:dev and coqorg/coq:dev-ocaml-4.09 won't have the same commit SHA1.

This is probably a minor issue, but as I had already said in coq-community/bignums#36 (comment), this could ultimately be solved if we decide to switch those nightly builds in "pull-mode" to some dedicated jobs in Coq's main CI in "push-mode" (from Gitlab CI to Docker Hub as well).

Anyway, the nightly builds work well for the time being :) and up to now I didn't get other complaints regarding the lag between coqorg/coq:dev and coq@master, so I'd say this other refactoring for coqorg/coq:dev could be undertaken after the 1.-2.-3.-4. plan of my previous comment, maybe :)

[ejgallego]

Note that there is good news upstream, OCaml developers are kindly looking into the performance bug, so maybe 4.10.1 could work fine and thus be used [with less effort in restructuring the docker setup]

[erikmd]

@ejgallego @liyishuai FYI step 3. is now complete, so coqorg/coq:*-ocaml-4.09.0-flambda images are ready.

For example:

$ docker run --rm -it coqorg/coq:8.10-ocaml-4.09.0-flambda bash -c "opam switch && opam list"
Unable to find image 'coqorg/coq:8.10-ocaml-4.09.0-flambda' locally
8.10-ocaml-4.09.0-flambda: Pulling from coqorg/coq
[…]
Status: Downloaded newer image for coqorg/coq:8.10-ocaml-4.09.0-flambda
#   switch          compiler                       description
->  4.09.0+flambda  ocaml-variants.4.09.0+flambda  4.09.0+flambda
# Packages matching: installed
# Name         # Installed    # Synopsis
base-bigarray  base
base-threads   base
base-unix      base
conf-findutils 1              Virtual package relying on findutils
conf-m4        1              Virtual package relying on m4
coq            8.10.2         pinned to version 8.10.2
coq-bignums    8.10.0         Bignums, the Coq library of arbitrary large number
dune           2.4.0          pinned to version 2.4.0
num            1.3            pinned to version 1.3
ocaml          4.09.0         The OCaml compiler (virtual package)
ocaml-config   1              OCaml Switch Configuration
ocaml-variants 4.09.0+flambda Official release 4.09.0, with flambda activated
ocamlfind      1.8.1          pinned to version 1.8.1
opam-depext    1.1.3          Query and install external dependencies of OPAM pa

See the complete list of tags here:
https://hub.docker.com/r/coqorg/coq/tags

To do this I needed to refactor the Docker Hub hooks that take care of pushing tag alises, and I've also setup a cron automated build for coqorg/coq:dev-ocaml-4.09.0-flambda that will rebuild that image each night just after coqorg/coq:dev.

@liyishuai feel free to test these new images :)

I didn't update the wiki for now as:

1. this wiki update should be done once we're ready to announce this evolution and I'd like to get some input from @Zimmi48 before that (and we'll both have very little time till next week)

2. the evolution at stake is fully backward-compatible for now, given the Dockerfile of already-existing images (without the -ocaml-4.09.0-flambda suffix) have been kept as is as we discussed above (but I've rebuilt them as well to take Base image should try to install Coq deps. #7 into account for the base images)

[ejgallego]

That's very cool @erikmd ; I am wondering how download / build times do compare when using the image with only one OCaml switch.

Maybe splitting the images per-switch would yield better overall efficiency?

[erikmd]

Hi @ejgallego, thanks for your comment! and sorry for late reply.

Maybe splitting the images per-switch would yield better overall efficiency?

Yes! actually this is exactly what I was planning to do in the upcoming weeks (cf. item 4. of the plan mentioned in #4 (comment)), but I'll certainly need to switch the platform in charge of performing the builds before doing/announcing that. Théo rightly suggested that GitLab CI could be the way to go.

I am wondering how download / build times do compare when using the image with only one OCaml switch.

Good idea, I'll do some benchmarks at that time.

[erikmd]

Closed as subsumed by issue coq-community/docker-coq#4