Merge pull request #77 from math-comp/ci

Update CI

.github/workflows/docker-action.yml

@@ -18,8 +18,10 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.16'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -31,7 +31,7 @@ before applying the proof procedures.
   - [MathComp](https://math-comp.github.io) ssreflect 1.15 or later
   - [MathComp](https://math-comp.github.io) algebra
   - [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
-  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later
+  - [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later (known not to work with 1.17.0)
 - Coq namespace: `mathcomp.algebra_tactics`
 - Related publication(s):
   - [Reflexive tactics for algebra, revisited](https://drops.dagstuhl.de/opus/volltexte/2022/16738/) doi:[10.4230/LIPIcs.ITP.2022.29](https://doi.org/10.4230/LIPIcs.ITP.2022.29)

coq-mathcomp-algebra-tactics.opam

@@ -2,7 +2,7 @@
 # Follow the instructions on https://github.com/coq-community/templates to regenerate.
 
 opam-version: "2.0"
-maintainer: "sakaguchi@coins.tsukuba.ac.jp"
+maintainer: "kazuhiko.sakaguchi@inria.fr"
 version: "dev"
 
 homepage: "https://github.com/math-comp/algebra-tactics"
@@ -28,7 +28,7 @@ depends: [
   "coq-mathcomp-ssreflect" {>= "1.15"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-zify" {>= "1.1.0"}
-  "coq-elpi" {>= "1.15.0"}
+  "coq-elpi" {>= "1.15.0" & != "1.17.0"}
 ]
 
 tags: [

meta.yml

@@ -27,7 +27,7 @@ authors:
 - name: Kazuhiko Sakaguchi
   initial: true
 
-opam-file-maintainer: sakaguchi@coins.tsukuba.ac.jp
+opam-file-maintainer: kazuhiko.sakaguchi@inria.fr
 
 license:
   fullname: CeCILL-B Free Software License Agreement
@@ -43,9 +43,13 @@ tested_coq_nix_versions:
 tested_coq_opam_versions:
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.16'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
@@ -65,9 +69,9 @@ dependencies:
     [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
 - opam:
     name: coq-elpi
-    version: '{>= "1.15.0"}'
+    version: '{>= "1.15.0" & != "1.17.0"}'
   description: |-
-    [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later
+    [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later (known not to work with 1.17.0)
 
 namespace: mathcomp.algebra_tactics