From 13cb49cb3376bb036c59ec8f67d2020aff23a0dd Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 26 Oct 2023 12:51:50 +0200 Subject: [PATCH] Update CI --- .github/workflows/docker-action.yml | 5 +++++ README.md | 2 +- coq-mathcomp-algebra-tactics.opam | 2 +- meta.yml | 10 +++++++++- 4 files changed, 16 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 43d2629..678e264 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -20,6 +20,10 @@ jobs: - 'mathcomp/mathcomp:2.0.0-coq-8.16' - 'mathcomp/mathcomp:2.0.0-coq-8.17' - 'mathcomp/mathcomp:2.0.0-coq-8.18' + - 'mathcomp/mathcomp:2.0.0-coq-8.16' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.1.0-coq-dev' - 'mathcomp/mathcomp-dev:coq-8.16' - 'mathcomp/mathcomp-dev:coq-8.17' - 'mathcomp/mathcomp-dev:coq-8.18' @@ -40,6 +44,7 @@ jobs: if: ${{ always() }} run: sudo chown -R 1001:116 . + # See also: # https://github.com/coq-community/docker-coq-action#readme # https://github.com/erikmd/docker-coq-github-action-demo diff --git a/README.md b/README.md index 14c9da4..f187c59 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, -like the `add Ring` and `Add Field` commands. Therefore, each of these tactics +like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., `int * R` where `R` is an abstract diff --git a/coq-mathcomp-algebra-tactics.opam b/coq-mathcomp-algebra-tactics.opam index 3991b57..10eed5c 100644 --- a/coq-mathcomp-algebra-tactics.opam +++ b/coq-mathcomp-algebra-tactics.opam @@ -16,7 +16,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, -like the `add Ring` and `Add Field` commands. Therefore, each of these tactics +like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., `int * R` where `R` is an abstract diff --git a/meta.yml b/meta.yml index a2db58e..11c57cf 100644 --- a/meta.yml +++ b/meta.yml @@ -13,7 +13,7 @@ description: |- the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, - like the `add Ring` and `Add Field` commands. Therefore, each of these tactics + like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., `int * R` where `R` is an abstract @@ -52,6 +52,14 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' +- version: '2.0.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '2.1.0-coq-dev' + repo: 'mathcomp/mathcomp' - version: 'coq-8.16' repo: 'mathcomp/mathcomp-dev' - version: 'coq-8.17'