diff --git a/.claude/hooks/session-start.sh b/.claude/hooks/session-start.sh new file mode 100755 index 00000000..8aa97c96 --- /dev/null +++ b/.claude/hooks/session-start.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Owner: Jonathan D.A. Jewell +# +# 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 diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 00000000..e06b0338 --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,14 @@ +{ + "hooks": { + "SessionStart": [ + { + "hooks": [ + { + "type": "command", + "command": "$CLAUDE_PROJECT_DIR/.claude/hooks/session-start.sh" + } + ] + } + ] + } +} diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 00000000..6d194192 --- /dev/null +++ b/.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}" + } +} diff --git a/.tool-versions b/.tool-versions index bb020dee..22aee9d7 100644 --- a/.tool-versions +++ b/.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 diff --git a/Justfile b/Justfile index 57769894..36b0208e 100644 --- a/Justfile +++ b/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 diff --git a/scripts/bootstrap-provers.sh b/scripts/bootstrap-provers.sh new file mode 100755 index 00000000..d9915084 --- /dev/null +++ b/scripts/bootstrap-provers.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Owner: Jonathan D.A. Jewell +# +# 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." diff --git a/scripts/install-coq.sh b/scripts/install-coq.sh new file mode 100755 index 00000000..57148da0 --- /dev/null +++ b/scripts/install-coq.sh @@ -0,0 +1,42 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Owner: Jonathan D.A. Jewell +# +# 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 diff --git a/scripts/install-idris2.sh b/scripts/install-idris2.sh new file mode 100755 index 00000000..a664e01a --- /dev/null +++ b/scripts/install-idris2.sh @@ -0,0 +1,75 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Owner: Jonathan D.A. Jewell +# +# 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 diff --git a/scripts/install-zig.sh b/scripts/install-zig.sh new file mode 100755 index 00000000..ea3aba19 --- /dev/null +++ b/scripts/install-zig.sh @@ -0,0 +1,56 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Owner: Jonathan D.A. Jewell +# +# 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 '?'))"