Merge pull request #15 from coq-community/mathcomp-docker-images

Mathcomp docker images

Author: anton-trunov

.github/workflows/docker-action.yml

@@ -17,11 +17,11 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:8.10'
-          - 'coqorg/coq:8.11'
-          - 'coqorg/coq:8.12'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:dev'
+          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.10'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -42,7 +42,7 @@ axiomatization and extraction to OCaml native integers.
 - Compatible OCaml versions: 4.05 or later (not tested on previous versions)
 - Additional dependencies:
   - OCamlbuild
-  - [MathComp](https://math-comp.github.io) 1.7.0 or later (`algebra` suffices)
+  - [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices)
 - Coq namespace: `Bits`
 - Related publication(s):
   - [From Sets to Bits in Coq](https://hal.archives-ouvertes.fr/hal-01251943/document) doi:[10.1007/978-3-319-29604-3_2](https://doi.org/10.1007/978-3-319-29604-3_2)

coq-bits.opam

@@ -21,7 +21,7 @@ depends: [
   "ocaml" {(>= "4.05" & < "4.13~")}
   "coq" {(>= "8.10" & < "8.14~") | (= "dev")}
   "ocamlbuild" 
-  "coq-mathcomp-algebra" {(>= "1.7" & < "1.13~") | (= "dev")}
+  "coq-mathcomp-algebra" {(>= "1.12" & < "1.13~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -55,21 +55,26 @@ supported_coq_versions:
   opam: '{(>= "8.10" & < "8.14~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '8.10'
-- version: '8.11'
-- version: '8.12'
-- version: '8.13'
-- version: dev
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
+- version: '1.12.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.11'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.10'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: ocamlbuild
   description: OCamlbuild
 - opam:
     name: coq-mathcomp-algebra
-    version: '{(>= "1.7" & < "1.13~") | (= "dev")}'
+    version: '{(>= "1.12" & < "1.13~") | (= "dev")}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.7.0 or later (`algebra` suffices)
+    [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices)
 
 namespace: Bits