chore: CI: reuse the Lake artifact cache in non-release builds - #14665
Open
Kha wants to merge 4 commits into
Open
chore: CI: reuse the Lake artifact cache in non-release builds#14665Kha wants to merge 4 commits into
Kha wants to merge 4 commits into
Conversation
This PR makes CI reuse cached `.olean`s below the level at which it produces a distributable toolchain, cutting build time for pull requests, the merge queue and master. Nightlies and tagged releases keep building exactly as shipped. A release build passes `CHECK_OLEAN_VERSION=ON`, which is forwarded to stage 0 and so stamps the commit githash into every stage 1 `.olean` and makes `lean` reject `.olean`s carrying any other. That makes the artifacts commit-specific, which is why such a build replaces the system-wide Lake cache with a job-level one and why its stage 1 Actions cache has no cross-commit fallback. Stamping only from check level 2 up makes both usable everywhere below: Lake traces are keyed on the stage 0 tree hash, so they already accept `.olean`s from another commit. The published `lean` still reports the commit githash either way, because stage 1 keeps `USE_GITHASH` at its default, so downstream Lake traces stay commit-specific. `release` also gated the artifact upload that `pr-release.yml` and `grove.yml` consume, so that moves to a separate `upload` matrix entry. The shell tests on `matrix.release` now compare against `true` rather than testing for non-emptiness, which a `false` entry would have passed. Finally, the cache round trip in `Verify Lake Cache` gets a throwaway cache directory, as its `lake cache clean` would otherwise delete the shared system-wide cache that a build without the stamp now uses. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This PR has CI download the Lake artifact cache wherever it builds without the release githash stamp, and removes the `Linux Lake (Cached)` job that existed to try that out alongside the release job. The download and the git depth it needs to resolve a cached ancestor revision were gated on that job's name; they now key off a `lake-cache` matrix entry, which is exactly the complement of `release` because a stamped build cannot load what the cache holds from other commits. The dropped job duplicated the release job's build and test run, so removing it also frees the capacity it took. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This PR drops the Actions cache of stage 1 build outputs, which the Lake artifact cache now supersedes, and has `update-stage0.yml` fetch that cache instead. The two covered the same ground: everything the Actions cache stored lives under the stage 1 `lib` directory, which `Verify Lake Cache` already deletes and restores from the Lake cache on every run. Being content-addressed and global rather than scoped to the branch, the Lake cache should also hit more often, and not saving a copy of the stdlib per commit leaves the repository's Actions cache quota to `ccache`. `update-stage0.yml` built without `USE_LAKE_CACHE` and relied on the release job's Actions cache, so it gains the option and the `cache-get` target. That target already configures stage 1 for itself, and needs no `LEAN_GITHASH` override because this build sets no `CHECK_OLEAN_VERSION`, leaving stage 0's own githash equal to the stage 0 tree hash Lake keys its traces on. It may therefore also reuse `.olean`s stamped with another commit's githash. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
tydeu
approved these changes
Aug 4, 2026
tydeu
reviewed
Aug 4, 2026
This PR makes Lake recompile a bootstrapping package's object files when the Lean runtime headers they are compiled against change, and makes the build refresh its copy of those headers. Previously, editing `src/include/lean/lean.h` left both the copy in the build tree and the stdlib's `.o` files stale. Lake identifies the headers a module's C file includes via its Lean trace, but the core build pins that trace to the stage 0 tree hash and overrides the include directory to the current source tree's headers, so header changes went unnoticed. `buildLeanO` now mixes a trace over the headers in `leanIncludeDir?` into the object file's trace whenever that override is in effect, which is exactly the bootstrapping case. Non-bootstrap packages are unaffected, as their headers are already identified by the toolchain githash. The headers are copied into the build tree, where both the C++ sources and the C files generated by `lean` include them from, by a `lean-headers` build target rather than by a configure-time `file(COPY)`. Editing a header now refreshes the copy during the build instead of requiring a CMake reconfiguration. Note that the Lake change only takes effect for the stage 1 build after `make update-stage0`, since stage 1 is built by stage 0's `lake`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Kha
force-pushed
the
pr-ci-no-release-stamp
branch
from
August 5, 2026 09:55
a6df594 to
133a88a
Compare
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
3 participants
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.
This PR speeds up pull request, merge queue and master builds by having them make full use of the artifact cache. Nightlies and tagged releases keep (re)building exactly as shipped.
Those builds could not use the caches because they were configured as
releasebuilds, which passCHECK_OLEAN_VERSION=ON. That option is forwarded to stage 0, so every stage 1.oleanis stamped with the commit githash andleanrejects any carrying a different one, making the artifacts commit-specific. The stamp is now applied only from check level 2 up, where CI actually produces a toolchain to distribute (with PR releases intentionally ignored here as they are developer-facing). Lake keys its traces on the stage 0 tree hash, so they already accept.oleans built at another commit, and the publishedleanbinary reports the commit githash either way because stage 1 keepsUSE_GITHASHat its default, leaving downstream traces commit-specific.With the stamp gone below that level, the
Linux Lake (Cached)job that existed to exercise the cache alongside the release job is redundant and is removed; its cache download becomes alake-cachematrix entry, kept as the exact complement ofreleasebecause a stamped build would reject what the cache serves it. The Actions cache of stage 1 build outputs is redundant too, since everything it stored lives under the stage 1libdirectory thatVerify Lake Cachealready restores from the Lake cache on every run, and being content-addressed and global rather than scoped to the branch the Lake cache should hit more often. Dropping it also stops writing a copy of the library per commit into the repository's Actions cache quota, whichccache(itself unchanged) shares.