Commit 2026-10-06 00:50 508cfcd1

feat(cache): build the URLs of reads and uploads from a single Location type (#44173) This PR adds one type, Location, that builds the URLs of every cache read and every upload (Cache/Location.lean). A location is a root URL, a label, and an optional scope (a repo and, optionally, a commit). The scope gives the files directory. Only a scope with a commit gives a marker. A known container resolves to a location with Container.location, which adds the container segment to the base URL. A user-supplied URL resolves with Location.ofEndpoint. Both trim whitespace and trailing slashes.

• A read resolves its trust-ordered locations (readLocations), then downloads through them (downloadFiles).
• An upload resolves one location (uploadLocation), then writes the files and the location's marker, if any. mkFileURL, markerReadURL, StagedUploadDest, containerUploadDest, Container.getURL, and Cache/Upload/Dest.lean are removed. The URLs do not change. Behavior changes:
• All Git lookups (HEAD, --scope refs, cache query, --unsafe) run in the Mathlib checkout, not the current directory.
• MATHLIB_CACHE_PUT_URL is normalized, and upload messages label it by the variable name.
• The curl upload message names the full directory.
• get resolves its locations before it checks for missing files, so a bad MATHLIB_CACHE_FROM always warns. The layout rules stay as they are on master. #43900 and #43330 will build on this type. lake exe cache-test passes (380 assertions). 🤖 Generated with Claude Code