Compatibility mc112 (#34)

* test compilation with MathComp 1.12 and Analysis 0.3.5

.github/workflows/docker-action.yml

@@ -19,6 +19,8 @@ jobs:
         image:
           - 'mathcomp/mathcomp:1.11.0-coq-8.11'
           - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

.travis.yml

@@ -16,6 +16,8 @@ env:
   matrix:
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.12"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.12.0-coq-8.11"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.12.0-coq-8.12"
 
 install: |
   # Prepare the COQ container

README.md

@@ -27,14 +27,14 @@ in several examples of monadic equational reasoning.
 - License: [LGPL-2.1-or-later](LICENSE)
 - Compatible Coq versions: Coq 8.11 to 8.12
 - Additional dependencies:
-  - [MathComp ssreflect 1.11](https://math-comp.github.io)
-  - [MathComp fingroup 1.11](https://math-comp.github.io)
-  - [MathComp algebra 1.11](https://math-comp.github.io)
-  - [MathComp solvable 1.11](https://math-comp.github.io)
-  - [MathComp field 1.11](https://math-comp.github.io)
-  - [MathComp analysis 0.3.4](https://github.com/math-comp/analysis)
-  - [Infotheo 0.2.1](https://github.com/affeldt-aist/infotheo)
-  - [Paramcoq 0.1.2](https://github.com/coq-community/paramcoq)
+  - [MathComp ssreflect](https://math-comp.github.io)
+  - [MathComp fingroup](https://math-comp.github.io)
+  - [MathComp algebra](https://math-comp.github.io)
+  - [MathComp solvable](https://math-comp.github.io)
+  - [MathComp field](https://math-comp.github.io)
+  - [MathComp analysis](https://github.com/math-comp/analysis)
+  - [Infotheo](https://github.com/affeldt-aist/infotheo)
+  - [Paramcoq](https://github.com/coq-community/paramcoq)
 - Coq namespace: `monae`
 - Related publication(s):
   - [A hierarchy of monadic effects for program verification using equational reasoning](https://staff.aist.go.jp/reynald.affeldt/documents/monae.pdf) doi:[10.1007/978-3-030-33636-3_9](https://doi.org/10.1007/978-3-030-33636-3_9)

coq-monae.opam

@@ -1,9 +1,5 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "Reynald Affeldt <[email protected]>"
-version: "dev"
 
 homepage: "https://github.com/affeldt-aist/monae"
 dev-repo: "git+https://github.com/affeldt-aist/monae.git"
@@ -23,13 +19,13 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.11" & < "8.13~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") }
-  "coq-mathcomp-analysis" { (= "0.3.4") }
-  "coq-infotheo" { >= "0.2.1" }
+  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.13~") }
+  "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.13~") }
+  "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.13~") }
+  "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.13~") }
+  "coq-mathcomp-field" { (>= "1.11.0" & < "1.13~") }
+  "coq-mathcomp-analysis" { (>= "0.3.4" & < "0.4~") }
+  "coq-infotheo" { >= "0.2.1" & < "0.3~"}
   "coq-paramcoq" { >= "1.1.2" & < "1.2~" }
 ]
 

meta.yml

@@ -41,48 +41,52 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '1.11.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.11'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.11.0" & < "1.13~") }'
   description: |-
-    [MathComp ssreflect 1.11](https://math-comp.github.io)
+    [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.11.0" & < "1.13~") }'
   description: |-
-    [MathComp fingroup 1.11](https://math-comp.github.io)
+    [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.11.0" & < "1.13~") }'
   description: |-
-    [MathComp algebra 1.11](https://math-comp.github.io)
+    [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.11.0" & < "1.13~") }'
   description: |-
-    [MathComp solvable 1.11](https://math-comp.github.io)
+    [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.11.0" & < "1.12~") }'
+    version: '{ (>= "1.11.0" & < "1.13~") }'
   description: |-
-    [MathComp field 1.11](https://math-comp.github.io)
+    [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (= "0.3.4") }'
+    version: '{ (>= "0.3.4" & < "0.4~") }'
   description: |-
-    [MathComp analysis 0.3.4](https://github.com/math-comp/analysis)
+    [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.2.1" }'
+    version: '{ >= "0.2.1" & < "0.3~"}'
   description: |-
-    [Infotheo 0.2.1](https://github.com/affeldt-aist/infotheo)
+    [Infotheo](https://github.com/affeldt-aist/infotheo)
 - opam:
     name: coq-paramcoq
     version: '{ >= "1.1.2" & < "1.2~" }'
   description: |-
-    [Paramcoq 0.1.2](https://github.com/coq-community/paramcoq)
+    [Paramcoq](https://github.com/coq-community/paramcoq)
 
 namespace: monae