From 98e57abe34f3e0b7935dd02b9df22059f21ab410 Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Thu, 22 Oct 2026 16:40:53 -0300 Subject: [PATCH 1/3] feat: set MATHLIB_CACHE_GET_URL to cache.mathlib.org for Mathlib cache downloads --- CHANGELOG.md | 6 ++++++ README.md | 7 +++++++ action.yml | 3 +++ 3 files changed, 16 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e821e0a..9749d4d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,12 @@ 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` when running + `lake exe cache get`, so Mathlib cache clients that read this variable download from + cache.mathlib.org. A value set by the workflow takes precedence + ### Fixed - pass `--no-modify-path` to `elan-init` so installing elan no longer edits the diff --git a/README.md b/README.md index add0c4e..8dbd260 100644 --- a/README.md +++ b/README.md @@ -40,6 +40,13 @@ 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 cache.mathlib.org. +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 a value that your workflow sets. + ### 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. diff --git a/action.yml b/action.yml index 8ebeca1..822f54c 100644 --- a/action.yml +++ b/action.yml @@ -286,6 +286,9 @@ runs: run: | : Get Mathlib Cache echo "::group::Mathlib Cache" + # Point cache clients that read `MATHLIB_CACHE_GET_URL` at cache.mathlib.org. + # A value set by the workflow takes precedence. + export MATHLIB_CACHE_GET_URL="${MATHLIB_CACHE_GET_URL:-https://cache.mathlib.org/mathlib4}" lake exe cache get echo "::endgroup::" echo From 9e3cf7e5d3205909a2370b67558dd7572ac5c571 Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Thu, 22 Oct 2026 17:56:24 -0300 Subject: [PATCH 2/3] feat: unset an empty MATHLIB_CACHE_GET_URL so the cache client uses its default --- CHANGELOG.md | 3 ++- README.md | 2 ++ action.yml | 7 ++++++- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9749d4d..6f76518 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - set `MATHLIB_CACHE_GET_URL` to `https://cache.mathlib.org/mathlib4` when running `lake exe cache get`, so Mathlib cache clients that read this variable download from - cache.mathlib.org. A value set by the workflow takes precedence + cache.mathlib.org. A value set by the workflow takes precedence. An empty value + unsets the variable, so the cache client uses its own default endpoint ### Fixed diff --git a/README.md b/README.md index 8dbd260..f0a0ef5 100644 --- a/README.md +++ b/README.md @@ -46,6 +46,8 @@ Mathlib cache clients that read this variable download from cache.mathlib.org. 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 a value that your workflow sets. +To use the default endpoint of the cache client, 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. diff --git a/action.yml b/action.yml index 822f54c..edad32b 100644 --- a/action.yml +++ b/action.yml @@ -288,7 +288,12 @@ runs: echo "::group::Mathlib Cache" # Point cache clients that read `MATHLIB_CACHE_GET_URL` at cache.mathlib.org. # A value set by the workflow takes precedence. - export MATHLIB_CACHE_GET_URL="${MATHLIB_CACHE_GET_URL:-https://cache.mathlib.org/mathlib4}" + # An empty value unsets the variable, so the client uses its own 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 From 7968f4c5a1e1540326b6777b61a6d83840175e9a Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Thu, 22 Oct 2026 17:58:12 -0300 Subject: [PATCH 3/3] docs: reword the Mathlib cache endpoint comment, README section, and CHANGELOG entry --- CHANGELOG.md | 4 ++-- README.md | 7 +++---- action.yml | 5 ++--- 3 files changed, 7 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6f76518..395dca5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,9 +9,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Changed -- set `MATHLIB_CACHE_GET_URL` to `https://cache.mathlib.org/mathlib4` when running +- 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 set by the workflow takes precedence. An empty value + 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 diff --git a/README.md b/README.md index f0a0ef5..6f66b53 100644 --- a/README.md +++ b/README.md @@ -42,11 +42,10 @@ 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 cache.mathlib.org. -Older clients ignore it. +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 a value that your workflow sets. -To use the default endpoint of the cache client, set `MATHLIB_CACHE_GET_URL` to an empty string. +`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 diff --git a/action.yml b/action.yml index edad32b..ebf11cf 100644 --- a/action.yml +++ b/action.yml @@ -286,9 +286,8 @@ runs: run: | : Get Mathlib Cache echo "::group::Mathlib Cache" - # Point cache clients that read `MATHLIB_CACHE_GET_URL` at cache.mathlib.org. - # A value set by the workflow takes precedence. - # An empty value unsets the variable, so the client uses its own default. + # 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