|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# |
| 4 | +# install-proof-toolchains.sh — self-provision the formal-proof toolchains that |
| 5 | +# ECHIDNA's proof corpus is checked with: Idris2, Agda (+stdlib), Coq, Lean 4. |
| 6 | +# |
| 7 | +# Idempotent: re-running skips already-present components in well under a second, |
| 8 | +# so it is safe to invoke from a SessionStart hook. The first run on a cold |
| 9 | +# container takes ~30 min (almost all of it the Idris2 source bootstrap). |
| 10 | +# |
| 11 | +# Target: Ubuntu 24.04 (the Claude-on-web / GitHub-Actions base). On any other |
| 12 | +# host, or without root, it prints a note and exits 0 rather than breaking the |
| 13 | +# session. |
| 14 | +set -euo pipefail |
| 15 | + |
| 16 | +LEAN_VERSION="4.13.0" |
| 17 | +IDRIS2_VERSION="v0.8.0" |
| 18 | +LEAN_PREFIX="/opt/lean-${LEAN_VERSION}-linux" |
| 19 | + |
| 20 | +log() { printf '\033[1;36m[proof-setup]\033[0m %s\n' "$*"; } |
| 21 | +have() { command -v "$1" >/dev/null 2>&1; } |
| 22 | + |
| 23 | +# ── Guards: only provision where it makes sense ────────────────────────────── |
| 24 | +if [ "$(id -u)" != "0" ] && ! have sudo; then |
| 25 | + log "not root and no sudo — skipping (provision manually if proofs are needed)"; exit 0 |
| 26 | +fi |
| 27 | +SUDO=""; [ "$(id -u)" = "0" ] || SUDO="sudo" |
| 28 | +if ! have apt-get; then |
| 29 | + log "no apt-get (not Debian/Ubuntu) — skipping"; exit 0 |
| 30 | +fi |
| 31 | + |
| 32 | +# Fast exit when everything is already present. |
| 33 | +if have idris2 && have agda && have coqc && [ -x "${LEAN_PREFIX}/bin/lean" ]; then |
| 34 | + log "all proof toolchains already present — nothing to do"; exit 0 |
| 35 | +fi |
| 36 | + |
| 37 | +# ── 1. APT base: agda, coq, chezscheme (for the Idris2 bootstrap), build deps ─ |
| 38 | +if ! have agda || ! have coqc || ! have chezscheme; then |
| 39 | + log "apt: disabling 403'ing third-party PPAs, then installing toolchains" |
| 40 | + for f in /etc/apt/sources.list.d/deadsnakes-*.sources /etc/apt/sources.list.d/ondrej-*.sources; do |
| 41 | + [ -f "$f" ] && $SUDO mv "$f" "$f.disabled" 2>/dev/null || true |
| 42 | + done |
| 43 | + $SUDO apt-get update -qq |
| 44 | + $SUDO apt-get install -y --no-install-recommends \ |
| 45 | + agda agda-stdlib coq chezscheme zstd build-essential libgmp-dev curl ca-certificates git |
| 46 | +fi |
| 47 | + |
| 48 | +# ── 2. Register agda-stdlib (Debian ships sources but no library registration) ─ |
| 49 | +STDLIB_LIB=/usr/share/agda-stdlib/standard-library.agda-lib |
| 50 | +if [ -d /usr/share/agda-stdlib ] && [ ! -f "$STDLIB_LIB" ]; then |
| 51 | + log "registering agda-stdlib" |
| 52 | + printf 'name: standard-library\ninclude: .\n' | $SUDO tee "$STDLIB_LIB" >/dev/null |
| 53 | +fi |
| 54 | +mkdir -p "$HOME/.agda" |
| 55 | +grep -qxF "$STDLIB_LIB" "$HOME/.agda/libraries" 2>/dev/null || echo "$STDLIB_LIB" >> "$HOME/.agda/libraries" |
| 56 | +grep -qxF 'standard-library' "$HOME/.agda/defaults" 2>/dev/null || echo 'standard-library' >> "$HOME/.agda/defaults" |
| 57 | +# Agda errors on Unicode identifiers (ℕ, ≤, …) under a C locale — always run it |
| 58 | +# as: LC_ALL=C.UTF-8 agda <file>.agda |
| 59 | +log "reminder: invoke agda with LC_ALL=C.UTF-8" |
| 60 | + |
| 61 | +# ── 3. Lean 4 (pinned tarball; the elan host 403s under the network policy) ─── |
| 62 | +if [ ! -x "${LEAN_PREFIX}/bin/lean" ]; then |
| 63 | + log "installing Lean ${LEAN_VERSION}" |
| 64 | + curl -fsSL "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" -o /tmp/lean.tar.zst |
| 65 | + $SUDO tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt |
| 66 | +fi |
| 67 | +for b in lean lake; do $SUDO ln -sf "${LEAN_PREFIX}/bin/$b" /usr/local/bin/"$b"; done |
| 68 | + |
| 69 | +# ── 4. Idris2 0.8.0 (not packaged; bootstrap from source via Chez, ~10 min) ─── |
| 70 | +if ! have idris2; then |
| 71 | + log "building Idris2 ${IDRIS2_VERSION} from source — this is the slow step" |
| 72 | + curl -fsSL "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VERSION}.tar.gz" -o /tmp/idris2.tar.gz |
| 73 | + rm -rf /tmp/idris2-src && mkdir -p /tmp/idris2-src |
| 74 | + tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1 |
| 75 | + ( cd /tmp/idris2-src \ |
| 76 | + && make bootstrap SCHEME=chezscheme \ |
| 77 | + && $SUDO make install PREFIX=/usr/local \ |
| 78 | + && $SUDO make install-with-src-libs PREFIX=/usr/local ) |
| 79 | +fi |
| 80 | + |
| 81 | +# ── 5. Report ──────────────────────────────────────────────────────────────── |
| 82 | +log "installed versions:" |
| 83 | +{ idris2 --version; agda --version; coqc --version | head -1; "${LEAN_PREFIX}/bin/lean" --version; } 2>/dev/null | sed 's/^/ /' || true |
| 84 | +log "proof toolchains ready (lteLit helper lives in verification/proofs/idris2/NatLte.idr)." |
| 85 | + |
| 86 | +# ── SOLVERS (maximal-scope stage) ──────────────────────────────────────────── |
| 87 | +# The solver corpus (proofs/{tptp,z3,cvc5,dimacs,acl2,hol_light,mizar,fstar}) |
| 88 | +# is provisioned by a sibling install-solvers.sh: z3/cvc5/eprover/vampire/spass/ |
| 89 | +# glpk/minizinc are cheap (apt + GitHub-release binaries); acl2/hol-light/mizar |
| 90 | +# are heavy source builds. Added when that stage begins. |
0 commit comments