build(bootstrap): iser-style SessionStart prover bootstrap (Coq/Idris2/Zig)

.claude/hooks/session-start.sh

@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# SessionStart hook for Claude Code on the web. Bootstraps the formal-
+# methods provers (Coq / Idris2 / Zig) via scripts/bootstrap-provers.sh so
+# a fresh remote session can run the proofs without a manual install dance.
+#
+# ASYNC (non-blocking): the first stdout line opts into async mode, so the
+# session becomes usable immediately while the provers install in the
+# background. Coq (apt) and Zig (vendor binary) land in ~1–2 min; the
+# Idris2 source build takes ~10–15 min and finishes within asyncTimeout.
+# Everything is idempotent + fail-soft, so re-runs and blocked egress are
+# both safe. PATH for idris2 is persisted via $CLAUDE_ENV_FILE.
+
+set -uo pipefail
+
+# Opt into async so session startup is not blocked by the ~15-min Idris2 build.
+echo '{"async": true, "asyncTimeout": 1200000}'
+
+# Only meaningful in the remote (web) environment; devcontainers use the
+# postCreateCommand instead. No-op locally.
+if [ "${CLAUDE_CODE_REMOTE:-}" != "true" ]; then
+  exit 0
+fi
+
+exec "${CLAUDE_PROJECT_DIR:-.}/scripts/bootstrap-provers.sh" \
+  > "${TMPDIR:-/tmp}/ephapax-bootstrap.log" 2>&1

.claude/settings.json

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

.devcontainer/devcontainer.json

@@ -0,0 +1,12 @@
+{
+  "name": "ephapax",
+  "image": "mcr.microsoft.com/devcontainers/base:ubuntu-24.04",
+  "features": {
+    "ghcr.io/devcontainers/features/rust:1": {},
+    "ghcr.io/devcontainers/features/common-utils:2": {}
+  },
+  "postCreateCommand": "bash scripts/bootstrap-provers.sh",
+  "remoteEnv": {
+    "PATH": "${containerEnv:HOME}/.idris2/bin:${containerEnv:PATH}"
+  }
+}

.tool-versions

@@ -2,3 +2,11 @@
 # asdf tool versions for Ephapax development
 rust stable
 ocaml 5.4.1
+# Prover toolchain pins — the single source of truth the install scripts
+# default to (COQ_VERSION / IDRIS2_VERSION / ZIG_VERSION in
+# scripts/install-*.sh) and that CI mirrors. asdf/mise consume zig + idris2
+# directly; coq is provisioned via apt (noble ships exactly 8.18.0), kept
+# here only as the documented pin.
+coq 8.18.0
+idris2 0.7.0
+zig 0.14.0

Justfile

@@ -72,6 +72,12 @@ conformance:
 status-gate:
     ./scripts/status-gate.sh
 
+# Provision all provers (Coq / Idris2 / Zig) the -iser way: curl+tar from
+# vendor/codeload over HTTPS, never git; idempotent + fail-soft. Same entry
+# point the SessionStart hook and the devcontainer postCreate use.
+bootstrap:
+    bash scripts/bootstrap-provers.sh
+
 # Build Idris2 formal proofs
 idris-build:
     cd src/formal && idris2 --build ephapax-formal.ipkg

scripts/bootstrap-provers.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# bootstrap-provers.sh — one entry point that provisions every prover the
+# Ephapax proofs need, using the -iser doctrine (curl+tar from vendor /
+# codeload over HTTPS, never `git clone`; idempotent; fail-soft).
+#
+#   Coq 8.18   → formal/*.v            (scripts/install-coq.sh, apt)
+#   Idris2 0.7 → src/abi, src/formal   (scripts/install-idris2.sh, codeload)
+#   Zig 0.14   → tools/coproc/*.zig    (scripts/install-zig.sh, ziglang.org)
+#
+# Why this exists: a fresh Claude-Code-on-the-web container is re-cloned
+# from scratch, so the provers must be (re)installed per session. This is
+# invoked by the SessionStart hook (.claude/hooks/session-start.sh) and by
+# the devcontainer postCreateCommand, and can be run by hand (`just
+# bootstrap`).
+#
+# Fail-soft by construction: each installer exits 0 even on failure, so a
+# blocked egress domain degrades gracefully (that prover is simply absent)
+# rather than bricking startup. Idris2 is built from source (~10–15 min);
+# Coq (apt) and Zig (vendor binary) are quick.
+#
+# If CLAUDE_ENV_FILE is set (Claude Code on the web), the Idris2 bin dir is
+# persisted onto PATH for the rest of the session.
+
+set -uo pipefail
+
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+log() { printf '[bootstrap-provers] %s\n' "$*"; }
+
+# Put the Idris2 install dir on PATH up front so the installers' idempotency
+# checks see an already-installed idris2 and skip the ~15-min rebuild.
+export PATH="${PREFIX:-$HOME/.idris2}/bin:$PATH"
+
+log "begin — $(date -u 2>/dev/null || echo '?')"
+
+bash "$HERE/install-coq.sh"    || true
+bash "$HERE/install-zig.sh"    || true
+bash "$HERE/install-idris2.sh" || true
+
+# Persist Idris2 on PATH for the session (Claude Code on the web).
+IDRIS2_BIN="${PREFIX:-$HOME/.idris2}/bin"
+if [ -x "$IDRIS2_BIN/idris2" ] && [ -n "${CLAUDE_ENV_FILE:-}" ]; then
+  echo "export PATH=\"$IDRIS2_BIN:\$PATH\"" >> "$CLAUDE_ENV_FILE"
+  log "persisted $IDRIS2_BIN to \$CLAUDE_ENV_FILE"
+fi
+export PATH="$IDRIS2_BIN:$PATH"
+
+log "summary:"
+log "  coq:    $(command -v coqc   >/dev/null 2>&1 && coqc   --version 2>/dev/null | head -1 || echo 'absent')"
+log "  idris2: $(command -v idris2 >/dev/null 2>&1 && idris2 --version 2>/dev/null | head -1 || echo 'absent')"
+log "  zig:    $(command -v zig    >/dev/null 2>&1 && echo "zig $(zig version 2>/dev/null)"  || echo 'absent')"
+log "done."

scripts/install-coq.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# install-coq.sh — provision Coq for the Ephapax formal proofs (formal/).
+#
+# Coq is the one prover that needs no curl+tar dance: Ubuntu 24.04 (noble)
+# ships exactly 8.18.0 (`coq 8.18.0+dfsg`), the version pinned by
+# formal/Justfile, pixi.toml's [feature.proofs], and .github/workflows/
+# coq-build.yml. apt mirrors are not GitHub, so the git-protocol repo scope
+# does not apply.
+#
+# Doctrine (shared with install-zig.sh / install-idris2.sh): idempotent
+# (early-exit if the pinned version is present) and fail-soft (never block
+# setup or session start — exit 0 on failure with a diagnostic).
+
+set -uo pipefail
+
+COQ_VERSION="${COQ_VERSION:-8.18.0}"
+note() { printf '[install-coq] %s\n' "$*" >&2; }
+
+if command -v coqc >/dev/null 2>&1; then
+  have="$(coqc --version 2>/dev/null | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1)"
+  if [ "$have" = "$COQ_VERSION" ]; then
+    note "coqc $COQ_VERSION already installed — skipping."
+    exit 0
+  fi
+  note "coqc present but version '$have' != '$COQ_VERSION' — (re)installing via apt."
+fi
+
+if ! command -v apt-get >/dev/null 2>&1; then
+  note "apt-get unavailable — install Coq $COQ_VERSION another way (opam/nix). Skipping (non-blocking)."
+  exit 0
+fi
+
+sudo apt-get update -qq || note "apt update failed (continuing)"
+if sudo apt-get install -y --no-install-recommends coq; then
+  note "installed: $(coqc --version 2>/dev/null | head -1)"
+else
+  note "apt install of coq failed — skipping (non-blocking)."
+  exit 0
+fi

scripts/install-idris2.sh

@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# install-idris2.sh — provision Idris2 for the Ephapax ABI + formal proofs
+# (src/abi/ephapax-abi.ipkg, src/formal/ephapax-formal.ipkg).
+#
+# Follows the `iseriser/scripts/install-zig.sh` doctrine:
+#   * curl + tar over HTTPS — NEVER `git clone`. The agent/CI proxy
+#     scopes the GIT protocol to one repo (so `git clone idris-lang/Idris2`
+#     → 403), but allowlists HTTPS to github.com / codeload.github.com.
+#     A source *tarball* from codeload is a normal HTTPS GET → 200.
+#   * pinned version (IDRIS2_VERSION), idempotent (early-exit if present),
+#   * fail-soft: a missing Idris2 must NOT block setup or session start
+#     (exit 0 on any fetch/build failure, with a diagnostic).
+#
+# Egress note: codeload.github.com is allowlisted by default. If your
+# environment's proxy is stricter, add `codeload.github.com` to the
+# HTTPS egress allowlist (same way ziglang.org is added for zig).
+
+set -uo pipefail
+
+IDRIS2_VERSION="${IDRIS2_VERSION:-0.7.0}"
+PREFIX="${PREFIX:-$HOME/.idris2}"
+SCHEME="${SCHEME:-chezscheme}"
+
+note() { printf '[install-idris2] %s\n' "$*" >&2; }
+
+# Idempotent: already the pinned version? Check both PATH *and* the install
+# location ($PREFIX/bin/idris2). The latter matters because callers may run
+# this before adding $PREFIX/bin to PATH, and we must NOT trigger a ~15-min
+# rebuild when idris2 is already installed.
+existing="$(command -v idris2 2>/dev/null || true)"
+[ -z "$existing" ] && [ -x "$PREFIX/bin/idris2" ] && existing="$PREFIX/bin/idris2"
+if [ -n "$existing" ]; then
+  have="$("$existing" --version 2>/dev/null | grep -oE '[0-9]+\.[0-9]+\.[0-9]+' | head -1)"
+  if [ "$have" = "$IDRIS2_VERSION" ]; then
+    note "idris2 $IDRIS2_VERSION already installed ($existing) — skipping."
+    exit 0
+  fi
+fi
+
+# Backend + C deps from apt (no cross-repo network). These are the two
+# that bit us the first time: chezscheme (the codegen backend) and
+# libgmp-dev (gmp.h, needed by the refc support lib at `make install`).
+if command -v apt-get >/dev/null 2>&1; then
+  sudo apt-get update -qq || note "apt update failed (continuing)"
+  sudo apt-get install -y --no-install-recommends \
+    "$SCHEME" libgmp-dev make gcc curl || note "apt install of backend deps failed"
+fi
+if ! command -v "$SCHEME" >/dev/null 2>&1; then
+  note "Chez Scheme ($SCHEME) unavailable — cannot build Idris2. Skipping (non-blocking)."
+  exit 0
+fi
+
+work="$(mktemp -d)"; trap 'rm -rf "$work"' EXIT
+url="https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}"
+note "fetching Idris2 ${IDRIS2_VERSION} source via HTTPS (curl, not git): $url"
+if ! curl -fsSL -o "$work/idris2.tar.gz" "$url"; then
+  note "download failed (proxy/egress?). Skipping — session start not blocked."
+  exit 0
+fi
+tar -xzf "$work/idris2.tar.gz" -C "$work" || { note "extract failed — skipping."; exit 0; }
+src="$work/Idris2-${IDRIS2_VERSION}"
+
+note "bootstrapping (SCHEME=$SCHEME, PREFIX=$PREFIX) …"
+if make -C "$src" bootstrap SCHEME="$SCHEME" PREFIX="$PREFIX" \
+   && make -C "$src" install PREFIX="$PREFIX"; then
+  note "installed → $PREFIX/bin/idris2"
+  note "add to PATH:  export PATH=\"$PREFIX/bin:\$PATH\""
+  "$PREFIX/bin/idris2" --version >&2 || true
+else
+  note "build/install failed — skipping (non-blocking). See logs above."
+  exit 0
+fi

scripts/install-zig.sh

@@ -0,0 +1,56 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# install-zig.sh — provision Zig for ephapax's coprocessor seam
+# (`just build-coproc`, tools/coproc/*.zig; pixi.toml wants zig >= 0.13).
+#
+# Ported from hyperpolymath/iseriser/scripts/install-zig.sh. The doctrine:
+#   * fetch a PINNED prebuilt binary by curl+tar straight from the vendor
+#     (ziglang.org) — never a package manager, never git;
+#   * idempotent (early-exit if the pinned version is already on PATH);
+#   * fail-soft: a missing Zig must NOT block setup or session start.
+#
+# Egress note: github.com is allowlisted by the agent/CI proxy by default,
+# but ziglang.org must be added to the HTTPS egress allowlist explicitly.
+# If it is not reachable, this script logs and exits 0 (non-blocking).
+
+set -uo pipefail
+
+ZIG_VERSION="${ZIG_VERSION:-0.14.0}"
+PREFIX="${PREFIX:-/usr/local}"
+note() { printf '[install-zig] %s\n' "$*" >&2; }
+
+if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then
+  note "zig $ZIG_VERSION already installed — skipping."
+  exit 0
+fi
+
+case "$(uname -m)" in
+  x86_64|amd64) zarch=x86_64 ;;
+  aarch64|arm64) zarch=aarch64 ;;
+  *) note "unsupported arch $(uname -m) — install zig $ZIG_VERSION manually. Skipping."; exit 0 ;;
+esac
+case "$(uname -s)" in
+  Linux)  zos=linux ;;
+  Darwin) zos=macos ;;
+  *) note "unsupported OS $(uname -s) — install zig $ZIG_VERSION manually. Skipping."; exit 0 ;;
+esac
+
+tarball="zig-${zos}-${zarch}-${ZIG_VERSION}.tar.xz"
+url="https://ziglang.org/download/${ZIG_VERSION}/${tarball}"
+work="$(mktemp -d)"; trap 'rm -rf "$work"' EXIT
+
+note "fetching $url"
+if ! curl -fsSL -o "$work/$tarball" "$url"; then
+  note "download failed (ziglang.org not allowlisted?). Skipping — session start not blocked."
+  exit 0
+fi
+tar -xJf "$work/$tarball" -C "$work" || { note "extract failed — skipping."; exit 0; }
+
+dest="${PREFIX}/lib/zig-${ZIG_VERSION}"
+sudo rm -rf "$dest"
+sudo mkdir -p "${PREFIX}/lib" "${PREFIX}/bin"
+sudo mv "$work/zig-${zos}-${zarch}-${ZIG_VERSION}" "$dest"
+sudo ln -sf "${dest}/zig" "${PREFIX}/bin/zig"
+note "installed → ${PREFIX}/bin/zig ($(zig version 2>/dev/null || echo '?'))"