search

math-comp / docker-mathcomp

Docker images of coq-mathcomp [maintainer=@erikmd]
https://hub.docker.com/r/mathcomp/mathcomp/#supported-tags
BSD 3-Clause "New" or "Revised" License
6 stars 2 forks source link

Add Mathcomp 2.2.0 #32

Closed proux01 closed 9 months ago

pi8027 commented 9 months ago

mathcomp/2.2.0-coq-dev and mathcomp-dev:coq-8.19 are still missing, or is it intentional?

proux01 commented 9 months ago

I may have missed something, we will need @erikmd help there

erikmd commented 9 months ago

Thanks @proux01 for the merge; I just pushed 2a4ec83181fbbf637e562fbc2f09b3be24c31586 Hence https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines/911869 is pending

erikmd commented 9 months ago

I will also manually update https://hub.docker.com/r/mathcomp/mathcomp#supported-tags from now on, by doing:

./external/docker-keeper/keeper.py write-artifacts
cat generated/README.md
erikmd commented 9 months ago

Question: what are all the stable mathcomp version compatible with coq 8.19 ? it seems there's not only 2.2.0

proux01 commented 9 months ago

Yes, that's the "raison d'être" of mathcomp 2.2.0.

proux01 commented 9 months ago

I mean only MC 2.2.0 and MC master do compile on Coq 8.19.

erikmd commented 9 months ago

(and 1.19.0 IINM)

so, thanks, that means that the current list @ https://hub.docker.com/r/mathcomp/mathcomp#supported-tags is complete