Stream: Elpi users & devs

Topic: coq-elpi on `coq.dev` again


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (May 13 2022 at 12:57):

I think that currently docker images for coq.dev are broken

view this post on Zulip Enrico Tassi (May 13 2022 at 12:57):

so yes, outdated

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 13 2022 at 13:05):

I don't think so. I keep receiving mails of failed builds.

view this post on Zulip Ali Caglayan (May 13 2022 at 13:05):

I've been using the coq.dev opam packages no problem

view this post on Zulip Enrico Tassi (May 13 2022 at 13:05):

Note that .v file may compile, but ml files with overlays no

view this post on Zulip Enrico Tassi (May 13 2022 at 13:05):

with an outdated image

view this post on Zulip Ali Caglayan (May 13 2022 at 13:06):

Could it be the OCaml version?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 13 2022 at 13:11):

Cf. https://gitlab.com/coq-community/docker-coq/-/pipelines/538383252

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 13 2022 at 13:13):

the 4.07 image no, it does not

view this post on Zulip Théo Zimmermann (May 13 2022 at 13:13):

WDYM?

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 13 2022 at 13:14):

CC @Erik Martin-Dorel

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 18:02 UTC