Repository navigation
Reuse validated project builds after mechanical PR rebases - #545
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [High risk] CI workflow adds GitHub API calls and reuses cached builds. The PR should not merge until its changes to required checks and gates satisfy the repository instruction. FindingsSummaryThe PR adds a conditional rebase job that reuses a previously validated PR project build, overlays available main-build artifacts, and builds the combined Lean root. It also adds artifact packaging, a documentation-preflight shortcut, and static-only quality checking. Reviews (1) · Last reviewed commit: "ci: reuse validated PR builds after mech..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| errors = run_checks( | ||
| root, | ||
| skip_lean_axioms=args.skip_lean_axioms or args.static_only, | ||
| skip_project_declarations=args.static_only, | ||
| ) |
There was a problem hiding this comment.
When artifact restoration succeeds, the rebase workflow runs --static-only instead of its ordinary lint and quality sequence. This flag skips project-declaration and axiom checks, so the rebase gate can pass without running checks required by the normal path. The repository instruction says not to change checks or gates unless explicitly asked. Preserve those checks or obtain an explicit exception before merging.
Context Used: CLAUDE.md (source)
| def test_project_archive_contains_only_pr_module( | ||
| rebased: tuple[Path, str, str, str, str], tmp_path: Path | ||
| ) -> None: | ||
| """The reusable artifact excludes the rest of the large pool build.""" | ||
| root, _, _, base, head = rebased | ||
| for project in ("A", "B", "C"): | ||
| path = root / ".lake/build/lib/lean/LeanPool" / f"{project}.olean" | ||
| path.parent.mkdir(parents=True, exist_ok=True) | ||
| path.write_text(project) | ||
| archive_path = tmp_path / "build.tar.gz" | ||
| rebase_fastpath.pack(root, base, head, archive_path) | ||
| with tarfile.open(archive_path, "r:gz") as archive: | ||
| names = archive.getnames() | ||
| manifest = json.load(archive.extractfile(rebase_fastpath.MANIFEST)) | ||
| assert manifest["projects"] == ["B"] | ||
| assert ".lake/build/lib/lean/LeanPool/B.olean" in names | ||
| assert ".lake/build/lib/lean/LeanPool/A.olean" not in names | ||
| assert ".lake/build/lib/lean/LeanPool/C.olean" not in names |
There was a problem hiding this comment.
This archive test uses only a single-file project, but the packer also collects compiled files from projects with nested modules. Without a nested-project pack-and-restore test covering its library and IR outputs, a regression that omits those files could go unnoticed and force expensive recompilation after rebases.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
1 participant
When the auto-rebase bot merges a newly accepted project into an already green import PR, the PR currently recompiles and revalidates its unchanged project. This adds a verified rebase path: it confirms the prior successful run and unchanged PR-owned sources and project card, restores the PR's compiled modules, overlays the current
mainbuild (or the newly merged project's artifact while that cache warms), builds the combinedLeanPoolroot, and runs static repository checks. If eligibility or artifact restoration fails, normal CI runs. Documentation preflight can likewise check the regenerated root without downloading Mathlib after a verified rebase. Merges tomainkeep the full validation path.PR builds now retain a small project-scoped artifact for later rebases; existing open PRs need one normal run to seed it.
Validation: 500 Python tests; Ruff lint and format; actionlint; generated-index check; static repository quality check; local Lean artifact-restore/root-build smoke test; eligibility checked against a real rebased PR history.