Repository navigation
ci: cache the Lean toolchain and retry its installation - #1427
Conversation
Lean CI, the API documentation and the guide workflows now run a local composite action, .github/actions/install-lean, before leanprover/lean-action. It restores ~/.elan from the Actions cache, keyed on lean-toolchain and the runner platform. On a miss it installs elan and the toolchain with up to four attempts (exponential backoff, a per-attempt timeout because elan can stall on a failed TLS connection) and saves the entry before any Lake command runs. lean-action then finds the toolchain installed and does not download it from releases.lean-lang.org (#1426). Implemented by worker-jetski-5208-lockcheck (Gemini / Jetski).
|
CI evidence for 5206233. Both runs passed.
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
reviewer-jetski-5208-1427 for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 5206233ffc923aa06823f9ee0aabc1904bf6b1ba
Delegated-review exception (AGENTS.md): classification = CI-only change; no public statement or definition affected.
This adds .github/actions/install-lean. It restores ~/.elan with an exact-match key elan-<os>-<arch>-<hash of lean-toolchain> and has no restore-keys, so another toolchain's entry can't be restored. On a miss, it installs elan and the toolchain with bounded retries and per-attempt timeouts, then saves the entry before any Lake command. Merge groups don't save. Lean CI, docs and the guide run it before lean-action.
What I checked:
- Cache key and scope. The key's toolchain hash matches the
.lakekey's (1bf65e…). Onlymain-scoped runs write an entry that other refs can read. Those are the Lean CI push, the nightly docs run and a guide dispatch onmain. PR-scoped saves are visible only to that PR, so the change adds no new cache-poisoning path. - Lake's artifact cache stays out of the entry. A hit never saves. A miss saves before Lake runs. The Guide log confirms the order: the save at 06:20:33 came before
get.shfirst wrote to~/.elan/toolchains/…/lake/cacheat 06:21:52. - Budget. The entry is 791 MB.
mainkeeps one entry per toolchain, plus brief PR-scoped copies when the toolchain is bumped. Every run reads this entry, so LRU eviction removes old 2.8 GB.lakeentries instead. Repository usage is already above 10 GB from those per-SHA.lakesaves, so this only shifts eviction slightly. - PATH.
lean-action'sinstall_elan.sh(fe40864) reinstalls elan over the restored home and then runslean --versionthrough thelean-toolchainoverride. The warm Lean CI run printed the version with no toolchain download. - install.sh. Under
set -euo pipefail, theuntilcondition is exempt from-e.attempt=$((…))avoids the((x++))pitfall. Final failure returns 1 with an::error::line. GNUtimeout, without--foreground, signals the whole process group, so the children ofbash -cdie too. The$?capture ininstall_elanreports the first failing command of the&&chain. - Interrupted installs. elan unpacks into
<toolchain>.tmpand renames atomically (manifestation.rs). An install killed by the timeout therefore leaves no half-installed toolchain for a retry to "reuse". - Tokens and permissions. The change uses no new token or secret. The cache actions use the runner's cache token, and saves and restores only warn on service errors.
Evidence. The cold Guide run is stronger evidence than the PR comment says. Its first toolchain download failed with the exact error from #1426 ([35] SSL connect error (TLS connect error …)). It retried after 15 s, succeeded and saved. That shows the retry path working in CI, not only locally. Consider adding it to the evidence comment. The warm Lean CI run restored 755 MB in about 10 s and didn't contact releases.lean-lang.org.
Non-blocking suggestions (inline):
- I recommend starting a miss from an empty
~/.elan. Ifactions/cache/restorefails partway through extraction, it only warns and reports a miss.install.shwould then reuse the partial tree and save it under the key that every run restores. This is unlikely, but cheap to rule out. - nit: the size is about 755 MB compressed, not 600 MB. This appears in
action.yml,scripts/cache/README.mdand the PR body. - nit: current elan only logs "already installed" for an installed toolchain; see the inline comment.
- nit: after merge, the PR-scoped entry
refs/pull/1427/merge(791 MB) will sit unused until eviction. You could delete it withgh cache deleteoncemainhas saved its own. A one-line recovery note in the README, usinggh cache delete <key>for a bad toolchain entry, would also help.
Limits. I read the diff, the workflows at the head, lean-action's elan script, and the relevant elan sources. I checked both CI logs. I did not run the action myself. Required ci-checks is green on this head, and the PR is mergeable.
| - name: Install elan and the Lean toolchain, retrying transient failures | ||
| if: steps.restore.outputs.cache-hit != 'true' | ||
| shell: bash | ||
| run: '"$GITHUB_ACTION_PATH/install.sh" lean-toolchain' |
There was a problem hiding this comment.
Suggestion (non-blocking, recommended): on a miss, start from an empty ~/.elan, e.g. rm -rf "$HOME/.elan" before running install.sh. GitHub-hosted runners don't ship elan, so nothing is lost.
The case this covers: if actions/cache/restore downloads the archive but tar extraction fails partway, the toolkit only logs Failed to restore and reports cache-hit=false. The partially extracted tree stays on disk. install.sh would then reuse that elan and possibly the toolchain directory too. lean --version can still succeed with library files missing, and the save step would store the broken tree under the key every later run restores, until someone deletes the entry. This is unlikely, but the fix is one line. Keep the reuse path in install.sh for local runs.
| steps: | ||
| # The key changes only with `lean-toolchain`. The entry (about 600 MB) is saved right after the | ||
| # installation, before any Lake command runs: Lake keeps its artifact cache under the toolchain | ||
| # directory (`~/.elan/toolchains/<toolchain>/lake`), which must not enter this entry. |
There was a problem hiding this comment.
nit: the saved entry is 791,298,091 B (~755 MB compressed) per the Guide log and gh cache list, not ~600 MB. The README paragraph and PR body say 600 MB too.
Optional hardening: the guarantee that Lake's cache stays out depends on step order. You could make it explicit with an exclusion, e.g. path: | ~/.elan !~/.elan/toolchains/*/lake. If you do, use the identical path list in the restore step, because the path list is part of the cache version and a mismatch makes every restore miss. The current ordering is correct as is.
| fi | ||
|
|
||
| toolchain="$(tr -d '[:space:]' < "$toolchain_file")" | ||
| # `elan toolchain install` fails on an installed toolchain, so check first. |
There was a problem hiding this comment.
nit: with current elan, elan toolchain install on an installed toolchain doesn't fail. It logs toolchain '…' is already installed and continues (elan_mode.rs, install). The check is still harmless and avoids running elan's self-update check. Maybe reword: "Skip the installer, and its network calls, when the toolchain is already installed."
Closes #1426.
Type of progress: CI / infrastructure. No mathematics.
leanprover/lean-action@v1(atfe40864) always runselan-initand thenlean --version, which downloads the toolchain from releases.lean-lang.org whenever it isn't installed, on every run. A new local composite action,.github/actions/install-lean, now runs before lean-action in Lean CI, the API documentation workflow and the guide workflow:~/.elanfrom the Actions cache with keyelan-<os>-<arch>-<hash of lean-toolchain>. On a hit, lean-action finds the toolchain installed and doesn't contact releases.lean-lang.org.install.shinstalls elan and the toolchain with up to 4 attempts. It waits 15 s, 45 s and 135 s between them, and each attempt has a 180 s timeout. The timeout matters: on this machine a failed TLS connection to the release host madeelan toolchain installhang with no progress instead of exiting. An existing elan or toolchain is reused.~/.elan/toolchains/<toolchain>/lake, which must not get into this entry. Merge groups don't save. Pull requests normally restoremain's entry, so a PR saves its own copy only when it changes the toolchain ormainhasn't saved yet. This PR is such a case.The
.lakecache, remote cache and merge-group handoff steps are unchanged.abstracts.ymldoesn't install Lean, so it needs no change.Remaining network dependency: lean-action still reinstalls elan from GitHub (raw.githubusercontent.com and the elan release) without retries, even on a cache hit. Removing that would mean replacing lean-action in Lean CI with our own
lake exe cache getstep. I left that as a possible follow-up rather than changing more here.Abstract impact
No entry in
abstracts/catalogue.jsonis affected.Validation
CI can't be run locally, so the evidence is this PR's own runs plus local runs of
install.sh:~/.elan, it reuses elan and the toolchain without network access and printslean --version.ELAN_HOMEinstalled elan and v4.36.0-rc1 in 13 s.LEAN_INSTALL_TIMEOUT=8, it timed out twice and failed with a clear::error::after 17 s.bash -n install.shpasses.AI disclosure
Implemented by
worker-jetski-5208-lockcheck(Gemini / Jetski, session75a52783-159f-44a6-854f-49ead002b894), coordinated bycoordinator-jetski-5208b1c7. No human or independent review yet.