Commit 2026-09-02 18:10 03616a12
View on Github āfeat(cache): read from cache.mathlib.org by default (#43308)
Cache reads use https://cache.mathlib.org by default. The endpoint serves the same /{container}/{key} namespace as the Azure storage account, and it caches artifacts at its edge.
Upcoming changes include separating the storage for forks from the master cache.
CI already reads through the endpoint: PR #42657 added the MATHLIB_CACHE_BASE_URL seam, and PR #42777 wired it from a repository variable. This PR makes the endpoint the default for every other client.
MATHLIB_CACHE_DEBUG_USE_LEGACY=1 sends reads back to the storage account. The variable is a troubleshooting fallback, hence 'unsupported', albeit documented. 1 and true turn it on, 0, false, and an absent or empty value turn it off, and any other value prints one warning and keeps the default.
MATHLIB_CACHE_BASE_URL stays as a durable way to choose a read host for CI, and it takes precedence.
The write path does not change in this PR.
After this PR, an empty MATHLIB_CACHE_BASE_URL selects the endpoint, not Azure. To send CI back to Azure, set the variable to https://lakecache.blob.core.windows.net.
Validation: lake exe cache-test passes with no variable set, with the legacy flag, and with a base URL set. A live lake exe cache get Mathlib/Init.lean fetched 64 of 64 files from the endpoint by default, and the same 64 from the storage account under the flag. A set base URL won over the flag, and an unrecognized flag value printed exactly one warning.
š¤ Generated with Claude Code