|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# bootstrap-lean.sh — install the pinned Lean 4 toolchain so the proofs in |
| 4 | +# this directory can be built and verified. |
| 5 | +# |
| 6 | +# WHY THIS EXISTS |
| 7 | +# proofs/Tangle.lean is the repo's build oracle (.github/workflows/ |
| 8 | +# lean-proofs.yml) and the working rule is "every edit ends with a Lean |
| 9 | +# compile". GitHub Actions runners have open network and install Lean fine, |
| 10 | +# but sandboxed/allowlisted environments (e.g. Claude Code on the web) |
| 11 | +# cannot reach elan's default dist server release.lean-lang.org. GitHub |
| 12 | +# release assets ARE reachable, so when the normal install path is blocked |
| 13 | +# this script fetches the pinned toolchain directly from github.com. |
| 14 | +# |
| 15 | +# The version is read from proofs/lean-toolchain, so this stays correct |
| 16 | +# when the pin is bumped. Idempotent and non-interactive. |
| 17 | +# |
| 18 | +# USAGE |
| 19 | +# ./proofs/bootstrap-lean.sh # install the toolchain |
| 20 | +# eval "$(./proofs/bootstrap-lean.sh --print-path)" # and put lean on PATH |
| 21 | +# # then: |
| 22 | +# cd proofs && lean Tangle.lean # 0 errors == proofs verified |
| 23 | +set -euo pipefail |
| 24 | + |
| 25 | +PRINT_PATH=0 |
| 26 | +[ "${1:-}" = "--print-path" ] && PRINT_PATH=1 |
| 27 | + |
| 28 | +# Resolve repo paths relative to this script. |
| 29 | +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" |
| 30 | +PIN_FILE="$SCRIPT_DIR/lean-toolchain" |
| 31 | + |
| 32 | +log() { [ "$PRINT_PATH" -eq 1 ] || echo "bootstrap-lean: $*"; } |
| 33 | + |
| 34 | +if [ ! -f "$PIN_FILE" ]; then |
| 35 | + echo "bootstrap-lean: no $PIN_FILE found" >&2 |
| 36 | + exit 1 |
| 37 | +fi |
| 38 | + |
| 39 | +PIN="$(tr -d '[:space:]' < "$PIN_FILE")" # e.g. leanprover/lean4:v4.14.0 |
| 40 | +VER="${PIN##*:}" # v4.14.0 |
| 41 | +VNUM="${VER#v}" # 4.14.0 |
| 42 | +ELAN_DIR="${ELAN_HOME:-$HOME/.elan}" |
| 43 | +TC_NAME="$(printf '%s' "$PIN" | sed 's|/|--|; s|:|---|')" # leanprover--lean4---v4.14.0 |
| 44 | +TC_PATH="$ELAN_DIR/toolchains/$TC_NAME" |
| 45 | + |
| 46 | +# --print-path mode: just emit the PATH export (for eval), do no work. |
| 47 | +if [ "$PRINT_PATH" -eq 1 ]; then |
| 48 | + # $PATH is intentionally literal — it must expand when this line is later |
| 49 | + # eval'd / sourced, not now. Only %s (= $ELAN_DIR) expands here. |
| 50 | + # shellcheck disable=SC2016 |
| 51 | + printf 'export PATH="%s/bin:$PATH"\n' "$ELAN_DIR" |
| 52 | + exit 0 |
| 53 | +fi |
| 54 | + |
| 55 | +export PATH="$ELAN_DIR/bin:$PATH" |
| 56 | + |
| 57 | +# Already bootstrapped — fast idempotent exit. |
| 58 | +if [ -x "$TC_PATH/bin/lean" ]; then |
| 59 | + log "Lean toolchain $PIN already present at $TC_PATH" |
| 60 | + log "Run: eval \"\$($0 --print-path)\" then (cd $SCRIPT_DIR && lean Tangle.lean)" |
| 61 | + exit 0 |
| 62 | +fi |
| 63 | + |
| 64 | +# 1. elan (toolchain manager). raw.githubusercontent.com is reachable. |
| 65 | +if [ ! -x "$ELAN_DIR/bin/elan" ]; then |
| 66 | + log "installing elan…" |
| 67 | + curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ |
| 68 | + | sh -s -- -y --default-toolchain none >/dev/null |
| 69 | +fi |
| 70 | + |
| 71 | +# 2. Try the normal toolchain install; fall back to the GitHub release asset |
| 72 | +# if the elan dist server is unreachable (the allowlist case). |
| 73 | +if "$ELAN_DIR/bin/elan" toolchain install "$PIN" >/dev/null 2>&1 \ |
| 74 | + && [ -x "$TC_PATH/bin/lean" ]; then |
| 75 | + log "installed $PIN via elan." |
| 76 | +else |
| 77 | + log "elan dist server unreachable — using GitHub release asset." |
| 78 | + arch="$(uname -m)" |
| 79 | + case "$arch" in |
| 80 | + x86_64) asset="lean-${VNUM}-linux.tar.zst" ;; |
| 81 | + aarch64) asset="lean-${VNUM}-linux_aarch64.tar.zst" ;; |
| 82 | + *) echo "bootstrap-lean: unsupported arch '$arch'" >&2; exit 1 ;; |
| 83 | + esac |
| 84 | + url="https://github.com/leanprover/lean4/releases/download/${VER}/${asset}" |
| 85 | + tmp="$(mktemp -d)" |
| 86 | + trap 'rm -rf "$tmp"' EXIT |
| 87 | + log "downloading $url" |
| 88 | + curl -sSfL -o "$tmp/lean.tar.zst" "$url" |
| 89 | + |
| 90 | + # zstd is needed to unpack .tar.zst. |
| 91 | + if ! command -v unzstd >/dev/null 2>&1 && ! command -v zstd >/dev/null 2>&1; then |
| 92 | + if command -v apt-get >/dev/null 2>&1; then |
| 93 | + sudo apt-get install -y zstd >/dev/null 2>&1 \ |
| 94 | + || apt-get install -y zstd >/dev/null 2>&1 || true |
| 95 | + fi |
| 96 | + fi |
| 97 | + |
| 98 | + mkdir -p "$ELAN_DIR/toolchains" |
| 99 | + tar --use-compress-program=unzstd -xf "$tmp/lean.tar.zst" -C "$tmp" |
| 100 | + extracted="$(find "$tmp" -maxdepth 1 -type d -name 'lean-*' | head -1)" |
| 101 | + if [ -z "$extracted" ]; then |
| 102 | + echo "bootstrap-lean: extraction produced no lean-* directory" >&2 |
| 103 | + exit 1 |
| 104 | + fi |
| 105 | + rm -rf "$TC_PATH" |
| 106 | + mv "$extracted" "$TC_PATH" |
| 107 | + log "installed $PIN from GitHub release." |
| 108 | +fi |
| 109 | + |
| 110 | +# 3. Sanity check. |
| 111 | +if [ -x "$TC_PATH/bin/lean" ]; then |
| 112 | + log "ready — $("$TC_PATH/bin/lean" --version 2>/dev/null || echo '(version unavailable)')" |
| 113 | + log "next: eval \"\$($0 --print-path)\" then (cd $SCRIPT_DIR && lean Tangle.lean)" |
| 114 | +else |
| 115 | + echo "bootstrap-lean: toolchain bootstrap FAILED" >&2 |
| 116 | + exit 1 |
| 117 | +fi |
0 commit comments