build(bootstrap): make the SessionStart prover hook synchronous (#324)

## Summary

Flip `.claude/hooks/session-start.sh` from **async** to **synchronous**,
as requested. The session now blocks until Coq/Idris2/Zig are
provisioned, so the first prompt is **guaranteed** a working prover
instead of racing the background install.

## Why this is the right trade-off (not just a slower start)

The ~10–15 min Idris2 source build is paid **once on a cold container**.
Claude Code on the web **caches the container after the SessionStart
hook completes**, so every subsequent session hits the installers'
idempotent early-exits and starts fast — with the prover guarantee
intact each time. And because the installers are fail-soft + idempotent,
a cold build truncated by any hook timeout simply resumes on the next
session until the container is cached. Net: pay once, fast + guaranteed
thereafter.

## Change
- Removed the async opt-in (`{"async": true, ...}`) so the hook runs
synchronously.
- The verbose Idris2 build is redirected to
`$TMPDIR/ephapax-bootstrap.log`; only a one-line-per-prover summary
reaches the session transcript (no build spam).
- A header comment documents how to revert to async if the cold-start
wait is ever unwelcome.

Only `.claude/hooks/session-start.sh` changes; the installer scripts,
devcontainer, `.tool-versions`, and `just bootstrap` are untouched.

## Validated in-session
- Emits **no** async JSON (true sync mode).
- Runs `bootstrap-provers.sh` to completion and prints the
Coq/Idris2/Zig summary.
- **No-ops silently** when `CLAUDE_CODE_REMOTE` is unset (devcontainers
use postCreate instead).
- This environment confirms `CLAUDE_CODE_REMOTE=true`, so the remote
path is the one that fires.

## Hook execution mode
**Synchronous.** Pro: provers guaranteed before the first prompt (no
race). Con: first cold session waits for the build; amortized to ~0 by
container caching thereafter.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

---
_Generated by [Claude
Code](https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

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