Add min-dclr snapshot review skill - #10
Open
junekim623 wants to merge 13 commits into
Open
Conversation
meta-cla
Bot
added
the
CLA Signed
junekim623
changed the title
junekim623
changed the title
Address review feedback on the declaration-closure CLI. Links: a nested Lean root produced GitHub URLs missing the repository prefix, so every link 404'd. Carry the prefix on ClosureReport and apply it to urls while paths stay relative to the Lean root. Snapshot scope: git status always reports the whole repository, so unrelated work elsewhere in a monorepo marked the snapshot dirty and suppressed all links. Scope the check to the Lean root. Private roots: Lean mangles private names, so looking roots up by the name the caller typed raised an uncaught KeyError. Match on the display name and fail with a DeclarationClosureError when a root is unresolved. Base revision: a two-dot diff against a branch tip reported base-branch commits as changes. Resolve --base through its merge base with HEAD. Deletions: only added diff lines were considered, so removing a structure field left it out of the "exact" closure. Attribute zero-added-line hunks to the declarations on either side of the seam. Axioms: an introduced axiom landed in neither definitions nor theorems and vanished from the checklist. Report it as reviewable. Also read untracked files with --full-name so they match the repository-relative paths git diff reports, accept ? and ! in Lean names, escape non-identifier name components in the generated driver, and skip the redundant source scan when building links.
The command ran `lake build` and only then asked whether the checkout was dirty, so an artifact it had just generated — a regenerated lake-manifest.json — marked the snapshot uncommitted and suppressed every permalink. The tool degraded its own output. Read the snapshot before the build, and judge it on *.lean sources alone. A link addresses one line in one source file, so a rebuilt manifest, a regenerated site, or work on another project in the same repository cannot move it. Decide pinning per declaration rather than per snapshot. A url is emitted whenever that declaration's own file matches HEAD, so a review taken mid-edit keeps immutable links for every untouched file instead of losing all of them; dirty still reports the overall snapshot for labeling. Reuse the ignored-directory set that index_project already applies, so vendored sources under .lake cannot dirty a snapshot in projects that do not gitignore them.
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
min-dclrskill that refreshes a complete source-to-Lean review checklist on demandautoform declaration-closure, a deterministic CLI backed by Lean's elaborated constant environmentdefinitionsorder for the agent to preserve in the review$min-dclrthrough Codex,/autoform:min-dclrthrough Claude Code, andmin-dclrthrough MuseTest plan
uv run --extra dev pytest -q tests/test_declaration_closure.py tests/test_lean_sources.py tests/test_skill_examples.py::test_min_dclr_refreshes_the_current_snapshot tests/test_plugin_runtime.py(26 passed)uv run autoform declaration-closure --helpCabannesThesis.supervision_nonAmbiguous)fairinternal/formal-math: 29 roots, 153 reachable changed declarations, 122 non-root definitions, and 567 dependency edges; verified duplicate-name resolution linksisQuasicoherent_kernelto its imported production modulemake lintmake check-examplequick_validate.py skills/min-dclrvalidate_plugin.py .make test(540 passed, 1 skipped; the unrelatedtest_cas_acquire_race_has_exactly_one_winnerfails under the local Git environment)