From c2ded97b6ab4d91c765ca57d3e30eb6f71808572 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sat, 11 Jul 2026 13:36:55 +0200 Subject: [PATCH 1/3] Support Rocq 9.1 and 9.2 Lift the coq version bound to < 9.3~ and add Rocq 9.1 and 9.2 to the CI matrix. Regenerated files kept in sync with meta.yml. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/docker-action.yml | 2 ++ coq-math-classes.opam | 2 +- meta.yml | 4 +++- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 25e9898..2fffbe1 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -21,6 +21,8 @@ jobs: - 'coqorg/coq:8.19' - 'coqorg/coq:8.18' - 'rocq/rocq-prover:dev' + - 'rocq/rocq-prover:9.2' + - 'rocq/rocq-prover:9.1' - 'rocq/rocq-prover:9.0' fail-fast: false steps: diff --git a/coq-math-classes.opam b/coq-math-classes.opam index 2dfd230..a44fa6e 100644 --- a/coq-math-classes.opam +++ b/coq-math-classes.opam @@ -30,7 +30,7 @@ build: [ ] install: [make "install"] depends: [ - "coq" {(>= "8.18" & < "9.1~") | (= "dev")} + "coq" {(>= "8.18" & < "9.3~") | (= "dev")} "coq-bignums" ] diff --git a/meta.yml b/meta.yml index c14301c..a390029 100644 --- a/meta.yml +++ b/meta.yml @@ -52,10 +52,12 @@ license: supported_coq_versions: text: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions) - opam: '{(>= "8.18" & < "9.1~") | (= "dev")}' + opam: '{(>= "8.18" & < "9.3~") | (= "dev")}' tested_rocq_opam_versions: - version: dev +- version: "9.2" +- version: "9.1" - version: "9.0" tested_coq_opam_versions: From adab5559697e3adc060a45fbb6caf9a569e43719 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sat, 11 Jul 2026 14:18:00 +0200 Subject: [PATCH 2/3] opam: depend on rocq-core for Rocq 9.x (fix 9.2 resolution) Rocq 9.2 drops the `coq` compatibility opam package, so `depends: coq` is unsatisfiable there. Depend on `rocq-core` for 9.x (keeping `coq` for 8.18-8.20), following the coq-community/tarjan and fourcolor pattern. coq-bignums already ships a +rocq9.2 build, so it is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- coq-math-classes.opam | 5 +++-- meta.yml | 7 +++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/coq-math-classes.opam b/coq-math-classes.opam index a44fa6e..559f134 100644 --- a/coq-math-classes.opam +++ b/coq-math-classes.opam @@ -30,8 +30,9 @@ build: [ ] install: [make "install"] depends: [ - "coq" {(>= "8.18" & < "9.3~") | (= "dev")} - "coq-bignums" + ("coq" {>= "8.18" & < "8.21~"} + | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}) + "coq-bignums" ] tags: [ diff --git a/meta.yml b/meta.yml index a390029..b335a55 100644 --- a/meta.yml +++ b/meta.yml @@ -51,8 +51,11 @@ license: identifier: MIT supported_coq_versions: - text: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions) - opam: '{(>= "8.18" & < "9.3~") | (= "dev")}' + text: Coq 8.18 to 8.20 or Rocq 9.0 to 9.2 (use releases for other Coq/Rocq versions) + # The coq-core/rocq-core split (Rocq 9.2 drops the `coq` compatibility + # package) means the compiler dependency must be hand-written as a + # disjunction in coq-math-classes.opam; this field is kept for reference. + opam: '{>= "8.18" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}' tested_rocq_opam_versions: - version: dev From 03d6b903c82b7c8c5cb8fc0de68b3dcc878b85b9 Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Sat, 11 Jul 2026 14:31:41 +0200 Subject: [PATCH 3/3] opam: allow Rocq 9.3 (< 9.4~) per review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 9.3 is branched and does not break math-classes (Gaëtan Gilbert), so extend the rocq-core bound to < 9.4~. --- coq-math-classes.opam | 2 +- meta.yml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/coq-math-classes.opam b/coq-math-classes.opam index 559f134..45d1310 100644 --- a/coq-math-classes.opam +++ b/coq-math-classes.opam @@ -31,7 +31,7 @@ build: [ install: [make "install"] depends: [ ("coq" {>= "8.18" & < "8.21~"} - | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}) + | "rocq-core" {(>= "9.0" & < "9.4~") | (= "dev")}) "coq-bignums" ] diff --git a/meta.yml b/meta.yml index b335a55..572fa6a 100644 --- a/meta.yml +++ b/meta.yml @@ -51,11 +51,11 @@ license: identifier: MIT supported_coq_versions: - text: Coq 8.18 to 8.20 or Rocq 9.0 to 9.2 (use releases for other Coq/Rocq versions) + text: Coq 8.18 to 8.20 or Rocq 9.0 to 9.3 (use releases for other Coq/Rocq versions) # The coq-core/rocq-core split (Rocq 9.2 drops the `coq` compatibility # package) means the compiler dependency must be hand-written as a # disjunction in coq-math-classes.opam; this field is kept for reference. - opam: '{>= "8.18" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}' + opam: '{>= "8.18" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.4~") | (= "dev")}' tested_rocq_opam_versions: - version: dev