Update CI

Author: pi8027

.github/workflows/docker-action.yml

@@ -17,45 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.18'
           - 'mathcomp/mathcomp:1.19.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-coq-8.20'

README.md

@@ -42,9 +42,9 @@ slices in the input.
   - Kazuhiko Sakaguchi (initial)
   - Cyril Cohen
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Coq versions: 8.13 or later
+- Compatible Coq versions: 8.19 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.13.0 or later
+  - [MathComp](https://math-comp.github.io) 1.19.0, 2.2.0, or later
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
   - [Mczify](https://github.com/math-comp/mczify) (required only for `icfp25/`)
   - [Equations](https://github.com/mattam82/Coq-Equations) (required only for `icfp25/`)

coq-stablesort.opam

@@ -37,13 +37,11 @@ In addition, each of the above two kinds of mergesort functions has a smooth
 slices in the input."""
 
 build: [make "-j%{jobs}%"]
-# The filter below has been added by hand to avoid running the test suite with
-# Coq 8.17 or MathComp < 1.15.
-run-test: [ [make "-j%{jobs}%" "build-icfp25" ] { "1.16~" <= coq-mathcomp-ssreflect:version & (coq:version < "8.17~" | "8.18~" <= coq:version) } ]
+run-test: [make "-j%{jobs}%" "build-icfp25"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.13"}
-  "coq-mathcomp-ssreflect" {>= "1.13.0"}
+  "coq" {>= "8.19"}
+  "coq-mathcomp-ssreflect" {(>= "1.19.0" & < "2.0~") | (>= "2.2.0")}
   "coq-paramcoq" {>= "1.1.3"}
   "coq-mathcomp-zify" {with-test}
   "coq-equations" {with-test}

meta.yml

@@ -52,90 +52,18 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.13 or later
-  opam: '{>= "8.13"}'
+  text: 8.19 or later
+  opam: '{>= "8.19"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.13'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.14'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '1.19.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.19.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.19.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '1.19.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '2.3.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
@@ -156,9 +84,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.13.0"}'
+    version: '{(>= "1.19.0" & < "2.0~") | (>= "2.2.0")}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.13.0 or later
+    [MathComp](https://math-comp.github.io) 1.19.0, 2.2.0, or later
 - opam:
     name: coq-paramcoq
     version: '{>= "1.1.3"}'