Please rebuild images with latest dune

[JasonGross]

I'm seeing opam decide to recompile Coq due to "upstream or system changes" in dune, if I try to install any Coq package https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/4625517245/jobs/8181344979#step:5:457

[Alizter]

@JasonGross You can also pin the Dune version to avoid the upgrade.

[JasonGross]

What's the command for doing that?

[Alizter]

opam pin add dune <version>

[JasonGross]

@JasonGross You can also pin the Dune version to avoid the upgrade.

dune is already pinned to 3.6.1, opam still wants to update it to 3.6.1 if I install coq-equations

[Alizter]

@JasonGross Once you pin you will have to upgrade once. What version are you current at that you want to stay at? You should pin to that. All pinning will do is tell the opam solver to not update that dependency once the version constraint is satisfied.

[Alizter]

However if I have understood correctly you are saying that Dune is 3.6.1 and even when pinned to that verison, installing equations will cause a rebuild?

[JasonGross]

What version are you current at that you want to stay at?

3.6.1, according to opam list, and it's already pinned. Pinning does not prevent recompilation

https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/4629119643/jobs/8188996268#step:5:518 https://github.com/coq-community/run-coq-bug-minimizer/actions/runs/4629119643/jobs/8188996268#step:5:556

However if I have understood correctly you are saying that Dune is 3.6.1 and even when pinned to that verison, installing equations will cause a rebuild?

Yes

[Alizter]

I have no idea what has happened there. I guess @erikmd you should update to 3.7.1 so that the version is stable.

[erikmd]

Hi all!

Thanks for opening the issue 🙃

This is a normal issue, caused by the merge of https://github.com/ocaml/opam-repository/pull/23574 yesterday.

Feel free to let me know by an issue or by a Zulip message if you face with similar "upstream or system changes" anew.

For this symptom, the standard solution is to rebuild all images to incorporate the latest version of the package from upstream opam-repository.

But as pointed out by @Alizter, we can now benefit from the dune.3.7.1 package, released 2 days ago.

I pushed a commit, a docker-base pipeline is on-going, and tomorrow I'll rebuild the docker-coq images.

[erikmd]

BTW

You can also pin the Dune version to avoid the upgrade.

dune is already pinned, cf. this line.

As said before, the only "issue" here is an upstream change in opam-repository.

Whatever is the pinning state of the dune package, every ocaml user in the ecosystem will need to update one's switch.

[erikmd]

and tomorrow I'll rebuild the docker-coq images.

A very last rebuild is on-going. Closing the issue now.

[erikmd]

Note: if you use mathcomp/mathcomp images (built on gitlab.com), the runner over there is broken, so we should wait for a couple of days to migrate to gitlab.inria.fr, so that latest dune is also available in mathcomp/mathcomp images.

[Alizter]

@erikmd Do you build the images on Gitlab? It should be possible to build them in Github.

[erikmd]

@Alizter basically, all {coqorg/base, coqorg/coq, mathcomp/mathcomp, mathcomp/mathcomp-dev} Docker images are built within GitLab CI with the docker-keeper tooling I developed (cf. my Coq Workshop 2020 talk), which is much more expressive w.r.t. what we can do with GHA (e.g., GHA workflows cannot use YAML &anchors), so no need to move away from this technical solution.

The only issue is that MathComp is not under an OSI-approved free license, and as a result, we don't benefit from CI minutes enough since a couple of months.

So we recently worked together with @Zimmi48 and @maximedenes:

• in order to implement coq/bot#234,
• generalize coqbot to change the gitlab domain name,
• and finally migrate the GitLab CI mathcomp repos to gitlab.inria.fr, which comes with Inria builtin runners.

As soon as all this is implemented, I'll post an announcement on Zulip.