Add 2.4.0-rocq-prover-9.1

[pi8027]

Besides that, mathcomp/mathcomp:2.5.0-rocq-prover-dev and mathcomp/mathcomp-dev:rocq-prover-9.1 seem still lacking (on Docker Hub), although the former is already listed in images.yml. Any idea on how to fix it?

[pi8027]

Ping @erikmd and @proux01

[pi8027]

By the way, I probably should have removed 2.4.0-rocq-prover-dev. Its build fails with the following message:

#6 264.6 # File "./seq.v", line 1412, characters 3-37:
#6 264.6 # Error: The LHS of (fun_if (filter p))
#6 264.6 #     [seq x <- if _ then _ else _ | p x]
#6 264.6 # does not match any subterm of the goal

The build of 2.5.0-rocq-prover-dev still fails with the following message:

#6 244.5 # COQC HB/structures.v
#6 244.5 # File "./HB/structures.v", line 17, characters 0-30:
#6 244.5 # Error: Cannot find a physical path bound to logical path
#6 244.5 # elpi with prefix elpi.

Cf. https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/1298464

[erikmd]

Ping @erikmd

Hello @pi8027, I've just received a notification of your ping.

Unfortunately, I can't actively maintain docker-rocq anymore (context: rocq-community/docker-coq-action#88 (comment)).

So I'm afraid I won't be able to help you right now with these docker-mathcomp build errors.

Anyway:

• @Zimmi48 is aware of this need to continue maintaining Docker images of Rocq & mathcomp
• @Justme0606 will probably be able to work on docker-rocq / docker-mathcomp soon
  (as an aside: mathcomp children images are paramount IMHO, because it is a very popular Rocq core library, it is developed by Inria, pre-building it allows one to earn hours of CI time (instead of just basing upon docker-rocq images) and maintaining them "upstream" (by the principal docker-rocq maintainer) allows one to detect compatibility issues very early, and rebuild docker-mathcomp automatically via docker-keeper, as soon as a docker-rocq image changes)
• if some of you among the mathcomp maintainers is interested to help Sylvain, feel free to let @Zimmi48 know
• FYI, I published an arXiv report that recaps the architecture/initial-requirements of docker-rocq + comparison with nix:
  https://arxiv.org/abs/2510.19089
• And there's this dashboard that allows one to have a global view on docker-keeper/docker-rocq/rocker-mathcomp:
  https://github.com/erikmd/docker-keeper-dashboard

[pi8027]

Hello @erikmd, thanks a lot for the information! I will propose to discuss what we can do about this in a MathComp meeting. (Perhaps, it means that it's time to move to Nix-based CI.)

[pi8027]

Besides that, [..] mathcomp/mathcomp-dev:rocq-prover-9.1 seem still lacking (on Docker Hub), [..]

Indeed, it's in the main MathComp repo! Here is my attempt to fix it: math-comp/math-comp#1498