leanprover
feat: lake: local artifact cache
This PR introduces an local artifact cache for Lake. When enabled, Lake will shared build artifacts (built files) across different instances of the same package using and input- and content-addressed cache.
The cache location is determined by the system configuration. Lake's first preference is to store it under the Lean toolchain in a lake/cache directory. 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, the cache will be disabled. Users can override this location through the LAKE_CACHE_DIR environment variable. If set but empty, caching will be disabled.
The cache is both input and content-addressed. Input hash to content hash mappings 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. 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.
To enable support for the local cache, packages must set enableArtifactCache := true in 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 means artifacts are no longer necessarily available within the build directory, which can break custom build scripts.
Module *.olean and and *.ilean artifacts 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 *.olean files when the performance issues with pre-resolving modules in Lake for lean --setup are solved.
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-8922 has successfully built against this PR. (2025-06-22 04:52:57) View Log
- ✅ Mathlib branch lean-pr-testing-8922 has successfully built against this PR. (2025-06-22 06:05:06) View Log
- ✅ Mathlib branch lean-pr-testing-8922 has successfully built against this PR. (2025-06-27 03:09:48) View Log
- ✅ Mathlib branch lean-pr-testing-8922 has successfully built against this PR. (2025-06-27 04:53:18) View Log
Here are the benchmark results for commit 9c75dfa1d657e96e24da106bca39b448a96557ea. There were significant changes against commit db499e96aac8ad654c8ed5ab40c4e6885d38c9a1:
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 σ)
Here are the benchmark results for commit 6f6c053f402f650e2f826b6db8eed946044c9c1c. There were significant changes against commit d3dda9f6d4428a906c096067ecb75e432afc4615:
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 σ)