From f2e5897a43f982c8ec562fe65c9892bdc4aec085 Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Tue, 6 May 2025 12:28:51 +0200 Subject: [PATCH] adapting docker images to mathcomp 2.4 and hieararchy builder 1.9 --- .github/workflows/docker-action.yml | 1 + README.md | 3 ++- coq-htt-core.opam | 6 +++--- coq-htt.opam | 4 ++-- meta.yml | 12 ++++++++++-- 5 files changed, 18 insertions(+), 8 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 23287ab..2aaf380 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,6 +19,7 @@ jobs: image: - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.3.0-coq-8.20' + - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0' - 'mathcomp/mathcomp-dev:rocq-prover-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 5e92ee4..1099810 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,8 @@ that HTT implements Separation logic as a shallow embedding in Coq. - License: [Apache-2.0](LICENSE) - Compatible Coq versions: 8.19 or later - Additional dependencies: - - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io) + - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) + - [MathComp ssreflect 2.2 or later](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) - [FCSL-PCM 2.1](https://github.com/imdea-software/fcsl-pcm) diff --git a/coq-htt-core.opam b/coq-htt-core.opam index 8182418..2d78443 100644 --- a/coq-htt-core.opam +++ b/coq-htt-core.opam @@ -31,12 +31,12 @@ variables). The connection reconciles dependent types with effects of state and establishes Separation logic as a type theory for such effects. In implementation terms, it means that HTT implements Separation logic as a shallow embedding in Coq.""" -build: [make "-C" "htt" "-j%{jobs}%"] -install: [make "-C" "htt" "install"] +build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "3.6"} "coq" { (>= "8.19" & < "9.1~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq-hierarchy-builder" { (>= "1.7.0" & < "1.10~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } diff --git a/coq-htt.opam b/coq-htt.opam index 4265e46..bb0c93a 100644 --- a/coq-htt.opam +++ b/coq-htt.opam @@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"] install: [make "-C" "examples" "install"] depends: [ "dune" {>= "3.6"} - "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") } + "coq" { (>= "8.19" & < "9.1~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") } "coq-mathcomp-algebra" "coq-mathcomp-fingroup" "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") } diff --git a/meta.yml b/meta.yml index 74003c1..da7bebe 100644 --- a/meta.yml +++ b/meta.yml @@ -88,15 +88,23 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.3.0-coq-8.20' repo: 'mathcomp/mathcomp' +- version: '2.4.0-rocq-prover-9.0' + repo: 'mathcomp/mathcomp' - version: 'rocq-prover-dev' repo: 'mathcomp/mathcomp-dev' + dependencies: +- opam: + name: coq-hierarchy-builder + version: '{ (>= "1.7.0" & < "1.10~") | (= "dev") }' + description: |- + [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder) - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }' + version: '{ (>= "2.2.0" & < "2.5~") | (= "dev") }' description: |- - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io) + [MathComp ssreflect 2.2 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra description: |-