Hi, I noticed the following two issues in the CI/CD cron job of docker-coq-action:

https://github.com/coq-community/docker-coq-action/actions/runs/5282157912/jobs/9556715975

Cc @Pierre Roux @Reynald Affeldt @Cyril Cohen @Théo Zimmermann @Karl Palmskog FYI

Issue 1:

```
The following actions will be performed:
- recompile coq-elpi dev [upstream or system changes]
- recompile coq-hierarchy-builder dev [uses coq-elpi]
- recompile coq-mathcomp-ssreflect dev* [uses coq-hierarchy-builder]
- recompile coq-mathcomp-fingroup dev* [uses coq-mathcomp-ssreflect]
- recompile coq-mathcomp-algebra dev* [uses coq-mathcomp-fingroup]
- recompile coq-mathcomp-solvable dev* [uses coq-mathcomp-algebra]
- recompile coq-mathcomp-field dev* [uses coq-mathcomp-solvable]
- recompile coq-mathcomp-character dev* [uses coq-mathcomp-field]
```

but coq-elpi's opam package was not updated recently; so I suspect that what could get rid of the rebuild is an opam pin… do you agree?

Issue 2:

```
Error: The compilation of coq-elpi.dev failed at "make COQBIN=/home/coq/.opam/4.13.1+flambda/bin/ ELPIDIR=/home/coq/.opam/4.13.1+flambda/lib/elpi OCAMLWARN=".
#=== ERROR while compiling coq-elpi.dev =======================================#
# context 2.1.3 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/extra-dev#2023-06-13 19:50
# path ~/.opam/4.13.1+flambda/.opam-switch/build/coq-elpi.dev
# command /usr/bin/make COQBIN=/home/coq/.opam/4.13.1+flambda/bin/ ELPIDIR=/home/coq/.opam/4.13.1+flambda/lib/elpi OCAMLWARN=
# exit-code 2
# env-file ~/.opam/log/coq-elpi-936-bac9e2.env
# output-file ~/.opam/log/coq-elpi-936-bac9e2.out
### output ###
# [...]
# 2624 | ComCoercion.try_add_new_coercion_with_target gr ~local ~poly
# 2625 | ~reversible ~source ~target
# 2626 | | _, _ ->
# 2627 | ComCoercion.try_add_new_coercion gr ~local ~poly ~reversible
# 2628 | end.
# Error: This expression has type nonuniform:bool -> unit
# but an expression was expected of type unit
# because it is in the left-hand side of a sequence
# make[2]: *** [Makefile.coq:738: src/coq_elpi_builtins.cmo] Error 2
# make[1]: *** [Makefile:50: build-core] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-elpi.dev'
# make: *** [Makefile:42: all] Error 2
```

do you have a clue about this error?

@Erik Martin-Dorel unfortunately no clue about the Elpi issue, which I posted about here yesterday. We could try to ping Enrico, but he is likely very busy today (Coq Workshop stuff).

Pierre's best guess was that it's a transient issue with some overlay

I guess regenerating images on pushes on Coq master is not enough for PR with overlays since those overlays are usually merged after the PR itself. So I guess we either should hope for another PR without overlays to be merged shortly after or have a way to rebuild the DOcker image once overlays are merged.

Note: the image of `mathcomp/mathcomp-dev:coq-dev`

did not change after its initial build, it is just that (1) inside the image, `opam install any-package`

rebuilds coq-elpi, which fails and also (2) it is now impossible to rebuild the image. So I suspect that there's a more recent non-backward compat. change in coq-dev side.

OK, so we have two problems: some package coq-elpi depends on was likely updated in opam, and coq-elpi doesn't build.

For the first problem, I don't think there's a dependency of coq-elpi that was updated: as said in my initial post, coq-elpi and coq-hierarchical-builder are the only dev packages in mathcomp 2 that are not pinned; so maybe after each new commit in coq-elpi (without a pin), there's a rebuild. Just guessing anyway!

So I'll investigate further on this first problem this WE.

For the second issue I don't know but maybe @Enrico Tassi will be able to tell later on when he has more time.

In the meantime, I propose to remove the stalled image `mathcomp/mathcomp-dev:coq-dev`

(now ? tomorrow ?) so that as soon as the image builds anew, it is pushed.

either now or tomorrow is fine by me.

Erik Martin-Dorel said:

Note: the image of

`mathcomp/mathcomp-dev:coq-dev`

did not change after its initial build, it is just that (1) inside the image,`opam install any-package`

rebuilds coq-elpi, which fails and also (2) it is now impossible to rebuild the image. So I suspect that there's a more recent non-backward compat. change in coq-dev side.

When did you try? Given the error Karl is highlighting, I'd really expect that overlay (metged just 20 hours away) to fix it.

More generally, I think this point an issue with Coq PR with overlays, do we have a better plan than removing the image? (which is a bit sad)

BTW, I think we shouldn't remove the image but just wait for the next Coq PR to be merged (there have not been any in the last 24 hours which explains it is still broken, but that's frequent enough).

In such cases, `opam install --fake coq-elpi`

should shut up opam, and one can request a rebuild later with `opam upgrade coq-elpi`

, or `opam reinstall coq-elpi`

if no opam sees no upgrades available.

I've recently seen such spurious rebuilds (without changes) when creating Docker images and cleaning .opam aggressively (say, removing downloaded sources...); IIRC, opam has become pickier here than a while ago. This might affect packages differently depending on their sources/pinning strategy.

@Karl Palmskog after merging PR in Coq, the mathcomp-dev:coq-dev Docker image is back: https://hub.docker.com/r/mathcomp/mathcomp-dev/tags

Btw, I assume `mathcomp-dev`

means MC2 now?

Yes, `coq-mathcomp-ssreflect.dev`

is MC2, you have `coq-mathcomp-ssreflect.1.dev`

for the matchomp-1 branch.

I mean for the OPAM packages, for Docker images, an image based on the mathcomp-1 branch should be added but is not there yet.

in the meantime, one could use the general Coq Docker images and install `coq-mathcomp-ssreflect.1.dev`

manually from the `extra-dev`

repo.

is `coq-mathcomp-ssreflect.dev`

in the `extra-dev`

opam repo supposed to have `"coq-hierarchy-builder" {= "1.4.0"}`

? This means that one can't use the package without activating the `released`

repo. The GitHub repo version has `>= "1.4.0"`

, which seems more reasonable.

You're right, that should probably be `>=`

should I do the PR? This problem hit me a couple of times now (not having the `released`

repo in a switch, can't install `coq-mathcomp-ssreflect.dev`

).

https://github.com/coq/opam-coq-archive/pull/2617

Last updated: Nov 29 2023 at 22:01 UTC