build(bootstrap): make the SessionStart prover hook synchronous

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

Author: claude

.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"