Closed pi8027 closed 2 years ago
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 https://github.com/coq-community/docker-coq/issues/30 … I'll let you know!
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.
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 https://github.com/coq-community/docker-coq/issues/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 https://github.com/math-comp/docker-mathcomp/pull/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)).
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
It seems to me that this issue has been addressed (although images are not mono-switch yet?). Thanks, @erikmd.
Thanks @pi8027! you're right:
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.