Repository navigation
Flag truncated files in partial-port audit - #114
Conversation
There was a problem hiding this comment.
Pull request overview
This PR improves the deterministic partial-port audit so it can detect “same file exists but is truncated” cases by matching imported/upstream files via a normalized relative path (dropping project-root prefixes), and it extends the audit finding output to report these truncated matches.
Changes:
- Add
normalize_relative_pathand use it inevaluate_statsto detect matched files whose imported LOC is below the tolerance. - Extend
AuditFindingwithtruncated_filesand include it in the formatted output. - Add tests covering Monlib-style root normalization and truncated matched files.
Fit: good_fit
Level: undergraduate
Branch: tooling / import-audit
Mode: theory_building
Obscure problem: false
Code quality: 4/5
Significance: Improves reliability of upstream-import auditing by catching a concrete partial-import failure mode where filename/stem matching alone misses truncation.
Verdict: request_changes
Findings:
evaluate_statscan raiseZeroDivisionErrorwhen computing per-file truncation ratios for upstream files withloc == 0.normalize_relative_pathdocstring example does not match the current behavior (it drops the upstream leading component too).
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| python/lean_pool/partial_port_audit.py | Add normalized-path matching and truncated-file reporting to the partial-port audit. |
| python/tests/test_partial_port_audit.py | Add coverage for project-root normalization and truncated matched-file detection. |
| matching_imports = imported_by_path.get(normalize_relative_path(file.path), []) | ||
| if not matching_imports: | ||
| continue | ||
| imported_file = max(matching_imports, key=lambda item: item.loc) |
| usually live under the upstream root module. Dropping those leading project | ||
| components lets ``LeanPool/Foo/Bar/Baz.lean`` match ``Foo/Bar/Baz.lean``. |
Summary\n- add same-file normalized path matching to the deterministic partial-port audit\n- report files whose imported LOC is outside the tolerance even when the filename exists\n- add tests covering Monlib-style project-root normalization and truncated matched files\n\n## Verification\n- uv run --group test pytest\n- uv run ruff check\n- uv run ruff format --check\n- git diff --check\n\nThis catches the failure mode seen in #76 where LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean exists, but is only a small slice of upstream Monlib/LinearAlgebra/QuantumSet/Basic.lean.