feat: lake: local artifact cache #8922
Merged
Conversation
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
c8af5af to
4b684a8
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 22, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 22, 2025
|
Mathlib CI status (docs):
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 22, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 22, 2025
|
!bench |
|
Here are the benchmark results for commit 9c75dfa. Benchmark Metric Change
================================================
+ nat_repr task-clock -12.7% (-27.4 σ)
+ nat_repr wall-clock -12.7% (-26.5 σ)
- workspaceSymbols task-clock 4.8% (33.3 σ)
- workspaceSymbols wall-clock 4.8% (34.2 σ) |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 25, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 25, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 26, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 26, 2025
7f679ce to
6f6c053
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 27, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 27, 2025
|
!bench |
|
Here are the benchmark results for commit 6f6c053. Benchmark Metric Change
=================================================
- stdlib grind 1.0% (24.9 σ)
- stdlib grind canon 1.6% (429.2 σ)
- stdlib wall-clock 6.2% (66.3 σ)
- workspaceSymbols task-clock 2.2% (28.5 σ)
- workspaceSymbols wall-clock 2.2% (25.4 σ) |
06c57c0 to
b5de358
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 27, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 27, 2025
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.
This PR introduces a local artifact cache for Lake. When enabled, Lake will shared build artifacts (built files) across different instances of the same package using an input- and content-addressed cache.
To enable support for the local cache, packages must set
enableArtifactCache := truein their package configuration. The reason for this is twofold. This feature is new and experimental, so it should be opt-in. Also, some packages may need to disable it as the cache entails that artifacts are no longer necessarily available within the build directory, which can break custom build scripts.The cache location is determined by the system configuration. Lake's first preference is to store it under the Lean toolchain in a
lake/cachedirectory. If Elan is not available, Lake will store it in common system location (e.g.,$XDG_CACHE_HOME/lake, or~/.cache/lake). On an exotic system where neither of these exist, the cache will be disabled. Users can override this location through theLAKE_CACHE_DIRenvironment variable. If set to empty, caching will be disabled.The cache is both input and content-addressed. Mappings from input hash to output content hash(es) are stored in a per-package JSON Lines file (e.g.,
<cache-dir>/inputs/<pkg-name>.jsonl). Thus, mappings are shared across different instances of a package, but not between packages. The output content hashes are also now stored in trace files in a newoutputsfield. The value of this field can be either a single hash or an object of multiple content hashes for targets which produce multiple artifacts (e.g., Lean module builds). Separately, artifacts are stored in a single flat content-addressed cache (e.g.,<cache-dir>/artifacts/<hash>.art. Artifacts are therefore shared across all cache-enabled packages.Module
*.oleanand and*.ileanartifacts are cached. However, each package will still copy the files to their build directory, as Lean and the server currently expect them to be at a specific path. This will be changed for*.oleanfiles when the performance issues with pre-resolving modules in Lake forlean --setupare solved.