Adapt to Rocq 9.4 and MathComp dev - #1
Merged
Conversation
Three unrelated breakages against Rocq 9.4+alpha / mathcomp dev: * Rocq now reserves `of` as a keyword (`constructor_binders` in g_vernac.mlg, "Add \"of _ & _ & _\" syntax for constructors"). coq-elpi parses HB's `of` clause as `IDENT "of"`, which no longer matches, so every `HB.mixin Record ... of ...`, `HB.factory Record ... of ...` and `HB.builders Context ... of ...` fails with a bare "Usage:" message. Use the equivalent `&` spelling, which is the form the HB usage message itself documents and works on older versions too. * mathcomp split its ring hierarchy: `SemiRing` no longer carries `1 != 0`, the nontrivial variant is `NzSemiRing`. Rename SemiRing -> NzSemiRing, ComSemiRing -> ComNzSemiRing, isSemiRing -> isNzSemiRing, SubSemiRing -> SubNzSemiRing, SubChoice_isSub[Com]SemiRing -> SubChoice_isSub[Com]NzSemiRing and SubSemiRing_isSubComSemiRing -> SubNzSemiRing_isSubComNzSemiRing, preserving the previous meaning of the dioid structures. * mathcomp's ssrfun now reserves `x ^*` at level 1 with left associativity; match that reservation instead of level 2. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
force-pushed
the
claude/rocq-dev-compat
branch
from
July 28, 2026 05:59
737c439 to
67e0565
Compare
Collaborator
|
@JasonGross I do prefer the proof script reordering to the use of SsrOldRewriteGoalsOrder. It's fine to bump the lower bound on MathComp to >= 2.6 |
Contributor
Author
|
Thanks — I updated this accordingly:
The follow-up commits are 4b6c6de and c52d2b4.
|
JasonGross
force-pushed
the
claude/rocq-dev-compat
branch
from
July 31, 2026 21:26
3469d50 to
c52d2b4
Compare
JasonGross
added a commit
to theorem-labs/opam
that referenced
this pull request
Jul 31, 2026
The dev sources use the MathComp 2.6 Nz* semiring hierarchy, so 2.4~ is too low. Matches the bound agreed upstream in math-comp/dioid#1. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
JasonGross
added a commit
to theorem-labs/opam
that referenced
this pull request
Jul 31, 2026
The dev sources use the MathComp 2.6 Nz* semiring hierarchy, so 2.4~ is too low. Matches the bound agreed upstream in math-comp/dioid#1. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
proux01
force-pushed
the
claude/rocq-dev-compat
branch
3 times, most recently
from
August 21, 2026 10:54
34b0d89 to
aef0450
Compare
MathComp 2.5.0's mathcomp/boot/ssreflect.v carried `Global Set SsrOldRewriteGoalsOrder.`; mathcomp dev (2.6+, PR #1545) removed it, so the Rocq option reverts to its default and the side condition produced by `rewrite (_ : A = B)` is now left as the FIRST goal instead of the last. That is what the `; last first.` idiom in these proofs was compensating for. This is a mathcomp change, not a Rocq one: the flag itself is permanent and undeprecated. Swap the idiom at each of the five affected sites -- drop `; last first.` where it was present and add it where it was not -- leaving the proof scripts themselves untouched. With only five sites this is cheaper than adding a per-file `Set SsrOldRewriteGoalsOrder.`, and it is step (2) of the ladder mathcomp's own 2.6.0 CHANGELOG describes, so it does not have to be undone later. The cost is that the file now requires mathcomp >= 2.6, which the opam bounds state. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
proux01
force-pushed
the
claude/rocq-dev-compat
branch
from
August 21, 2026 11:14
aef0450 to
1946231
Compare
proux01
marked this pull request as ready for review
August 21, 2026 11:25
Collaborator
|
@JasonGross thanks for the PR and sorry for the delayed merge Do you need a release? |
Contributor
Author
|
No release necessary |
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.
Adapts Dioid to Rocq 9.4+alpha and MathComp development: updates Hierarchy Builder for the reserved
ofkeyword, follows the nontrivialNz*semiring split, aligns^*with current ssrfun, adjusts conditional-rewrite proofs, and relaxes opam bounds.Validated with:
opam exec --switch=rocq-dev-testing -- make -j4The complete build succeeds. This remains a draft because one commit targets current development rewrite-goal ordering and should be revisited if it changes before release.
Claude Opus 5 implemented the changes; the commits retain session attribution and co-authorship trailers.
Wordsmithed by Codex.