diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 28a63e62..d3a1b945 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/.travis.yml b/.travis.yml index 8e317cea..a1924c24 100644 --- a/.travis.yml +++ b/.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 diff --git a/README.md b/README.md index f698539c..b30910e4 100644 --- a/README.md +++ b/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) diff --git a/coq-monae.opam b/coq-monae.opam index 2cd08e14..acac5ab5 100644 --- a/coq-monae.opam +++ b/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 " -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~" } ] diff --git a/meta.yml b/meta.yml index 40ef8092..5419088c 100644 --- a/meta.yml +++ b/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