Karl Palmskog (May 13 2022 at 12:50): Karl Palmskog (May 13 2022 at 12:50):So it seems there are coq-elpi issues again on coq.dev:
# CAMLC -c src/coq_elpi_utils.mli
# CAMLC -c src/coq_elpi_HOAS.mli
# File "src/coq_elpi_HOAS.mli", line 100, characters 62-86:
# Error: Unbound module ComInductive.Mind_decl
# make[2]: *** [Makefile.coq:725: src/coq_elpi_HOAS.cmi] Error 2
# make[1]: *** [Makefile:50: build-core] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.07.1+flambda/.opam-switch/build/coq-elpi.dev'
# make: *** [Makefile:42: all] Error 2
See for example this build. Is this known, or can one do something?
Karl Palmskog (May 13 2022 at 12:52):hmm, I'm confused about the OCaml version here... could that be the issue? the mathcomp-dev:coq-dev Docker image is not up to date, and some old Coq master is used?
Enrico Tassi (May 13 2022 at 12:57):I think that currently docker images for coq.dev are broken
Enrico Tassi (May 13 2022 at 12:57):so yes, outdated
Karl Palmskog (May 13 2022 at 13:04):the general Docker images for coq.dev are back on track I believe. I think this error only pertains to MathComp Docker
Théo Zimmermann (May 13 2022 at 13:05):I don't think so. I keep receiving mails of failed builds.
Ali Caglayan (May 13 2022 at 13:05):I've been using the coq.dev opam packages no problem
Enrico Tassi (May 13 2022 at 13:05):Note that .v file may compile, but ml files with overlays no
Enrico Tassi (May 13 2022 at 13:05):with an outdated image
Ali Caglayan (May 13 2022 at 13:06):Could it be the OCaml version?
Théo Zimmermann (May 13 2022 at 13:06):If you don't want an outdated image, you can already switch to using one of the images with an explicit (compatible) OCaml version.
Ali Caglayan (May 13 2022 at 13:06):I mean I had to pin 4.13.1 since we are still sorting out the 4.14 compatibility.
Théo Zimmermann (May 13 2022 at 13:06):@Ali Caglayan Yes, the default Docker-Coq image uses a version of OCaml that is too old.
Enrico Tassi (May 13 2022 at 13:09):# Error: Unbound module ComInductive.Mind_decl
This is an old version of Coq, I did introduce this module a while back
Théo Zimmermann (May 13 2022 at 13:11):Cf. https://gitlab.com/coq-community/docker-coq/-/pipelines/538383252
Enrico Tassi (May 13 2022 at 13:11):I can't find the hash of Coq in the log. Is it there? if not we should add it.
Théo Zimmermann (May 13 2022 at 13:12):No idea but my point is that the main image does not build and has not been built since the OCaml version bump.
Enrico Tassi (May 13 2022 at 13:13):the 4.07 image no, it does not
Théo Zimmermann (May 13 2022 at 13:13):WDYM?
Karl Palmskog (May 13 2022 at 13:13):I think the root issue here is that mathcomp-docker uses 4.07.1 as the default Ocaml version, which needs bumping
Enrico Tassi (May 13 2022 at 13:14):CC @Erik Martin-Dorel
Paolo Giarrusso (May 13 2022 at 16:38):I mean I had to pin 4.13.1 since we are still sorting out the 4.14 compatibility.
@Ali Caglayan Karl's diagnosis is right, but FWIW the 4.14 issues seem solved — at least, they are fully solved IME with Coq 8.15.x
Erik Martin-Dorel (May 15 2022 at 23:40):Hi ! Thanks for the ping.
Karl Palmskog said:
I think the root issue here is that mathcomp-docker uses 4.07.1 as the default Ocaml version, which needs bumping
That's a very good point. At least for coq ≥ dev, the ocaml base image for docker-mathcomp should also be bumped accordingly.
I'll look after this ASAP; meanwhile, I removed the images tagged "dev" that were stalled to reduce "surprise" as much as possible
(anyway in case of doubt, the build date of all images is always indicated in
https://hub.docker.com/r/mathcomp/mathcomp/tags & https://hub.docker.com/r/coqorg/coq/tags )
Last updated: Oct 13 2024 at 01:02 UTC