Repository navigation
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds a new Python-based CI audit to detect “partial port” failure modes where a LeanPool project imports only a small slice of its declared upstream GitHub repository, by comparing imported Lean filenames (normalized) and non-comment LOC against the upstream checkout with a tolerance threshold, and reporting the largest missing upstream files.
Changes:
- Add
lean_pool.partial_port_auditCLI + supporting dataclasses to compute imported vs upstream Lean stats and emit findings. - Add pytest coverage for comment-stripping LOC counting, filename normalization, and suspicious/acceptable import scenarios.
- Add a GitHub Actions workflow that runs the audit on content PRs affecting LeanPool Lean files or
projects.yml.
Fit: good_fit
Level: undergraduate
Branch: repository tooling / CI
Mode: theory_building
Obscure problem: false
Code quality: 4/5
Significance: Helps maintain repository integrity by automatically flagging likely-incomplete upstream ports and surfacing actionable missing-file hints.
Verdict: request_changes
Actionable findings:
- The audit currently won’t run when only
LeanPool/projects.ymlchanges (despite the workflow triggering on that), so the intended check is skipped for metadata-only content PRs. - The “deterministic” claim is undermined by cloning upstream default-branch HEAD (time-dependent), and the workflow currently doesn’t enforce locked Python dependency resolution.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
python/lean_pool/partial_port_audit.py |
Implements the upstream-vs-imported comparison logic and CLI. |
python/tests/test_partial_port_audit.py |
Adds unit tests for LOC counting, stem normalization, and finding logic. |
.github/workflows/partial-port-audit.yml |
Wires the audit into CI for content PRs. |
Comment on lines
+123
to
+131
| def touched_prefixes(paths: list[str]) -> set[str]: | ||
| """Return top-level LeanPool project prefixes touched by a diff.""" | ||
| prefixes: set[str] = set() | ||
| for path in paths: | ||
| parts = path.split("/") | ||
| if len(parts) == 2 and parts[0] == "LeanPool" and parts[1].endswith(".lean"): | ||
| prefixes.add(parts[1].removesuffix(".lean")) | ||
| elif len(parts) >= 3 and parts[0] == "LeanPool": | ||
| prefixes.add(parts[1]) |
Comment on lines
+210
to
+217
| def clone_upstream(repo: str, clone_root: Path) -> Path | None: | ||
| """Clone ``repo`` under ``clone_root`` and return the checkout path.""" | ||
| target = clone_root / repo.replace("/", "__") | ||
| if target.exists(): | ||
| shutil.rmtree(target) | ||
| process = subprocess.run( | ||
| ["git", "clone", "--depth=1", f"https://github.com/{repo}.git", str(target)], | ||
| check=False, |
|
|
||
| - name: Sync Python dependencies | ||
| working-directory: python | ||
| run: uv sync |
Collaborator
Author
|
/profile |
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
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.
Adds a deterministic CI check for the porting failure mode where an import only includes a small slice of the upstream Lean project.
The audit runs on content PRs, reads the project source from
LeanPool/projects.yml, clones the upstreamsource.github_repo, and compares imported Lean file names plus non-comment LOC against upstream with a 10% tolerance. It reports the largest unmatched upstream files so the PR author can either port them or explicitly justify the scope.Local checks:
cd python && uv run ruff checkcd python && uv run ruff format --checkcd python && uv run --group test pytest tests/test_partial_port_audit.py