Skip to content

build(bootstrap): iser-style SessionStart prover bootstrap (Coq/Idris2/Zig)#323

Merged
hyperpolymath merged 3 commits into
mainfrom
claude/prover-bootstrap-iser
Jun 26, 2026
Merged

build(bootstrap): iser-style SessionStart prover bootstrap (Coq/Idris2/Zig)#323
hyperpolymath merged 3 commits into
mainfrom
claude/prover-bootstrap-iser

Conversation

@hyperpolymath

@hyperpolymath hyperpolymath commented Jun 26, 2026

Copy link
Copy Markdown
Owner

Summary

Make a fresh Claude-Code-on-the-web (or devcontainer) session come up prover-ready, using the hyperpolymath/iseriser bootstrap doctrine. No more manual apt/build dance, and no more "403 mystery."

Why this works (the 403, explained)

The agent/CI proxy has two independent gates:

  1. Git-protocol repo allowlist — scoped to hyperpolymath/ephapax. This is what 403s cargo's typed-wasm git dep and git clone idris-lang/Idris2.
  2. HTTPS egress domain allowlist — github.com / codeload.github.com / raw.githubusercontent.com / ziglang.org all return 200.

So the fix (the iser doctrine, documented in ephapaxiser/scripts/install-zig.sh) is: fetch every toolchain by curl+tar over HTTPS, never git clone. Idris2 was never unreachable — it just needs its source tarball from codeload, not a git clone.

What's here

Scripts — idempotent + fail-soft (a blocked egress domain degrades that one prover, never bricks startup):

  • scripts/install-coq.sh — apt (noble ships exactly 8.18.0, the pinned version)
  • scripts/install-zig.sh — ziglang.org vendor tarball (ported near-verbatim from iseriser)
  • scripts/install-idris2.sh — codeload source tarball + chezscheme/libgmp-dev, bootstrap-built. Idempotent via the install location ($PREFIX/bin/idris2), not just PATH — so it never re-triggers the ~15-min rebuild.
  • scripts/bootstrap-provers.sh — one entry point; persists idris2 on PATH via $CLAUDE_ENV_FILE.

Triggers (both, as requested):

  • .claude/hooks/session-start.sh + .claude/settings.json — async SessionStart hook for Claude Code on the web. Non-blocking: session is usable immediately; Coq + Zig land in ~1–2 min, the Idris2 build finishes in the background within asyncTimeout.
  • .devcontainer/devcontainer.json postCreateCommand — for devcontainers / Codespaces (synchronous).
  • just bootstrap — manual entry point.
  • .tool-versions — pins coq 8.18.0 / idris2 0.7.0 / zig 0.14.0.

Validated in-session

  • Fresh Zig 0.14.0 install from ziglang.org → success (proves the vendor-binary path through the proxy).
  • Coq 8.18.0 + Idris2 0.7.0 idempotent-skip (no rebuild) — including under a clean PATH (the bug the install-location check fixes).
  • SessionStart hook emits valid async JSON and execs the bootstrap.
  • With the bootstrapped toolchain: src/formal + src/abi (idris2), formal/Modality.v (coqc), and the zig coproc test all build.

Hook execution mode

Asynchronous (you asked for non-blocking, given the ~15-min Idris2 build).

  • Pro: session starts immediately; provers provision in the background.
  • Con: a step that needs a prover in the first ~15 min may briefly find it absent (fail-soft, so it just retries). Happy to switch the hook to synchronous if you'd rather guarantee provers-before-prompt.

Once merged to the default branch, all future web sessions use it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

Generated by Claude Code

claude added 2 commits June 26, 2026 21:10
@claude
proof(L1): close ADMIT 2 — remove the false region_liveness lemma via…
7bceee6 
… the honest val_region_no_exit reformulation

The provably-false region_liveness_at_split_l1_gen (asserting
In rv R -> In rv R' unconditionally; false in the T_Region_Active_L1
r = rv sub-case, witness ERegion rv (EI32 5) at R = [rv]) is removed.
Its 13 consumers in subst_typing_gen_l1_m now route region liveness
through the TRUE, Qed region_liveness_no_exit_l1_gen, supplied with a
new honest premise val_region_no_exit threaded through the substitution
chain (subst_typing_gen_l1_m / subst_typing_gen_l1 /
subst_preserves_typing_l1) and the L2 beta-case lemmas
(preservation_l2_app_eff_beta_linear / _l1).

Verified by rebuilt coqc 8.18.0 + Print Assumptions:
- formal/ outer Admitted: 4 -> 3. region_liveness removed; only the
  sacrosanct legacy Semantics.v preservation, step_pop, and the
  preservation_l1 capstone remain.
- The substitution chain and both L2 beta-case lemmas flip from
  "depends on a false axiom" to "Closed under the global context"
  (axiom-free, carrying the honest premise instead).
- preservation_l3 stays unconditionally axiom-free.

This is the sanctioned honest closure recorded in Semantics_L1.v's
2026-06-16 call-site audit and PROOF-NEEDS.md, not ad-hoc patching of
the legacy judgment.

Also corrects the PROOF-NEEDS.md §4 status-gate marker to ground truth
(was 5, now 3; scripts/status-gate.sh --proofs passes) and reconciles
the per-file table + the in-source audit comments.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
@claude
build(bootstrap): iser-style SessionStart prover bootstrap (Coq/Idris…
dec2259 
…2/Zig)

Provision the three provers the Ephapax proofs need without a manual install
dance, using the hyperpolymath/iseriser doctrine: fetch each toolchain by
curl+tar over HTTPS (vendor domain / codeload), never `git clone`. That
sidesteps the proxy's git-protocol repo scoping (which 403s non-ephapax
repos) while staying on the allowlisted HTTPS egress.

Scripts (idempotent + fail-soft):
- scripts/install-coq.sh     apt (noble ships exactly 8.18.0)
- scripts/install-zig.sh     ziglang.org vendor tarball (ported from iseriser)
- scripts/install-idris2.sh  codeload source tarball + chezscheme/libgmp-dev,
                             bootstrap-built; idempotent via the install
                             LOCATION (not just PATH) so it never re-builds
- scripts/bootstrap-provers.sh  one entry point; persists idris2 on PATH via
                             $CLAUDE_ENV_FILE

Triggers (both, per request):
- .claude/hooks/session-start.sh + .claude/settings.json  async SessionStart
  hook for Claude Code on the web (non-blocking: the ~15-min idris2 build runs
  in the background; Coq + Zig land in ~1-2 min)
- .devcontainer/devcontainer.json postCreateCommand  for devcontainers/Codespaces
- just bootstrap  manual entry point
- .tool-versions  pins coq 8.18.0 / idris2 0.7.0 / zig 0.14.0

Validated in-session: fresh Zig install from ziglang.org succeeds; Coq +
Idris2 idempotent-skip (no rebuild); src/formal + src/abi (idris2),
Modality.v (coq) and the zig coproc test all build with the bootstrapped
toolchain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
@hyperpolymath
hyperpolymath marked this pull request as ready for review June 26, 2026 22:09
@hyperpolymath
hyperpolymath merged commit 04d3c3e into main Jun 26, 2026
5 of 14 checks passed
@hyperpolymath
hyperpolymath deleted the claude/prover-bootstrap-iser branch June 26, 2026 22:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hyperpolymath @claude