From 56838f57c9aec10d6ce31be6fc0758de22b1311a Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 22:43:59 +0000 Subject: [PATCH] build(bootstrap): make the SessionStart prover hook synchronous MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flip .claude/hooks/session-start.sh from async to synchronous so session start blocks until Coq/Idris2/Zig are provisioned — the first prompt is guaranteed a working prover instead of racing the background install. The ~10-15 min Idris2 source build is paid once on a cold container; Claude Code on the web caches the container after the hook completes, so subsequent sessions hit the idempotent early-exits and start fast. Still fail-soft + idempotent, so a timeout-truncated cold build just resumes on the next session until the container is cached. The verbose build is logged to a file; only a one-line-per-prover summary reaches the transcript. Validated in-session: emits no async JSON; runs bootstrap to completion; prints the prover summary; no-ops silently when CLAUDE_CODE_REMOTE is unset. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL --- .claude/hooks/session-start.sh | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/.claude/hooks/session-start.sh b/.claude/hooks/session-start.sh index 8aa97c96..2c4a84b7 100755 --- a/.claude/hooks/session-start.sh +++ b/.claude/hooks/session-start.sh @@ -6,23 +6,35 @@ # 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. +# SYNCHRONOUS (blocking): the session does not start until the provers are +# provisioned, so the first prompt is GUARANTEED a working Coq/Idris2/Zig +# (no race where Claude runs a proof before its prover exists). The heavy +# Idris2 source build (~10–15 min) is paid ONCE on a cold container; Claude +# Code on the web caches the container after the hook completes, so every +# later session hits the idempotent early-exits and starts fast. Everything +# is fail-soft, so a blocked egress domain degrades gracefully instead of +# wedging startup; and because the installers are idempotent, a hook cut +# short by any timeout simply resumes on the next session until cached. +# PATH for idris2 is persisted via $CLAUDE_ENV_FILE. +# +# (To return to non-blocking startup, restore async mode by emitting +# `{"async": true, "asyncTimeout": 1200000}` as the first stdout line.) 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 +LOG="${TMPDIR:-/tmp}/ephapax-bootstrap.log" +echo "[session-start] Provisioning provers (Coq/Idris2/Zig) before the session starts." +echo "[session-start] First cold start builds Idris2 (~10-15 min, then cached). Full log: $LOG" + +# Run synchronously; keep the verbose Idris2 build out of the session +# transcript by logging to a file, then surface a one-line-per-prover summary. +"${CLAUDE_PROJECT_DIR:-.}/scripts/bootstrap-provers.sh" > "$LOG" 2>&1 || true + +echo "[session-start] Prover bootstrap finished:" +grep -E '^\[bootstrap-provers\] (coq|idris2|zig):' "$LOG" || tail -n 3 "$LOG"