Stream: math-comp devs

Topic: 2 questions about mathcomp/mathcomp-dev:coq-dev (MC master)


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Karl Palmskog (Jun 16 2023 at 09:56):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 16 2023 at 10:43):

either now or tomorrow is fine by me.

view this post on Zulip Erik Martin-Dorel (Jun 16 2023 at 10:44):

Done

view this post on Zulip Pierre Roux (Jun 16 2023 at 11:02):

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.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alexander Gryzlov (Jun 18 2023 at 21:11):

Btw, I assume mathcomp-dev means MC2 now?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre Roux (Jun 23 2023 at 15:26):

You're right, that should probably be >=

view this post on Zulip 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).

view this post on Zulip Karl Palmskog (Jun 23 2023 at 16:11):

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


Last updated: Jul 24 2024 at 13:02 UTC