From de1b7cde445fc0cf090c1268babd8360bc7f24a7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 8 Jul 2022 08:07:49 +0200 Subject: [PATCH] [CI] Add Coq 8.16 and MC 1.15 --- .github/workflows/docker-action.yml | 12 +++++------- README.md | 2 +- coq-coqeal.opam | 4 ++-- meta.yml | 28 ++++++++++++---------------- 4 files changed, 20 insertions(+), 26 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index bb76ea0..a6f77b1 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,20 +17,18 @@ jobs: strategy: matrix: image: + - 'mathcomp/mathcomp:1.15.0-coq-8.16' + - 'mathcomp/mathcomp:1.15.0-coq-8.15' + - 'mathcomp/mathcomp:1.15.0-coq-8.14' + - 'mathcomp/mathcomp:1.15.0-coq-8.13' - 'mathcomp/mathcomp:1.14.0-coq-8.15' - 'mathcomp/mathcomp:1.14.0-coq-8.14' - 'mathcomp/mathcomp:1.14.0-coq-8.13' - - 'mathcomp/mathcomp:1.14.0-coq-8.12' - - 'mathcomp/mathcomp:1.14.0-coq-8.11' - 'mathcomp/mathcomp:1.13.0-coq-8.15' - 'mathcomp/mathcomp:1.13.0-coq-8.14' - 'mathcomp/mathcomp:1.13.0-coq-8.13' - - 'mathcomp/mathcomp:1.13.0-coq-8.12' - - 'mathcomp/mathcomp:1.13.0-coq-8.11' - 'mathcomp/mathcomp-dev:coq-dev' - - 'mathcomp/mathcomp-dev:coq-8.15' - - 'mathcomp/mathcomp-dev:coq-8.14' - - 'mathcomp/mathcomp-dev:coq-8.13' + - 'mathcomp/mathcomp-dev:coq-8.16' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index ce4b4f1..664c57c 100644 --- a/README.md +++ b/README.md @@ -44,7 +44,7 @@ of the ForMath EU FP7 project (2009-2013). It has two parts: - Cyril Cohen ([**@CohenCyril**](https://github.com/CohenCyril)) - Pierre Roux ([**@proux01**](https://github.com/proux01)) - License: [MIT License](LICENSE) -- Compatible Coq versions: 8.10 or later (use releases for other Coq versions) +- Compatible Coq versions: 8.13 or later (use releases for other Coq versions) - Additional dependencies: - [Bignums](https://github.com/coq/bignums) same version as Coq - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later diff --git a/coq-coqeal.opam b/coq-coqeal.opam index f5f8822..cf50a66 100644 --- a/coq-coqeal.opam +++ b/coq-coqeal.opam @@ -21,11 +21,11 @@ of the ForMath EU FP7 project (2009-2013). It has two parts: build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.10" & < "8.16~") | (= "dev")} + "coq" {(>= "8.13" & < "8.17~") | (= "dev")} "coq-bignums" "coq-paramcoq" {>= "1.1.3"} "coq-mathcomp-multinomials" {((>= "1.5.1" & < "1.7~") | = "dev")} - "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.15~") | = "dev")} + "coq-mathcomp-algebra" {((>= "1.13.0" & < "1.16~") | = "dev")} "coq-mathcomp-real-closed" {(>= "1.1.2" & < "1.2~") | (= "dev")} ] diff --git a/meta.yml b/meta.yml index a558883..7d32e75 100644 --- a/meta.yml +++ b/meta.yml @@ -68,8 +68,8 @@ license: identifier: MIT supported_coq_versions: - text: 8.10 or later (use releases for other Coq versions) - opam: '{(>= "8.10" & < "8.16~") | (= "dev")}' + text: 8.13 or later (use releases for other Coq versions) + opam: '{(>= "8.13" & < "8.17~") | (= "dev")}' dependencies: - opam: @@ -88,7 +88,7 @@ dependencies: [MathComp Multinomials](https://github.com/math-comp/multinomials) >= 1.5.1 and < 1.7 - opam: name: coq-mathcomp-algebra - version: '{((>= "1.13.0" & < "1.15~") | = "dev")}' + version: '{((>= "1.13.0" & < "1.16~") | = "dev")}' description: |- [MathComp algebra](https://math-comp.github.io) 1.13.0 or later - opam: @@ -98,33 +98,29 @@ dependencies: [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later tested_coq_opam_versions: +- version: '1.15.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.14' + repo: 'mathcomp/mathcomp' +- version: '1.15.0-coq-8.13' + repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.15' repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.14' repo: 'mathcomp/mathcomp' - version: '1.14.0-coq-8.13' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.12' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.11' - repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.15' repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.14' repo: 'mathcomp/mathcomp' - version: '1.13.0-coq-8.13' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.12' - repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.11' - repo: 'mathcomp/mathcomp' - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.15' - repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.14' - repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.13' +- version: 'coq-8.16' repo: 'mathcomp/mathcomp-dev' namespace: CoqEAL