diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 1079b603..966a3fc1 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,6 +19,10 @@ jobs: 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' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 3120962e..9e7150de 100644 --- a/README.md +++ b/README.md @@ -71,7 +71,7 @@ make install ## Acknowledgments -Many thanks to several contributors ([committers](https://github.com/affeldt-aist/infotheo/graphs/contributors)). +Many thanks to several [contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors). The principle of inclusion-exclusion is a contribution by Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) diff --git a/coq-infotheo.opam b/coq-infotheo.opam index 54993d4e..7a2af6ba 100644 --- a/coq-infotheo.opam +++ b/coq-infotheo.opam @@ -21,12 +21,12 @@ build: [ ] install: [make "install"] depends: [ - "coq" { (>= "8.13" & < "8.15~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.14~") | (= "dev") } - "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.14~") | (= "dev") } - "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.14~") | (= "dev") } - "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.14~") | (= "dev") } - "coq-mathcomp-field" { (>= "1.13.0" & < "1.14~") | (= "dev") } + "coq" { (>= "8.13" & < "8.16~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") } + "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") | (= "dev") } + "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") | (= "dev") } + "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev") } + "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")} ] diff --git a/meta.yml b/meta.yml index d7f3385f..cf2813f4 100644 --- a/meta.yml +++ b/meta.yml @@ -42,38 +42,46 @@ nix: true supported_coq_versions: text: Coq 8.13, Coq 8.14 - opam: '{ (>= "8.13" & < "8.15~") | (= "dev") }' + opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }' 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' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.13.0" & < "1.14~") | (= "dev") }' + version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }' description: |- [MathComp field](https://math-comp.github.io) - opam: