From 14ba0f7fea567fbbadfcad206ed58e2c5c391dd8 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 28 Mar 2024 16:46:06 +0100 Subject: [PATCH 1/2] Adapt to math-comp/math-comp#1190 --- src/spec/operations/properties.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/spec/operations/properties.v b/src/spec/operations/properties.v index b70e083..f7ae2dc 100644 --- a/src/spec/operations/properties.v +++ b/src/spec/operations/properties.v @@ -1972,7 +1972,7 @@ Section Structures. Variable n:nat. -HB.instance Definition _ := Finite.copy (BITS n) [finType of BITS n]. +HB.instance Definition _ := Finite.on (BITS n). HB.instance Definition _ := GRing.isZmodule.Build (BITS n) (@addBA n) (@addBC n) (@add0B n) (@addBN n). HB.instance Definition _ := isMulGroup.Build (BITS n) From 5429b8806dd532b22a5b5fc07a0cd0229fdbb45a Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 28 Mar 2024 16:47:51 +0100 Subject: [PATCH 2/2] Update CI --- .github/workflows/docker-action.yml | 11 ++++++++--- coq-bits.opam | 4 ++-- meta.yml | 22 ++++++++++++++++------ 3 files changed, 26 insertions(+), 11 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index e80ef3c..b47e71f 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,11 +17,16 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.0.0-coq-8.16' - 'mathcomp/mathcomp:2.0.0-coq-8.18' - - 'mathcomp/mathcomp:2.1.0-coq-8.17' - 'mathcomp/mathcomp:2.1.0-coq-8.16' - - 'mathcomp/mathcomp:2.0.0-coq-8.16' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.16' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' + - 'mathcomp/mathcomp:2.2.0-coq-dev' + - 'mathcomp/mathcomp-dev:coq-8.17' + - 'mathcomp/mathcomp-dev:coq-8.19' + - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: - uses: actions/checkout@v3 diff --git a/coq-bits.opam b/coq-bits.opam index 2db0cec..167fd5f 100644 --- a/coq-bits.opam +++ b/coq-bits.opam @@ -18,9 +18,9 @@ axiomatization and extraction to OCaml native integers.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.16" & < "8.19~")} + "coq" {(>= "8.16" & < "8.20~") | (= "dev")} "ocamlbuild" - "coq-mathcomp-algebra" {(>= "2.0" & < "2.2~")} + "coq-mathcomp-algebra" {(>= "2.0" & < "2.3~") | (= "dev")} ] tags: [ diff --git a/meta.yml b/meta.yml index 875f156..5873306 100644 --- a/meta.yml +++ b/meta.yml @@ -48,19 +48,29 @@ license: supported_coq_versions: text: 8.16 or later (use releases for other Coq versions) - opam: '{(>= "8.16" & < "8.19~")}' + opam: '{(>= "8.16" & < "8.20~") | (= "dev")}' tested_coq_opam_versions: -- version: '2.1.0-coq-8.18' +- version: '2.0.0-coq-8.16' repo: 'mathcomp/mathcomp' - version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '2.1.0-coq-8.17' - repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '2.0.0-coq-8.16' +- version: '2.1.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-8.19' + repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-dev' repo: 'mathcomp/mathcomp' +- version: 'coq-8.17' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.19' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-dev' + repo: 'mathcomp/mathcomp-dev' dependencies: - opam: @@ -68,7 +78,7 @@ dependencies: description: OCamlbuild - opam: name: coq-mathcomp-algebra - version: '{(>= "2.0" & < "2.2~")}' + version: '{(>= "2.0" & < "2.3~") | (= "dev")}' description: |- [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices)