Update Docker CI

Author: pi8027

.github/workflows/docker-action.yml

@@ -17,9 +17,13 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-8.20'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.1'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:

README.md

@@ -24,10 +24,10 @@ which will be used to subsume notations for finite sets, eventually.
   - Cyril Cohen (initial)
   - Kazuhiko Sakaguchi
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.20 to 9.0
+- Compatible Rocq/Coq versions: 8.20 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io)
-- Coq namespace: `mathcomp.finmap`
+  - [MathComp](https://math-comp.github.io) ssreflect 2.2.0 or later
+- Rocq/Coq namespace: `mathcomp.finmap`
 - Related publication(s): none
 
 ## Building and installation instructions
@@ -37,7 +37,7 @@ is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-mathcomp-finmap
+opam install rocq-mathcomp-finmap
 ```
 
 To instead build and install manually, do:

meta.yml

@@ -31,25 +31,33 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.20 to 9.0
-  opam: '{ (>= "8.20" & < "8.21~") | (= "dev") }'
+  text: 8.20 or later
+  opam: '{>= "8.20"}'
 
 tested_coq_opam_versions:
-- version: '2.3.0-coq-8.20'
+- version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.20'
+- version: '2.4.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
+- version: '2.4.0-rocq-prover-9.1'
+  repo: 'mathcomp/mathcomp'
+- version: '2.5.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
+- version: '2.5.0-rocq-prover-9.1'
+  repo: 'mathcomp/mathcomp'
+- version: 'rocq-prover-9.1'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: rocq-mathcomp-ssreflect
-    version: '{ (>= "2.0" & < "2.5~") | (= "dev") }'
+    version: '{>= "2.2.0"}'
   description: |-
-    [MathComp ssreflect 2.0 to 2.3](https://math-comp.github.io)
+    [MathComp](https://math-comp.github.io) ssreflect 2.2.0 or later
 
 namespace: mathcomp.finmap
 

rocq-mathcomp-finmap.opam

@@ -22,9 +22,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   ("coq" {>= "8.20" & < "8.21~"}
-  | "rocq-core" {>= "9.0" | = "dev"})
-  ("coq-mathcomp-ssreflect" { >= "2.0" & < "2.4~" }
-  |"rocq-mathcomp-ssreflect" { (>= "2.4" & < "2.5~") | = "dev" })
+  | "rocq-core" {>= "9.0"})
+  ("coq-mathcomp-ssreflect" { >= "2.2" & < "2.4~" }
+  |"rocq-mathcomp-ssreflect" { >= "2.4" })
 ]
 
 tags: [