Help with docker-coq/docker-mathcomp rebuilds: looking for a volunteer

[erikmd]

TL;DR: would a person from @coq/core volunteer to help me trigger docker-base or docker-coq rebuilds?

Concretely, the problem:

• {docker-coq, docker-mathcomp} images aim to earn CI time by providing pre-compiled opam switches with coq+bignums(+coq-mathcomp-character).
• around several times per month, it happens some base opam packages are modified upstream, impyling coq is "rebuilt downstream" which thereby temporarily reduces the usefulness of the prebuilt coq. See the Example log below that shows the standard log pattern in this case.

The solution:

• last week-end, I significantly improved the docker-keeper tool to allow "transitive rebuilds", and propagate strategy, and HEAD commit message parsing.
• now, it is as easy as running

  cd docker-coq
  git pull
  git commit --allow-empty -m "docker-keeper: rebuild-all"
  git push
  

  or (depending on the layers that have to be rebuilt)

  cd docker-base
  git pull
  git commit --allow-empty -m "docker-keeper: rebuild-all"
  git push
  

• see also the Zulip thread which provides more technical details, and the discussion with @palmskog that led to this call
• to sum up, I wouldn't want to be the only person that can trigger rebuilds, hence this volunteer call @coq/core
  (I also opened a call for math-comp/core)
• the next step would be to post a message on Coq Discourse to tell end users about the typical log pattern below, and the possibility to ping me or the volunteer people.

Example log (in docker-coq-action CI jobs)

https://github.com/coq-community/graph-theory/actions/runs/9684414743/job/26722132412

  The following actions will be performed:
    - recompile conf-gmp               4             [upstream or system changes]
    - recompile zarith                 1.13*         [uses conf-gmp]
    - recompile coq-core               8.18.0        [uses zarith]
    - recompile coqide-server          8.18.0        [uses coq-core]
    - recompile coq-stdlib             8.18.0        [uses coq-core]
    - recompile coq                    8.18.0*       [uses coq-core]
    - recompile coq-serapi             8.18.0+0.18.3 [uses coq]
    - recompile coq-elpi               1.19.3        [uses coq]
    - recompile coq-bignums            9.0.0+coq8.18 [uses coq]
    - recompile coq-hierarchy-builder  1.6.0         [uses coq-elpi]
    - recompile coq-mathcomp-ssreflect 2.0.0*        [uses coq]
    - install   coq-mathcomp-finmap    2.1.0
    - recompile coq-mathcomp-fingroup  2.0.0*        [uses coq-mathcomp-ssreflect]
    - recompile coq-mathcomp-algebra   2.0.0*        [uses coq-mathcomp-fingroup]
    - recompile coq-mathcomp-solvable  2.0.0*        [uses coq-mathcomp-algebra]
    - recompile coq-mathcomp-field     2.0.0*        [uses coq-mathcomp-solvable]
    - recompile coq-mathcomp-character 2.0.0*        [uses coq-mathcomp-field]
  ===== 1 to install | 16 to recompile =====

In particular, see the [upstream or system changes]and the recompile zarith patterns. (In this case, a docker-base rebuild is needed.)