fix(rivet): correct FEAT-001 -- Coq-Interval is not actually usable - #44
Closed
avrabe wants to merge 1 commit into
Closed
fix(rivet): correct FEAT-001 -- Coq-Interval is not actually usable#44avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
PR #43 reported (and I independently reproduced/deepened) that Require Import Interval.Tactic fails: #41 fetched coqPackages.interval but never wired its real dependency closure (bignums, mathcomp-boot, mathcomp-fingroup, and transitively hierarchy-builder + the coq-elpi OCaml plugin). FEAT-001 and REQ-002 previously claimed this was done; demoting both back to draft/approved until it's genuinely fixed and covered by a CI target that exercises Interval.Tactic, not just fetches the package. Adds DD-003: the verified fix is coq_9_0.withPackages(...), which resolves the whole transitive closure (confirmed: its coqc compiles a Require Import Interval.Tactic smoke proof cleanly, which no amount of manual nixpkgs_package + -Q wiring reached). Left as a draft design decision for the follow-up PR, not implemented here. Refs #43 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey
Contributor
Author
|
Superseded by #43 — that PR now contains this correction (FEAT-001/REQ-002 demoted, DD-003 added) plus the actual fix (a working `coq_9_0.withPackages` environment + `rocq_interval_proof` rule + a real `Require Import Interval.Tactic` smoke test, verified PASSED). Closing this one rather than merging two PRs that both rewrite the same rivet artifacts. 🤖 Generated with Claude Code |
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.
Summary
PR #43 reported (and I independently reproduced/deepened) that
Require Import Interval.Tacticfails: #41 fetchedcoqPackages.intervalbut never wired its real dependency closure (bignums, mathcomp-boot, mathcomp-fingroup, and transitively hierarchy-builder + the coq-elpi OCaml plugin — see the PR #43 review comment for the full trace).FEAT-001 and REQ-002 previously claimed this capability was
implemented. Demoting both back todraft/approveduntil it's genuinely fixed and covered by a CI target that exercisesInterval.Tactic, not just fetches the package — this is the same claim-honesty discipline as #42, applied to a rivet artifact instead of a README.Adds DD-003: the verified fix is
coq_9_0.withPackages(...), which resolves the whole transitive closure automatically (confirmed empirically — itscoqccompiles aRequire Import Interval.Tacticsmoke proof cleanly, which no amount of manualnixpkgs_package+-Qwiring reached). Left as a draft design decision for the follow-up PR that actually implements the fix — not implemented in this PR.Test plan
rivet validate— PASS (same warning baseline as before)Refs #43
🤖 Generated with Claude Code
https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey