ci+hooks: auto-bootstrap Lean for web sessions + consolidate CI onto the script

Future-dependability follow-through (both authorized):

1. SessionStart hook (.claude/hooks/session-start.sh + .claude/settings.json):
   web/remote sessions auto-install the pinned Lean toolchain via
   proofs/bootstrap-lean.sh before the agent loop starts, so the proofs can be
   built/verified out of the box. Synchronous; resilient (a bootstrap failure
   warns but does not block the session); a no-op outside Claude Code on the web.

2. lean-proofs.yml now installs the toolchain through proofs/bootstrap-lean.sh
   instead of a bespoke elan step — single source of truth, and CI gains the
   GitHub-asset fallback so it stays green if release.lean-lang.org is down.

bootstrap-lean.sh: shellcheck-clean (SC2016 on the intentional literal $PATH
in --print-path is annotated). Verified: hook is a no-op when not remote and
bootstraps when remote; `lean Tangle.lean` still reports 0 errors.

https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE

Author: Jonathan D.A. Jewell

.claude/hooks/session-start.sh

@@ -0,0 +1,34 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SessionStart hook — make Lean available in Claude Code on the web so the
+# proofs in proofs/Tangle.lean can be built and verified (the repo's working
+# rule: "every edit ends with a Lean compile").
+#
+# Thin wrapper over proofs/bootstrap-lean.sh (the single source of truth for
+# toolchain setup). Synchronous: guarantees Lean is ready before the agent
+# loop starts, so it never races a build/verify against a half-installed
+# toolchain. Web/remote sessions only; local developers use their own Lean.
+set -euo pipefail
+
+[ "${CLAUDE_CODE_REMOTE:-}" = "true" ] || exit 0
+
+REPO="${CLAUDE_PROJECT_DIR:-$(pwd)}"
+BOOT="$REPO/proofs/bootstrap-lean.sh"
+if [ ! -x "$BOOT" ]; then
+  echo "session-start: $BOOT not found or not executable; skipping Lean bootstrap."
+  exit 0
+fi
+
+# Install the pinned toolchain (idempotent; ~16s cold, instant when cached).
+# A failure must not block the whole session — Lean just won't be ready, and
+# the developer can run proofs/bootstrap-lean.sh by hand.
+if "$BOOT"; then
+  # Persist `lean` on PATH for the rest of the session.
+  if [ -n "${CLAUDE_ENV_FILE:-}" ]; then
+    "$BOOT" --print-path >> "$CLAUDE_ENV_FILE"
+  fi
+else
+  echo "session-start: Lean bootstrap failed; continuing without Lean." \
+       "Run proofs/bootstrap-lean.sh manually once network is available." >&2
+fi
+exit 0

.claude/settings.json

@@ -0,0 +1,14 @@
+{
+  "hooks": {
+    "SessionStart": [
+      {
+        "hooks": [
+          {
+            "type": "command",
+            "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh"
+          }
+        ]
+      }
+    ]
+  }
+}

.github/workflows/lean-proofs.yml

@@ -40,13 +40,16 @@ jobs:
         with:
           persist-credentials: false
 
-      - name: Install elan
+      - name: Bootstrap Lean toolchain (pinned; GitHub-asset fallback)
         run: |
-          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-            | sh -s -- -y --default-toolchain none
+          # Single source of truth for toolchain setup (proofs/bootstrap-lean.sh).
+          # Uses the normal elan dist server on open networks (GitHub runners);
+          # falls back to the GitHub release asset if release.lean-lang.org is
+          # unreachable, so CI stays green through dist-server outages.
+          bash proofs/bootstrap-lean.sh
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-      - name: Pin Lean toolchain from proofs/lean-toolchain
+      - name: Show pinned Lean version
         working-directory: proofs
         run: |
           test -f lean-toolchain || { echo "::error::proofs/lean-toolchain missing"; exit 1; }

proofs/bootstrap-lean.sh

@@ -45,6 +45,9 @@ TC_PATH="$ELAN_DIR/toolchains/$TC_NAME"
 
 # --print-path mode: just emit the PATH export (for eval), do no work.
 if [ "$PRINT_PATH" -eq 1 ]; then
+  # $PATH is intentionally literal — it must expand when this line is later
+  # eval'd / sourced, not now. Only %s (= $ELAN_DIR) expands here.
+  # shellcheck disable=SC2016
   printf 'export PATH="%s/bin:$PATH"\n' "$ELAN_DIR"
   exit 0
 fi