Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 26, 2026
Merged

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 23 additions & 11 deletions .claude/hooks/session-start.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Loading