|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 4 | +# |
| 5 | +# On-demand provisioning of the prover / solver toolchains ArghDA drives. |
| 6 | +# Companion to hyperpolymath/echo-types scripts/provision-agda.sh, widened to |
| 7 | +# the full multi-backend set. Idempotent: safe to re-run; skips anything already |
| 8 | +# present. |
| 9 | +# |
| 10 | +# HONESTY CONTRACT (load-bearing — see arghda-core AGENTIC.a2ml): |
| 11 | +# A tool is only ever reported "OK" if its own `--version` (or equivalent) |
| 12 | +# actually returned exit 0 in THIS run. Anything else is reported MISSING or |
| 13 | +# FAILED with the command that was tried. The script never claims an install |
| 14 | +# it did not verify. |
| 15 | +# |
| 16 | +# Tiers: |
| 17 | +# default (tractable, installed now): agda(+stdlib +cubical lib), zig, |
| 18 | +# idris2, lean4, z3, cvc5 |
| 19 | +# --heavy (adds): coq/rocq (opam), isabelle (~4 GB) |
| 20 | +# --mizar (adds): mizar (niche; distribution uncertain) |
| 21 | +# --all: everything above |
| 22 | +# --verify-only: skip installs, just run the doctor table |
| 23 | +# |
| 24 | +# Usage: bash scripts/provision-provers.sh [--heavy] [--mizar] [--all] [--verify-only] |
| 25 | +set -uo pipefail # NB: no -e; we tolerate per-tool failure and report it. |
| 26 | + |
| 27 | +log() { echo "[provision] $*"; } |
| 28 | +warn() { echo "[provision] WARN: $*" >&2; } |
| 29 | +have() { command -v "$1" >/dev/null 2>&1; } |
| 30 | + |
| 31 | +# ---- Pinned versions (reused from the estate where a precedent exists) ------- |
| 32 | +STDLIB_TAG="v2.3" # echo-types pin |
| 33 | +ZIG_VER="0.15.2" # boj-server setup-zig pin |
| 34 | +IDRIS2_TAG="v0.7.0" # standards/a2ml CI pin |
| 35 | +LEAN_VER="v4.13.0" # tropical-resource-typing lean-toolchain |
| 36 | +CVC5_VER="1.2.0" # cvc5 static-binary release |
| 37 | +COQ_VER="8.18.0" # opam (with --heavy) |
| 38 | +ISABELLE_VER="Isabelle2024" # TUM tarball (with --heavy) |
| 39 | + |
| 40 | +STDLIB_DIR=/opt/agda-stdlib |
| 41 | +CUBICAL_DIR=/opt/agda-cubical |
| 42 | +ZIG_DIR=/opt/zig |
| 43 | +IDRIS2_SRC=/opt/Idris2 |
| 44 | +AGDA_HOME="${HOME}/.agda" |
| 45 | + |
| 46 | +WANT_HEAVY=0; WANT_MIZAR=0; VERIFY_ONLY=0 |
| 47 | +for a in "$@"; do case "$a" in |
| 48 | + --heavy) WANT_HEAVY=1 ;; |
| 49 | + --mizar) WANT_MIZAR=1 ;; |
| 50 | + --all) WANT_HEAVY=1; WANT_MIZAR=1 ;; |
| 51 | + --verify-only) VERIFY_ONLY=1 ;; |
| 52 | + *) warn "unknown flag: $a" ;; |
| 53 | +esac; done |
| 54 | + |
| 55 | +apt_get() { DEBIAN_FRONTEND=noninteractive apt-get "$@"; } |
| 56 | + |
| 57 | +# ============================================================================= |
| 58 | +# Installers — each best-effort, never aborts the script. |
| 59 | +# ============================================================================= |
| 60 | + |
| 61 | +install_agda() { |
| 62 | + have agda && { log "agda present: $(agda --version 2>&1 | head -1)"; return; } |
| 63 | + log "installing agda (apt agda-bin)…" |
| 64 | + apt_get update -qq || true |
| 65 | + apt_get install -y agda-bin >/dev/null 2>&1 || apt_get install -y agda >/dev/null 2>&1 || \ |
| 66 | + warn "apt could not install agda" |
| 67 | +} |
| 68 | + |
| 69 | +# NB: this environment's proxy routes `git clone` through a git-relay that only |
| 70 | +# permits the session's scoped repos (third-party clones return HTTP 403), but |
| 71 | +# plain `curl` to GitHub archive tarballs works. So all third-party sources are |
| 72 | +# fetched as release/branch tarballs, which is also more portable than a clone. |
| 73 | +fetch_tarball() { # fetch_tarball <url> <dest-dir> |
| 74 | + local url="$1" dest="$2" tmp="/tmp/arghda-fetch-$$.tar.gz" |
| 75 | + curl -fsSL "$url" -o "$tmp" 2>/dev/null && [ -s "$tmp" ] || { rm -f "$tmp"; return 1; } |
| 76 | + rm -rf "$dest"; mkdir -p "$dest" |
| 77 | + tar -xzf "$tmp" -C "$dest" --strip-components=1; local rc=$? |
| 78 | + rm -f "$tmp"; return $rc |
| 79 | +} |
| 80 | + |
| 81 | +install_agda_stdlib() { |
| 82 | + if [ -f "${STDLIB_DIR}/standard-library.agda-lib" ]; then |
| 83 | + log "agda-stdlib present at ${STDLIB_DIR}"; return |
| 84 | + fi |
| 85 | + log "fetching agda-stdlib ${STDLIB_TAG} tarball…" |
| 86 | + if fetch_tarball "https://github.com/agda/agda-stdlib/archive/refs/tags/${STDLIB_TAG}.tar.gz" "${STDLIB_DIR}"; then |
| 87 | + sed -i 's/^name: standard-library-.*/name: standard-library/' \ |
| 88 | + "${STDLIB_DIR}/standard-library.agda-lib" || true |
| 89 | + log "agda-stdlib ${STDLIB_TAG} ready" |
| 90 | + else |
| 91 | + warn "agda-stdlib tarball fetch failed" |
| 92 | + fi |
| 93 | +} |
| 94 | + |
| 95 | +# Cubical Agda is the `--cubical` FLAG (ships with the agda binary — free). |
| 96 | +# The agda/cubical LIBRARY (HIT stdlib) is optional and version-sensitive; |
| 97 | +# best-effort fetch, never fatal. |
| 98 | +install_agda_cubical() { |
| 99 | + [ -d "${CUBICAL_DIR}" ] && { log "agda/cubical library present"; return; } |
| 100 | + log "fetching agda/cubical library tarball (best-effort)…" |
| 101 | + fetch_tarball "https://github.com/agda/cubical/archive/refs/heads/master.tar.gz" "${CUBICAL_DIR}" \ |
| 102 | + || warn "agda/cubical fetch failed (the --cubical flag still works without the library)" |
| 103 | +} |
| 104 | + |
| 105 | +register_agda_libraries() { |
| 106 | + mkdir -p "${AGDA_HOME}" |
| 107 | + { |
| 108 | + [ -f "${STDLIB_DIR}/standard-library.agda-lib" ] && echo "${STDLIB_DIR}/standard-library.agda-lib" |
| 109 | + [ -f "${CUBICAL_DIR}/cubical.agda-lib" ] && echo "${CUBICAL_DIR}/cubical.agda-lib" |
| 110 | + for cand in /home/user/absolute-zero/absolute-zero.agda-lib \ |
| 111 | + "${HOME}/absolute-zero/absolute-zero.agda-lib"; do |
| 112 | + [ -f "$cand" ] && echo "$cand" |
| 113 | + done |
| 114 | + } > "${AGDA_HOME}/libraries" |
| 115 | + echo "standard-library" > "${AGDA_HOME}/defaults" |
| 116 | + log "registered ~/.agda/libraries:"; sed 's/^/ /' "${AGDA_HOME}/libraries" |
| 117 | +} |
| 118 | + |
| 119 | +install_zig() { |
| 120 | + have zig && { log "zig present: $(zig version 2>&1)"; return; } |
| 121 | + log "installing zig ${ZIG_VER}…" |
| 122 | + local base="https://ziglang.org/download/${ZIG_VER}" |
| 123 | + # Asset naming flipped arch/os around 0.14; try both. |
| 124 | + for name in "zig-x86_64-linux-${ZIG_VER}" "zig-linux-x86_64-${ZIG_VER}"; do |
| 125 | + if curl -fsSL "${base}/${name}.tar.xz" -o /tmp/zig.tar.xz 2>/dev/null; then |
| 126 | + rm -rf "${ZIG_DIR}"; mkdir -p "${ZIG_DIR}" |
| 127 | + tar -xJf /tmp/zig.tar.xz -C "${ZIG_DIR}" --strip-components=1 \ |
| 128 | + && ln -sf "${ZIG_DIR}/zig" /usr/local/bin/zig && { log "zig unpacked (${name})"; return; } |
| 129 | + fi |
| 130 | + done |
| 131 | + warn "zig download failed for both asset-name patterns at ${base}" |
| 132 | +} |
| 133 | + |
| 134 | +install_lean() { |
| 135 | + export PATH="${HOME}/.elan/bin:${PATH}" |
| 136 | + have lean && { log "lean present: $(lean --version 2>&1)"; return; } |
| 137 | + log "installing lean ${LEAN_VER} via elan…" |
| 138 | + if curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan.sh 2>/dev/null; then |
| 139 | + sh /tmp/elan.sh -y --default-toolchain "leanprover/lean4:${LEAN_VER}" >/dev/null 2>&1 \ |
| 140 | + || warn "elan install failed" |
| 141 | + else |
| 142 | + warn "could not fetch elan-init.sh" |
| 143 | + fi |
| 144 | +} |
| 145 | + |
| 146 | +# Idris2 is a CORE estate language (owns ABIs) — install via Chez bootstrap. |
| 147 | +install_idris2() { |
| 148 | + export PATH="${HOME}/.idris2/bin:${PATH}" |
| 149 | + have idris2 && { log "idris2 present: $(idris2 --version 2>&1)"; return; } |
| 150 | + log "installing idris2 ${IDRIS2_TAG} (chez bootstrap)…" |
| 151 | + have scheme || have chez || have chezscheme || apt_get install -y chezscheme >/dev/null 2>&1 || \ |
| 152 | + warn "could not install chezscheme (idris2 bootstrap needs a Chez Scheme)" |
| 153 | + local sch="" |
| 154 | + for c in chezscheme chez scheme; do have "$c" && { sch="$c"; break; }; done |
| 155 | + [ -z "$sch" ] && { warn "no Chez Scheme found; skipping idris2"; return; } |
| 156 | + if [ ! -f "${IDRIS2_SRC}/Makefile" ]; then |
| 157 | + fetch_tarball "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_TAG}.tar.gz" "${IDRIS2_SRC}" \ |
| 158 | + || { warn "idris2 tarball fetch failed"; return; } |
| 159 | + fi |
| 160 | + ( cd "${IDRIS2_SRC}" \ |
| 161 | + && make bootstrap SCHEME="${sch}" >/tmp/idris2-build.log 2>&1 \ |
| 162 | + && make install PREFIX="${HOME}/.idris2" >>/tmp/idris2-build.log 2>&1 ) \ |
| 163 | + || warn "idris2 build failed (see /tmp/idris2-build.log)" |
| 164 | +} |
| 165 | + |
| 166 | +install_z3() { |
| 167 | + have z3 && { log "z3 present: $(z3 --version 2>&1)"; return; } |
| 168 | + log "installing z3 (apt)…" |
| 169 | + apt_get install -y z3 >/dev/null 2>&1 || warn "apt could not install z3" |
| 170 | +} |
| 171 | + |
| 172 | +install_cvc5() { |
| 173 | + have cvc5 && { log "cvc5 present: $(cvc5 --version 2>&1 | head -1)"; return; } |
| 174 | + log "installing cvc5 ${CVC5_VER}…" |
| 175 | + have unzip || apt_get install -y unzip >/dev/null 2>&1 || true |
| 176 | + local base="https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}" |
| 177 | + # Single static binary first, then the zipped variant. |
| 178 | + if curl -fsSL "${base}/cvc5-Linux-x86_64-static" -o /usr/local/bin/cvc5 2>/dev/null \ |
| 179 | + && [ -s /usr/local/bin/cvc5 ]; then |
| 180 | + chmod +x /usr/local/bin/cvc5; log "cvc5 binary installed"; return |
| 181 | + fi |
| 182 | + for asset in "cvc5-Linux-x86_64-static.zip" "cvc5-Linux-static.zip" "cvc5-Linux.zip"; do |
| 183 | + if curl -fsSL "${base}/${asset}" -o /tmp/cvc5.zip 2>/dev/null && [ -s /tmp/cvc5.zip ]; then |
| 184 | + rm -rf /tmp/cvc5d; mkdir -p /tmp/cvc5d && unzip -q /tmp/cvc5.zip -d /tmp/cvc5d 2>/dev/null || continue |
| 185 | + local bin; bin="$(find /tmp/cvc5d -type f -name cvc5 | head -1)" |
| 186 | + [ -n "$bin" ] && { install -m755 "$bin" /usr/local/bin/cvc5; log "cvc5 installed (${asset})"; return; } |
| 187 | + fi |
| 188 | + done |
| 189 | + warn "cvc5 download failed for all known asset names at ${base}" |
| 190 | +} |
| 191 | + |
| 192 | +# ---- Heavy (opt-in) --------------------------------------------------------- |
| 193 | +install_coq() { |
| 194 | + have coqc && { log "coq present: $(coqc --version 2>&1 | head -1)"; return; } |
| 195 | + log "installing coq ${COQ_VER} via opam (heavy)…" |
| 196 | + if ! have opam; then |
| 197 | + apt_get install -y opam >/dev/null 2>&1 || { warn "opam unavailable"; return; } |
| 198 | + fi |
| 199 | + opam init --disable-sandboxing -y >/dev/null 2>&1 || true |
| 200 | + eval "$(opam env 2>/dev/null)" || true |
| 201 | + opam install -y "coq.${COQ_VER}" >/tmp/coq-build.log 2>&1 || warn "opam coq install failed (see /tmp/coq-build.log)" |
| 202 | +} |
| 203 | + |
| 204 | +install_isabelle() { |
| 205 | + have isabelle && { log "isabelle present"; return; } |
| 206 | + log "installing ${ISABELLE_VER} (heavy, ~4 GB)…" |
| 207 | + local url="https://isabelle.in.tum.de/dist/${ISABELLE_VER}_linux.tar.gz" |
| 208 | + if curl -fsSL "$url" -o /tmp/isabelle.tar.gz 2>/dev/null && [ -s /tmp/isabelle.tar.gz ]; then |
| 209 | + tar -xzf /tmp/isabelle.tar.gz -C /opt \ |
| 210 | + && ln -sf "/opt/${ISABELLE_VER}/bin/isabelle" /usr/local/bin/isabelle \ |
| 211 | + && log "isabelle unpacked" || warn "isabelle unpack failed" |
| 212 | + else |
| 213 | + warn "isabelle download failed: ${url}" |
| 214 | + fi |
| 215 | +} |
| 216 | + |
| 217 | +install_mizar() { |
| 218 | + have mizar && { log "mizar present"; return; } |
| 219 | + warn "mizar not auto-installed: distribution is manual (mizar.org). Flagged as UNKNOWN." |
| 220 | +} |
| 221 | + |
| 222 | +# ============================================================================= |
| 223 | +# Honest verification / doctor table. |
| 224 | +# ============================================================================= |
| 225 | +declare -a REPORT |
| 226 | +verify() { # verify <label> <cmd...> |
| 227 | + local label="$1"; shift |
| 228 | + local full rc line |
| 229 | + full="$("$@" 2>&1)"; rc=$? # rc is the tool's, not a pipe's |
| 230 | + # Prefer the first substantive line over toolchain warnings. |
| 231 | + line="$(printf '%s\n' "$full" | grep -viE 'warning|could not canonicalize|toolchains' | head -1)" |
| 232 | + [ -z "$line" ] && line="$(printf '%s\n' "$full" | head -1)" |
| 233 | + if [ "$rc" -eq 0 ] && [ -n "$line" ]; then |
| 234 | + REPORT+=("OK | ${label} | ${line}") |
| 235 | + else |
| 236 | + REPORT+=("MISSING | ${label} | (—)") |
| 237 | + fi |
| 238 | +} |
| 239 | + |
| 240 | +run_doctor() { |
| 241 | + export PATH="${HOME}/.elan/bin:${HOME}/.idris2/bin:${PATH}" |
| 242 | + eval "$(opam env 2>/dev/null)" || true |
| 243 | + REPORT=() |
| 244 | + verify "agda" agda --version |
| 245 | + verify "idris2" idris2 --version |
| 246 | + verify "lean" lean --version |
| 247 | + verify "z3" z3 --version |
| 248 | + verify "cvc5" cvc5 --version |
| 249 | + verify "zig" zig version |
| 250 | + verify "coqc" coqc --version |
| 251 | + verify "isabelle" isabelle version |
| 252 | + [ -f "${CUBICAL_DIR}/cubical.agda-lib" ] \ |
| 253 | + && REPORT+=("OK | cubical-lib | ${CUBICAL_DIR}") \ |
| 254 | + || REPORT+=("MISSING | cubical-lib | (flag --cubical still works without it)") |
| 255 | + echo |
| 256 | + echo "=== arghda doctor: backend availability (verified this run) ===" |
| 257 | + printf '%s\n' "${REPORT[@]}" | column -t -s '|' 2>/dev/null || printf '%s\n' "${REPORT[@]}" |
| 258 | + echo "===============================================================" |
| 259 | +} |
| 260 | + |
| 261 | +# ============================================================================= |
| 262 | +main() { |
| 263 | + if [ "${VERIFY_ONLY}" -eq 0 ]; then |
| 264 | + # Fast / reliable first; slow chez-bootstrap (idris2) last so it can never |
| 265 | + # block the others. |
| 266 | + install_agda |
| 267 | + install_agda_stdlib |
| 268 | + install_agda_cubical |
| 269 | + register_agda_libraries |
| 270 | + install_zig |
| 271 | + install_z3 |
| 272 | + install_cvc5 |
| 273 | + install_lean |
| 274 | + install_idris2 |
| 275 | + if [ "${WANT_HEAVY}" -eq 1 ]; then install_coq; install_isabelle; fi |
| 276 | + if [ "${WANT_MIZAR}" -eq 1 ]; then install_mizar; fi |
| 277 | + fi |
| 278 | + run_doctor |
| 279 | +} |
| 280 | +main |
0 commit comments