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

[ckeller]

Hi @erikmd
I kept the image and indeed, doing docker pull coqorg/coq:dev before all works. Many 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 coq/coq#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.