Adapt addition chains to Rocq dev - #181
Draft
JasonGross wants to merge 2 commits into
Draft
Conversation
The `< "1.19"` upper bound made coq-addition-chains the only unsolvable package in this repo on a mathcomp-dev switch: coq-addition-chains >= dev -> coq-mathcomp-ssreflect < 1.19 not available because the package is pinned to version dev With that one constraint ignored the solver plans a clean single-package install, so the cap was the sole solver-level block. The bound is stale rather than load-bearing: the port commit on this branch already makes theories/additions compile against mathcomp dev, and none of its repairs is a mathcomp 1.x -> 2.x API change. They are the stdlib removal of Even and Div2, the `_%type_scope` -> `_%_type_scope` argument-scope spelling, the `Equivalence`/`Reflexive`/`Symmetric`/ `Transitive` instance statements in Monoid_def.v, two proofs in each of Pow.v and Pow_variant.v, and one mathcomp 2.6 goal-order regression in fib.v. Cold build of this branch at The Rocq Prover 9.4+alpha with mathcomp dev, in a fresh tree with DUNE_CACHE=disabled: rc=0, 21 of 21 declared theories/additions files compiled, 0 Error lines. The floor moves to 2.0.0 to match coq-gaia-hydras.opam, the only other opam file in this repo that constrains ssreflect. Only `dev` was actually measured, so 2.0.0 is house consistency rather than a measured floor. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> 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.
Updates
coq-addition-chainsfor Rocq and MathComp development versions: restore the ssreflect rewrite-goal order expected byfib.v, remove retiredEvenandDiv2imports, targetequivexplicitly in relation-class instances, avoid fragile setoid rewriting in two power proofs, and update deprecatedArgumentsscope-delimiter syntax.The package build succeeds:
opam exec --switch=rocq-dev-testing -- dune build -p coq-addition-chains -j4Wordsmithed by Codex.