feat: set MATHLIB_CACHE_GET_URL to cache.mathlib.org for Mathlib cache downloads

CHANGELOG.md

@@ -7,6 +7,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Unreleased
 
+### Changed
+
+- set `MATHLIB_CACHE_GET_URL` to `https://cache.mathlib.org/mathlib4` for
+  `lake exe cache get`, so Mathlib cache clients that read this variable download from
+  cache.mathlib.org. A value that the workflow sets takes precedence. An empty value
+  unsets the variable, so the cache client uses its own default endpoint
+
 ### Fixed
 
 - pass `--no-modify-path` to `elan-init` so installing elan no longer edits the

README.md

@@ -40,6 +40,14 @@ Saving is skipped when the exact cache key was restored.
 > [!NOTE]
 GitHub caching is distinct from Mathlib caching with `lake exe cache get`
 
+### Mathlib cache endpoint
+`lean-action` runs `lake exe cache get` with `MATHLIB_CACHE_GET_URL` set to `https://cache.mathlib.org/mathlib4`.
+Mathlib cache clients that read this variable download from that URL. Older clients ignore it.
+To use a different endpoint, set `MATHLIB_CACHE_GET_URL` in the `env` of your workflow, job, or step.
+`lean-action` keeps that value.
+To use the cache client's default endpoint, set `MATHLIB_CACHE_GET_URL` to an empty string.
+`lean-action` then unsets the variable before it runs `lake exe cache get`.
+
 ### Cache keys
 `lean-action` uses [cache keys](https://github.com/actions/cache?tab=readme-ov-file#creating-a-cache-key) to save and restore caches.
 

action.yml

@@ -286,6 +286,13 @@ runs:
       run: |
         : Get Mathlib Cache
         echo "::group::Mathlib Cache"
+        # Use cache.mathlib.org unless the workflow sets `MATHLIB_CACHE_GET_URL`.
+        # The cache client reads an empty value as a URL, so unset it to get the client's default.
+        if [ -z "${MATHLIB_CACHE_GET_URL+x}" ]; then
+          export MATHLIB_CACHE_GET_URL="https://cache.mathlib.org/mathlib4"
+        elif [ -z "$MATHLIB_CACHE_GET_URL" ]; then
+          unset MATHLIB_CACHE_GET_URL
+        fi
         lake exe cache get
         echo "::endgroup::"
         echo