Support Rocq 9.1 and 9.2#226
Open
spitters wants to merge 2 commits into
Open
Conversation
Lift the coq version bound to < 9.3~ and add Rocq 9.1 and 9.2 to the CI matrix. Also re-sync meta.yml with the generated opam/CI files: the supported bound was stale (< 8.20~) and the tested-Rocq list was missing. Requires a Rocq 9.2-compatible coq-math-classes release. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rocq 9.2 drops the `coq` and `coq-elpi` compatibility opam packages (coq-elpi 3.4.0 pulls coq-core, capped at 9.1.1). Depend on rocq-core and rocq-elpi for 9.x, keeping coq/coq-elpi for 8.18-8.20, following the coq-community/tarjan and fourcolor pattern. Also accept rocq-math-classes. The CoRN 9.2 CI job needs a Rocq 9.2 coq-math-classes in coq-released. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
SkySkimmer
reviewed
Jul 11, 2026
| # Rocq 9.2 drops the `coq` compatibility opam package, so the compiler and | ||
| # elpi dependencies are hand-written as disjunctions (coq/rocq-core, | ||
| # coq-elpi/rocq-elpi) in coq-corn.opam; this field is kept for reference. | ||
| opam: '{>= "8.19" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}' |
Contributor
There was a problem hiding this comment.
I think you still need coq-core (contains the coqc etc binaries)
Collaborator
Author
|
Waiting for rocq-prover/opam#3772 |
Contributor
|
|coq-core| has no 9.2 release (capped at 9.1.1), so |coqc|/|coq_makefile| come from |rocq-core| on 9.2
this is incorrect
Gaëtan Gilbert
…On 2026-07-11 14:32, Bas Spitters wrote:
***@***.**** commented on this pull request.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
In meta.yml <#226 (comment)>:
> @@ -81,8 +81,11 @@ license:
identifier: GPL-2.0
supported_coq_versions:
- text: Coq 8.19 or greater
- opam: '{(>= "8.19" & < "9.3~") | (= "dev")}'
+ text: Coq 8.19 to 8.20 or Rocq 9.0 to 9.2
+ # Rocq 9.2 drops the `coq` compatibility opam package, so the compiler and
+ # elpi dependencies are hand-written as disjunctions (coq/rocq-core,
+ # coq-elpi/rocq-elpi) in coq-corn.opam; this field is kept for reference.
+ opam: '{>= "8.19" & < "8.21~"} | "rocq-core" {(>= "9.0" & < "9.3~") | (= "dev")}'
Same as on the math-classes PR: |coq-core| has no 9.2 release (capped at 9.1.1), so |coqc|/|coq_makefile| come from |rocq-core| on 9.2. For CoRN the elpi dep also has to move to |rocq-elpi| on 9.2 (|coq-elpi| 3.4.0 pulls the now-unavailable |coq-core|). Verified downstream once a 9.2 |coq-math-classes| is in coq-released.
—
Reply to this email directly, view it on GitHub <#226?email_source=notifications&email_token=AASZB3CCAA37XE5WQWHOYHD5EIXVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTINRXG43TOOJWGY4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLDGN5XXIZLSL5RWY2LDNM#discussion_r3564154027>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AASZB3BVROTPO4NQHXPHNFL5EIXVXAVCNFSNUABDKJSXA33TNF2G64TZHMYTSMRYGIZDSO2JONZXKZJ3GQ4DMMRQGQYTCMZRUF3AE>.
Triage notifications, keep track of coding agent tasks and review pull requests on the go with GitHub Mobile for iOS <https://github.com/notifications/mobile/ios/AASZB3EBBQBV2VDWB7TX6KL5EIXVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTINRXG43TOOJWGY4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJKTGN5XXIZLSL5UW64Y> and Android <https://github.com/notifications/mobile/android/AASZB3ECLK2BI6N5OLF34L35EIXVXA5CNFSNUABKM5UWIORPF5TWS5BNNB2WEL2QOVWGYUTFOF2WK43UKJSXM2LFO4XTINRXG43TOOJWGY4KM4TFMFZW63VHMNXW23LFNZ2KKZLWMVXHJLTGN5XXIZLSL5QW4ZDSN5UWI>. Download it today!
You are receiving this because you commented.Message ID: ***@***.***>
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds compatibility with the Rocq 9.1 and 9.2 releases, a prerequisite for cutting a
9.2.0release of CoRN.Changes
meta.yml/coq-corn.opam: lift the coq bound from< "9.1~"to< "9.3~"..github/workflows/docker-action.yml: addrocq/rocq-prover:9.1androcq/rocq-prover:9.2to the CI matrix.meta.ymlwith the committed generated files:supported_coq_versionswas stale (< "8.20~") and thetested_rocq_opam_versionslist (dev/9.0) was missing, someta.ymlhad drifted fromcoq-corn.opam/ the CI workflow. Now regenerable.The bound goes to
< "9.3~"(rather than< "9.2~") since master already carries adaptations for post-9.2 dev changes (e.g. the adaptation to rocq-prover/rocq#21849, milestone 9.3); the new CI rows verify the 9.1 and 9.2 stable releases.Depends on
coq-math-classesmust be released tocoq-releasedbefore CoRN can resolve against it on 9.2.Follow-up (not in this PR)
Once CI is green on 9.2, cut a
9.2.0tag and submitcoq-corn.9.2.0to the opam archive.🤖 Generated with Claude Code