Request to bump OCaml version to >= 4.07.0

[pi8027]

IIUC, the image mathcomp/mathcomp:1.12.0-coq-8.14 seems to use OCaml 4.05.0, but the only released version of Coq-elpi compatible with Coq 8.14 (coq-elpi.1.11.2) requires OCaml to be 4.07.0 or later. These constraints make it unable to use Coq-elpi in this image.

[erikmd]

Hi @pi8027, (sorry for late reply, I've just seen your issue).

That's a very good point. Actually, the image mathcomp/mathcomp:1.12.0-coq-8.14 contains two switches, including one with OCaml 4.07.1. But this is not the default switch 😅
To check this, one can do e.g.:

$ docker run --rm -it mathcomp/mathcomp:1.12.0-coq-8.14 opam switch

#   switch          compiler                       description
->  4.05.0          ocaml-base-compiler.4.05.0     4.05.0
    4.07.1+flambda  ocaml-variants.4.07.1+flambda  4.07.1+flambda

So I plan to clarify this (and change the default switch) ASAP, in line with rocq-community/docker-coq#30 … I'll let you know!

[gares]

Hello @erikmd , I did debug the problem and it is unfixable on the coq-elpi side since stdlib-shims is "incomplete" on 4.05.
At the same time the Coq-Platform for 8.13 is based on 4.07, while the one for 8.14 is based on 4.10, IIRC.
Ditching 4.05 seems not a big deal to, and 4.07 is a pretty solid release.

[erikmd]

Hi @gares, thanks for your feedback;
actually I believe my earlier comment was not clear enough:
in the current version of all stable Docker images mathcomp/mathcomp:*, ocaml 4.07 was already available,
albeit not the default switch (which admittedly was making the use of these images cumbersome:
e.g., when using the docker-coq-action, one would need to override the before_install field)

Anyway, the plan was clearly to remove 4.05 when fully addressing rocq-community/docker-coq#30
and ensuring that all Docker-Coq images are mono-switch.

But in the meantime, it looks very sensible to me to do a first update of Docker-MathComp by only keeping 4.07 from now on.

So I gonna merge PR #14 now to this aim and rebuild all Docker-MathComp images, so that we'll directly get a more recent ocaml this Friday by default (namely, 4.07 (and let me know if there's some specific need regarding 4.10 as well from your side)).

[erikmd]

So I gonna merge PR #14 now to this aim and rebuild all Docker-MathComp images

Just FTR, one can follow the on-going build in this GitLab CI pipeline:

https://gitlab.com/math-comp/docker-mathcomp/-/pipelines/421498178

[pi8027]

It seems to me that this issue has been addressed (although images are not mono-switch yet?). Thanks, @erikmd.

[erikmd]

Thanks @pi8027! you're right:

• we can close this issue, indeed solved for docker-mathcomp images that are now mono-switch "after-the-fact".
• the mono-switch refactoring of docker-coq is still pending though; will look after that as soon as I can.