Erik Martin-Dorel (Jun 16 2023 at 09:52): Erik Martin-Dorel (Jun 16 2023 at 09:52):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?
Karl Palmskog (Jun 16 2023 at 09:56):@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).
Karl Palmskog (Jun 16 2023 at 09:56):Pierre's best guess was that it's a transient issue with some overlay
Pierre Roux (Jun 16 2023 at 10:02):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.
Erik Martin-Dorel (Jun 16 2023 at 10:28):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.
Karl Palmskog (Jun 16 2023 at 10:30):OK, so we have two problems: some package coq-elpi depends on was likely updated in opam, and coq-elpi doesn't build.
Erik Martin-Dorel (Jun 16 2023 at 10:31):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.
Erik Martin-Dorel (Jun 16 2023 at 10:33):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.
Karl Palmskog (Jun 16 2023 at 10:43):either now or tomorrow is fine by me.
Erik Martin-Dorel (Jun 16 2023 at 10:44): Pierre Roux (Jun 16 2023 at 11:02):Erik Martin-Dorel said:
Note: the image of
mathcomp/mathcomp-dev:coq-devdid not change after its initial build, it is just that (1) inside the image,opam install any-packagerebuilds 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.
Pierre Roux (Jun 16 2023 at 11:02):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)
Pierre Roux (Jun 16 2023 at 11:04):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).
Paolo Giarrusso (Jun 17 2023 at 09:50):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.
Paolo Giarrusso (Jun 17 2023 at 09:53):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.
Pierre Roux (Jun 17 2023 at 21:51):@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
Alexander Gryzlov (Jun 18 2023 at 21:11):Btw, I assume mathcomp-dev means MC2 now?
Pierre Roux (Jun 18 2023 at 21:26):Yes, coq-mathcomp-ssreflect.dev is MC2, you have coq-mathcomp-ssreflect.1.dev for the matchomp-1 branch.
Pierre Roux (Jun 19 2023 at 06:51):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.
Karl Palmskog (Jun 19 2023 at 07:25):in the meantime, one could use the general Coq Docker images and install coq-mathcomp-ssreflect.1.dev manually from the extra-dev repo.
Karl Palmskog (Jun 22 2023 at 17:48):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.
Pierre Roux (Jun 23 2023 at 15:26):You're right, that should probably be >=
Karl Palmskog (Jun 23 2023 at 16:06):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).
Karl Palmskog (Jun 23 2023 at 16:11):https://github.com/coq/opam-coq-archive/pull/2617
Last updated: Nov 29 2023 at 22:01 UTC