reassemble: dependency-aware deletion, per-unit neighbour pruning, combo audit - #31
Merged
Merged
Conversation
…mbo audit Audit every lean_reassemble parameter combination and make each either well-defined or explicitly rejected — never a silent wrong/misleading result. Behavior: - Add a shared dependency-conflict detector (Rewrite.lean: deletedNames / danglingReferences / dependencyConflictMessage) over records' direct `deps`. materialize-repo and materialize-units now fail fast — naming each `dependent -> deleted` pair — when a surviving declaration would be left referencing a deleted theorem, instead of an opaque `lake` break (or, under a scoped --build-target, a false "passed"). A `sorry` dependent is correctly treated as safe (its references are holed out). - materialize-units: a manifest `delete` on a same-module neighbour now removes that declaration from each unit's file (target still holed, other neighbours kept), with the same conflict check scoped per module. A `keep` target is excluded with a warning, and a run that yields zero tasks (e.g. whole-run --proofs delete/keep) now fails instead of writing verification: passed over nothing. - Reject the inert --keep-eval / --in-process for materialize-units. Record the exact `lake build <target>` command in the repo manifest.json verification so a scoped verification is not mistaken for a whole-project one. Docs: reassemble/docs/parameter-matrix.md (the full spec), linked from the README; usage text updated. Tests: new TestProject/Fixture/Deps.lean + records-deps.jsonl (a real theorem->theorem edge the old fixtures lacked); pure danglingReferences tests, the three audit regressions, and units neighbour-pruning in ReassembleTests.lean.
ppotapov-aws
changed the title
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.
Audit every lean_reassemble parameter combination and make each either well-defined or explicitly rejected — never a silent wrong/misleading result.
Behavior:
deps. materialize-repo and materialize-units now fail fast — naming eachdependent -> deletedpair — when a surviving declaration would be left referencing a deleted theorem, instead of an opaquelakebreak (or, under a scoped --build-target, a false "passed"). Asorrydependent is correctly treated as safe (its references are holed out).deleteon a same-module neighbour now removes that declaration from each unit's file (target still holed, other neighbours kept), with the same conflict check scoped per module. Akeeptarget is excluded with a warning, and a run that yields zero tasks (e.g. whole-run --proofs delete/keep) now fails instead of writing verification: passed over nothing.lake build <target>command in the repo manifest.json verification so a scoped verification is not mistaken for a whole-project one.Docs: reassemble/docs/parameter-matrix.md (the full spec), linked from the README; usage text updated.
Tests: new TestProject/Fixture/Deps.lean + records-deps.jsonl (a real theorem->theorem edge the old fixtures lacked); pure danglingReferences tests, the three audit regressions, and units neighbour-pruning in ReassembleTests.lean.