ci: cache the Lean toolchain and retry its installation

.github/actions/install-lean/action.yml

@@ -0,0 +1,34 @@
+name: Install Lean
+description: >-
+  Restore elan and the toolchain named in `lean-toolchain` from the Actions cache, or install them
+  with bounded retries and save them (#1426). Run it before `leanprover/lean-action`: that action
+  always reinstalls elan from GitHub, but then finds the toolchain installed and does not download
+  it from releases.lean-lang.org.
+runs:
+  using: composite
+  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.
+    - name: Restore the Lean toolchain from the Actions cache
+      id: restore
+      uses: actions/cache/restore@caa296126883cff596d87d8935842f9db880ef25 # v5
+      with:
+        path: ~/.elan
+        key: elan-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+    - 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'
+    # Merge-group refs are discarded after the merge, so their copies would only take space from
+    # `main`'s entries. Pull requests restore `main`'s entry; one saves its own copy only when it
+    # changes the toolchain or before `main` has saved the current one.
+    - name: Save the Lean toolchain to the Actions cache
+      if: steps.restore.outputs.cache-hit != 'true' && github.event_name != 'merge_group'
+      uses: actions/cache/save@caa296126883cff596d87d8935842f9db880ef25 # v5
+      with:
+        path: ~/.elan
+        key: elan-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+    - name: Put elan on the path
+      shell: bash
+      run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

.github/actions/install-lean/install.sh

@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+# Install elan and the toolchain named in `lean-toolchain`, retrying transient download failures
+# (#1426). Each step is retried up to LEAN_INSTALL_ATTEMPTS times (default 4), waiting
+# LEAN_INSTALL_DELAY seconds (default 15) before the second attempt and three times longer before
+# each later one. An attempt that runs longer than LEAN_INSTALL_TIMEOUT seconds (default 180) is
+# stopped and counts as a failure: elan can stall indefinitely on a failed TLS connection instead
+# of exiting. An existing elan or toolchain is reused without contacting the network.
+#
+# Usage: install.sh [lean-toolchain path]   (default: ./lean-toolchain)
+set -euo pipefail
+
+toolchain_file="${1:-lean-toolchain}"
+attempts="${LEAN_INSTALL_ATTEMPTS:-4}"
+first_delay="${LEAN_INSTALL_DELAY:-15}"
+attempt_timeout="${LEAN_INSTALL_TIMEOUT:-180}"
+elan_home="${ELAN_HOME:-$HOME/.elan}"
+elan="$elan_home/bin/elan"
+
+retry() {
+  local description="$1" attempt=1 delay="$first_delay"
+  shift
+  until timeout --kill-after=10 "$attempt_timeout" "$@"; do
+    if ((attempt >= attempts)); then
+      echo "::error::$description failed after $attempt attempts"
+      return 1
+    fi
+    echo "::warning::$description failed (attempt $attempt of $attempts); retrying in ${delay}s"
+    sleep "$delay"
+    attempt=$((attempt + 1))
+    delay=$((delay * 3))
+  done
+}
+
+# `timeout` runs a command, not a shell function, so the installer runs in its own shell.
+install_elan='init="$(mktemp)" &&
+  curl --proto =https --tlsv1.2 -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o "$init" &&
+  sh "$init" -y --default-toolchain none --no-modify-path; status=$?; rm -f "$init"; exit "$status"'
+
+if [[ -x "$elan" ]]; then
+  echo "Reusing elan at $elan"
+else
+  retry "elan installation" bash -c "$install_elan"
+fi
+
+toolchain="$(tr -d '[:space:]' < "$toolchain_file")"
+# `elan toolchain install` fails on an installed toolchain, so check first.
+if "$elan" toolchain list | awk '{print $1}' | grep -qxF "$toolchain"; then
+  echo "Reusing installed toolchain $toolchain"
+else
+  retry "installation of $toolchain" "$elan" toolchain install "$toolchain"
+fi
+"$elan" run "$toolchain" lean --version

.github/workflows/docs.yml

@@ -25,6 +25,8 @@ jobs:
       - uses: actions/checkout@v4
       - name: Check documentation pins
         run: python3 scripts/check_docs.py --config-only
+      # Restores or installs the toolchain with retries (.github/actions/install-lean, #1426).
+      - uses: ./.github/actions/install-lean
       - uses: leanprover/lean-action@v1
         with:
           auto-config: "false"

.github/workflows/guide.yml

@@ -13,6 +13,7 @@ on:
       - "scripts/guide.sh"
       - "scripts/check_docs.py"
       - "lean-toolchain"
+      - ".github/actions/install-lean/**"
       - ".github/workflows/guide.yml"
   workflow_dispatch:
 
@@ -31,7 +32,9 @@ jobs:
         with:
           # scripts/cache/get.sh looks for the nearest ancestor whose outputs `main` CI uploaded.
           fetch-depth: 100
-      # Only installs Lean; the guide does not use the Actions cache, which Lean CI fills.
+      # Restores or installs the toolchain with retries (.github/actions/install-lean, #1426).
+      - uses: ./.github/actions/install-lean
+      # Only installs Lean; the guide does not use the `.lake` Actions cache, which Lean CI fills.
       - uses: leanprover/lean-action@v1
         with:
           auto-config: "false"

.github/workflows/lean_action_ci.yml

@@ -55,6 +55,9 @@ jobs:
           path: ./.lake
           key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('./lean-toolchain') }}-${{ hashFiles('./lake-manifest.json') }}-${{ github.sha }}
           restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('./lean-toolchain') }}-${{ hashFiles('./lake-manifest.json') }}
+      # Restore the toolchain from the Actions cache, or install it with retries, so that
+      # lean-action does not download it (.github/actions/install-lean, #1426).
+      - uses: ./.github/actions/install-lean
       - uses: leanprover/lean-action@v1
         with:
           auto-config: "false"

scripts/cache/README.md

@@ -26,6 +26,12 @@ CI reads the cache too. After restoring `.lake` from the GitHub Actions cache, L
 input hash already matches a build trace in `.lake`. A fresh runner would otherwise download a
 complete set on every run, although `.lake` usually has most of it.
 
+The Lean workflows also restore elan and the toolchain named in `lean-toolchain` (`~/.elan`,
+about 600 MB) from the Actions cache before `leanprover/lean-action` runs, so that the action does
+not download the toolchain. On a miss, `.github/actions/install-lean` installs them with bounded
+retries and saves the entry before any Lake command runs, so it never contains the local artifact
+cache above.
+
 ## Merge-queue handoff
 
 After all required checks pass, a merge-group run packages its root `.lake/build` outputs in a