Commit 2026-08-20 15:53 edae46c8

feat(cache): add a base URL for cache reads (#42657) The cache tool sends every request to the Azure storage account, and the account hostname is fixed in the tool. This PR adds MATHLIB_CACHE_BASE_URL: reads are {base}/{container}/{key} via the new Container.getURL, and any host that serves the same namespace is a valid base. The default base is the Azure account, so no command changes behavior. Writes (uploads, markers, blob listing) authenticate against Azure and keep Container.azureURL. Reads follow redirects, so a base can answer with the blob's current location; %{http_code} reports the final response, so the tool tells a hit from a miss. A redirect may target only https, and the chain is short (--proto-redir =https --max-redirs 5). The intention is to migrate this endpoint eventually. MATHLIB_CACHE_BASE_URL is intended for CI (and for contributors of the mathlib4 repository, if we need to override for some regression) We choose not to change the behavior of MATHLIB_CACHE_GET_URL, which overrides the 'container lookup change' entirely, because external tools (Lean-zh/LeanUp, kim-em/bubble) depend on this already; a dependency overrides that variable instead. MATHLIB_CACHE_BASE_URL instead serves the "official" multi-container namespace through a different host, and it keeps the container chain whole. Cache/SECURITY.md lists a substituted read endpoint as out of scope: the host that answers a read chooses the bytes it serves. Validation: a cold cache get pulled all 8678 files from a live mirror host, and again with the host in redirect mode. Two green ci_dev runs (one, two) set MATHLIB_CACHE_BASE_URL: https://cache.mathlib.org for all jobs and read the full cache through that host. Not covered there: fall-through reads from forks and legacy, the marker probe, and uploads (ci_dev skips them; the write path does not read the base).