coq-bignums.dev does not compile with coq.dev

[ckeller]

Hi With opam, when compiling coq-bignums.dev with the last version of coq.dev, I get the following error:

CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
File "plugin/bignums_syntax.ml", line 101, characters 57-112:
# 101 |       DAst.make ?loc @@ GApp (ref_W0, [DAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous)])
#                                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: The constructor GHole expects 3 argument(s),
#        but is applied here to 2 argument(s)

Thanks!

[proux01]

Strange the CI of Coq should prevent that and I just tested locally without issues. Could you try an opam update and rebuild both Coq and bignums? (maybe something like opam reinstall coq-core.dev coq-stdlib.dev coq-bignums.dev)?

[SkySkimmer]

3-arguments GHole was removed in https://github.com/coq/coq/pull/17220 so either your coq.dev version is not actually the latest, or some other install is getting used

[ckeller]

Thanks for your replies!

Could you try an opam update and rebuild both Coq and bignums? (maybe something like opam reinstall coq-core.dev coq-stdlib.dev coq-bignums.dev)?

What is failing is doing opam update && opam upgrade on the docker image coqorg/coq:dev. I tried this morning on another computer and it works. Maybe I was in a strange state with my containers on the other computer... Sorry for the noise.

[erikmd]

Hi @ckeller !

I'm not 100% sure (only you could confirm if you kept the image) but I can explain what you observed if you used a coqorg/coq:dev image:

The coq version is pinned (opam pin list) to the SHA1 of coq.master at the time the images are rebuilt by docker-keeper.

Note that this is necessary because coq.master is rebuilt roughly 4 times in Docker-Coq (for 4 different ocaml versions) at slightly different times, so we want to avoid "race conditions" over there.

If you want to upgrade your image, I'd suggest doing sudo docker pull coqorg/coq:dev anew and if you're not sure how to share a common directory between several containers, just use volumes or bind-mounts, using -v. E.g., sudo docker run -it -v "$PWD:$PWD" -w "$PWD" coqorg/coq:dev bash You can also pass --rm if you want to make the container ephemeral.

[ckeller]

Hi @erikmd I kept the image and indeed, doing docker pull coqorg/coq:dev before all works. Many thanks!