Update Docker CI

Author: pi8027

.github/workflows/docker-action.yml

@@ -9,6 +9,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 jobs:
   build:
@@ -17,9 +18,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
@@ -36,15 +36,19 @@ The easiest way to install the latest released version of Finite maps
 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 repo add rocq-released https://rocq-prover.org/opam/released
+opam install rocq-mathcomp-finmap
 ```
 
-To instead build and install manually, do:
+To instead build and install manually, you need to make sure that all the
+libraries this development depends on are installed.  The easiest way to do that
+is still to rely on opam:
 
 ``` shell
 git clone https://github.com/math-comp/finmap.git
 cd finmap
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install --deps-only .
 make   # or make -j <number-of-cores-on-your-machine> 
 make install
 ```

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: [