ci: incremental build on PRs — drop forced fresh elaboration (6m → 30s)#46
Merged
Conversation
CI was forcing rm -rf .lake/build/lib/lean/OpenGALib on every PR to force re-elaboration so all Lean linter warnings would reach build.log for the baseline check. With all three linter baselines now at 0 (MathTag/AnchorPurity/Naming), incremental build is sufficient: only re-elaborated files emit warnings, and any new violation in changed files (or their transitive consumers) still fails CI. Changes: - Remove 'Force fresh OpenGALib elaboration' step from PR builds - Improve cache key (include github.sha; restore-keys chain falls back to most-recent same-Mathlib-version build) - Add 'full-lint-on-main' safety-net job: on main push only, force fresh elaboration and re-check linter baselines authoritatively. Catches any regression that incremental missed. Expected impact: PR Lake build time drops from ~6 min → ~30 s on warm cache (90 % cache hit; only changed files + transitive consumers re-elaborate). Cold cache still ~6 min (one-time per Mathlib bump).
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
PR Lake build was forcing
rm -rf .lake/build/lib/lean/OpenGALibon every push to guarantee linter warnings reachbuild.log(Lean linters fire only during elaboration; cached.oleanskips them). With all three linter baselines at 0, incremental build suffices: only re-elaborated files emit warnings, and any new violation in changed files (or transitive consumers) still fails CI.Changes
Drop the forced fresh elaboration step from PR builds. Lake's normal incremental behavior re-elaborates only changed files + transitive deps. Linter warnings on those files still reach
build.log— caught by the unchanged baseline check.Improve cache key: include
${{ github.sha }}so each commit gets its own cache snapshot.restore-keyschain falls back to:Add
full-lint-on-mainsafety-net job: runs only onpushtomain, does fresh elaboration, re-checks linter baselines authoritatively. Catches any regression that incremental missed (rare — requires complex transitive dep effect).Expected impact
Safety analysis
The only way incremental misses a regression: a file's
.oleancached cleanly (no warning), then later a OTHER file's change makes the cached file's docstring/code violate a linter — but the cached file isn't re-elaborated.This can't happen because:
Eng/Mixeddecls): also self-contained.If a file changes, its own linters re-run. If only transitive deps change, the file's linter state can't shift.
Even so,
full-lint-on-mainprovides a safety net at merge time.Test plan
lake buildclean (incremental works)