Restore historical ssreflect rewrite goal ordering - #76
Draft
JasonGross wants to merge 1 commit into
Draft
Conversation
Several proofs in this development use conditional ssreflect rewrites together with `last by` / `first by` / `last first`, which relies on the side conditions being produced after the main goal. MathComp <= 2.5.0 enabled `SsrOldRewriteGoalsOrder` globally in mathcomp/boot/ssreflect.v, so the option was on for us; MathComp dev no longer does, and the Rocq option reverts to its default (off), which reorders those goals and breaks the proofs in finmap.v, heaps.v, stmod.v and terms.v. Set the option explicitly in prelude.v, which every other file requires. The option exists in Rocq 9.0 through dev, so this stays backwards compatible; verified building with Rocq 9.0, 9.1, 9.2 and 9.4+alpha. Co-Authored-By: Claude Opus 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
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
1 participant
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.
MathComp dev no longer globally enables
SsrOldRewriteGoalsOrder, but several proofs in this development rely on the former conditional-rewrite goal ordering. Enable the option explicitly and globally inprelude.v, which is imported throughout the library.Validation: a clean
make -j8build completes successfully against Rocq dev and MathComp dev in therocq-dev-testingopam switch. The build emits deprecation warnings but no errors.The compatibility change was developed by a Claude coding-agent session and independently reviewed and validated by OpenAI Codex.