refresh boilerplate and CI and bump Dune to 3.5 or later

.github/workflows/docker-action.yml

@@ -15,16 +15,18 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/DistributedComponents/disel/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/DistributedComponents/disel/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/DistributedComponents/disel/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/DistributedComponents/disel/actions/workflows/docker-action.yml
 
 
 
@@ -28,7 +28,7 @@ from implementation details.
 - License: [BSD 2-Clause "Simplified" license](LICENSE)
 - Compatible Coq versions: 8.14 or later
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices)
+  - [MathComp](https://math-comp.github.io) 1.13.0 to 1.19.0 (`ssreflect` suffices)
   - [FCSL PCM](https://github.com/imdea-software/fcsl-pcm) 1.7.0 or later
   - [Hoare Type Theory](https://github.com/imdea-software/htt) 1.2.0 or later
 - Coq namespace: `DiSeL`

coq-disel-calculator.opam

@@ -12,7 +12,7 @@ build: [make "-j%{jobs}%" "calculator"]
 depends: [
   "ocaml" {>= "4.05.0"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}

coq-disel-examples.opam

@@ -10,9 +10,9 @@ synopsis: "Example systems for Disel, a separation-style logic for compositional
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-disel" {= version}
 ]

coq-disel-tpc.opam

@@ -12,7 +12,7 @@ build: [make "-j%{jobs}%" "tpc"]
 depends: [
   "ocaml" {>= "4.05.0"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}

coq-disel.opam

@@ -19,9 +19,9 @@ from implementation details."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-mathcomp-ssreflect" {>= "1.13"}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "2.0"}
   "coq-fcsl-pcm" {>= "1.7.0"}
   "coq-htt" {>= "1.2.0"}
 ]

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name disel)

meta.yml

@@ -46,9 +46,13 @@ supported_coq_versions:
   opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: '1.15.0-coq-8.16'
+- version: '1.19.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.17.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
@@ -64,9 +68,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.13"}'
+    version: '{>= "1.13" & < "2.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices)
+    [MathComp](https://math-comp.github.io) 1.13.0 to 1.19.0 (`ssreflect` suffices)
 - opam:
     name: coq-fcsl-pcm
     version: '{>= "1.7.0"}'