From eae4dc4fcd10b42977130fc3595b64100b57adb3 Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Wed, 18 Dec 2024 11:55:50 +0100 Subject: [PATCH] update ssr upper bounds --- .github/workflows/docker-action.yml | 2 +- README.md | 4 ++-- coq-htt-core.opam | 4 ++-- coq-htt.opam | 4 ++-- meta.yml | 8 ++++---- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index e02d2c0..cb1399b 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -16,7 +16,7 @@ jobs: matrix: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - - 'mathcomp/mathcomp:2.2.0-coq-8.20' + - 'mathcomp/mathcomp:2.3.0-coq-8.20' - 'mathcomp/mathcomp:latest-coq-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 8213b20..3d79121 100644 --- a/README.md +++ b/README.md @@ -41,11 +41,11 @@ that HTT implements Separation logic as a shallow embedding in Coq. - License: [Apache-2.0](LICENSE) - Compatible Coq versions: Coq 8.19 to 8.20 - Additional dependencies: - - [MathComp ssreflect 2.2](https://math-comp.github.io) + - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm) - - [Dune](https://dune.build) 2.5 or later + - [Dune](https://dune.build) 3.6 or later - Coq namespace: `htt` - Related publication(s): - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331) diff --git a/coq-htt-core.opam b/coq-htt-core.opam index 1a20705..74837d7 100644 --- a/coq-htt-core.opam +++ b/coq-htt-core.opam @@ -3,7 +3,7 @@ opam-version: "2.0" maintainer: "fcsl@software.imdea.org" -version: "dev" +version: "2.0.1" homepage: "https://github.com/imdea-software/htt" dev-repo: "git+https://github.com/imdea-software/htt.git" @@ -35,7 +35,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") } diff --git a/coq-htt.opam b/coq-htt.opam index 7b19b3b..56ea4f2 100644 --- a/coq-htt.opam +++ b/coq-htt.opam @@ -1,6 +1,6 @@ opam-version: "2.0" maintainer: "fcsl@software.imdea.org" -version: "dev" +version: "2.0.1" homepage: "https://github.com/imdea-software/htt" dev-repo: "git+https://github.com/imdea-software/htt.git" @@ -32,7 +32,7 @@ build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") } diff --git a/meta.yml b/meta.yml index b8388ff..63d75fc 100644 --- a/meta.yml +++ b/meta.yml @@ -72,7 +72,7 @@ maintainers: opam-file-maintainer: fcsl@software.imdea.org -opam-file-version: dev +opam-file-version: 2.0.1 license: fullname: Apache-2.0 @@ -86,7 +86,7 @@ supported_coq_versions: tested_coq_opam_versions: - version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' -- version: '2.2.0-coq-8.20' +- version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' - version: 'latest-coq-dev' repo: 'mathcomp/mathcomp' @@ -94,9 +94,9 @@ tested_coq_opam_versions: dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }' + version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }' description: |- - [MathComp ssreflect 2.2](https://math-comp.github.io) + [MathComp ssreflect 2.2-2.3](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra description: |-