Add additional utility packages to most MathComp Docker images

[palmskog]

When I brought up this issue on the Zulip, there seemed to be positive sentiments toward adding additional packages to the MathComp Docker images (excluding possibly some old images).

Specifically, I'm interested in having the "utility" MathComp packages that are already in the Platform:

• Hierarchy Builder + Coq-Elpi + Elpi
• MathComp Zify
• MathComp Algebra Tactics
• Finmap

In particular, Hierarchy Builder will save a lot of CI time, and probably needs to be added sooner or later anyway. Other possible candidates that may be borderline are CoqEAL.

The version choice here is probably the most complicated to figure out, but maybe we can just follow the Coq Platform, since all the candidate packages are already there?

[erikmd]

Hi @palmskog, belated Thanks for opening this issue 👍

Indeed, adding at least the four items you mention looks sensible!

I vote for adding CoqEAL as well (which is in coq-platform and often used in "computational, mathcomp-based projects")

Regarding the versions choice, I see two strategies:

1. either adding the packages without any pinning (which is a bit lax but YMMV)
2. or adding these packages with the same version pinning as coq-platform (which is more satisfactory at first sight, but maybe need some automation to ensure that they are in sync?)

Finally, there's the choice of the minimal mathcomp version to extend with these packages… maybe this question is not that critical, and we could just start with merely extending 1.15.0… but I'd be happy to know if mathcomp's maintainers also have an opinion on that!

(Cc FYI @CohenCyril @amahboubi @gares @amahboubi @pi8027 @ybertot @thery @LaurenceRideau @affeldt-aist @proux01)

[proux01]

Starting with 1.15.0 looks good to me. For the pinnings, if they lie in the gitlab file of mathcomp, maybe we can just update them with every new mathcomp releases (sounds easier to me than trying to automate the thing).

[palmskog]

After giving some thought, I think the best approach is indeed adding the packages without any pinning. It's what I tend to do in local switches (create switch, pin Coq and MathComp, no more pinning) and seems to work well, and it saves effort. One might view it as if the Platform is there to make sure some version of these packages exists for a particular MathComp and Coq version.

I think starting with extending only 1.15 is fine, and will also ensure any CI problems are somewhat contained.