Commit 2025-05-24 22:50 bd15474d

feat(Cache): repository-scoped caches (#25137) Cache can now scope files by repository. By default, it will use the origin Git remote to determine the project repository. This can be overridden with the --repo= option (e.g., lake exe cache --repo=foo/bar get). On a get, it will first fetch the cache for detected repository and then the cache for the main Mathlib repository (i.e., this one). If --repo is specified, it will only fetch the cache for it. On a put, it will upload ALL build files to the (detected or specified) repository's cache. To avoid uploading files already present on the main Mathlib cache, use put-unpacked after fetching from the main cache. This will upload only the newly built (and thus not yet packed) artifacts.