A proof is a run with a state, and a proof that cannot start or is cut off says why on the pull #7708

A proof now writes a run of kind proof with a state, and one that can't start or is cut off says why on the pull. The new tests and the nearby suites (85 tests, including mcp-size) pass, and tsc and design-lint are clean. I didn't run the whole suite; scripts/fast.ts named 1341 files, so I ran the files that cover this change.

What changed

• Where proof runs live: run has a CHECK on kind that SQLite can't widen without a table rebuild, and the additive-migration rule forbids rebuilds. Proof runs therefore sit in a new proof_run table (migration 20261101120000-proof-run, pinned). core/proof_runs.ts reads them as Runs of kind proof, so listRuns merges them into the runs list, the MCP runs tool shows them, and /runs/<id> opens one. No new MCP tool.
• States: queued is waiting for a slot, running, ok is green, failed is red or head doesn't merge, and cancelled is cut off. The badge reads "Green" or "Cut off".
• Can't start: startProof records a queued run ("no check slot is spare") or a failed one ("head does not merge onto the base tip") and comments on the pull once per head and reason. When a slot frees, the same queued run starts.
• Cut off: a proof cut at the deadline or by a gate interruption ends cancelled, with a comment on the pull. After a restart, a proof run still running that this process doesn't hold is cut off on the next sweep and told (the forge stopped). The pull is then proved again, as before.
• Pull API next: an approved, green pull with a non-green proof now reads, for example, "approved and green, but its proof waits: no check slot is spare", instead of plain "approved and green". The same wording covers running, red and cut-off proofs.
• Tests: four new tests in merge-queue-proof.test.ts and one case in next_actor.test.ts. They cover:

- waiting for a slot, saying so once, and starting when one frees; - a head that doesn't merge, said once; - a cut-off run and comment, then proved again; - a restart-orphaned run.

Left out

• The pull page itself shows the wait only through next and the comment; the page has no separate proof row.
• listRuns with no kind now includes proofs for every caller that omits one.
• A waiting row is created only when another proof is already running. That is the existing rule for taking a slot, and I kept it.

To try

• Push a pull with an approved, green check on a busy forge.
• Open the runs list or call MCP runs: the proof appears there.
• Open the pull and read its comments and next.

Closes #7706

A proof now writes a run of kind proof with a state, and one that can't start or is cut off says why on the pull. The new tests and the nearby suites (85 tests, including mcp-size) pass, and tsc and design-lint are clean. I didn't run the whole suite; scripts/fast.ts named 1341 files, so I ran the files that cover this change.

What changed

• Where proof runs live: run has a CHECK on kind that SQLite can't widen without a table rebuild, and the additive-migration rule forbids rebuilds. Proof runs therefore sit in a new proof_run table (migration 20261101120000-proof-run, pinned). core/proof_runs.ts reads them as Runs of kind proof, so listRuns merges them into the runs list, the MCP runs tool shows them, and /runs/<id> opens one. No new MCP tool.
• States: queued is waiting for a slot, running, ok is green, failed is red or head doesn't merge, and cancelled is cut off. The badge reads "Green" or "Cut off".
• Can't start: startProof records a queued run ("no check slot is spare") or a failed one ("head does not merge onto the base tip") and comments on the pull once per head and reason. When a slot frees, the same queued run starts.
• Cut off: a proof cut at the deadline or by a gate interruption ends cancelled, with a comment on the pull. After a restart, a proof run still running that this process doesn't hold is cut off on the next sweep and told (the forge stopped). The pull is then proved again, as before.
• Pull API next: an approved, green pull with a non-green proof now reads, for example, "approved and green, but its proof waits: no check slot is spare", instead of plain "approved and green". The same wording covers running, red and cut-off proofs.
• Tests: four new tests in merge-queue-proof.test.ts and one case in next_actor.test.ts. They cover:

- waiting for a slot, saying so once, and starting when one frees; - a head that doesn't merge, said once; - a cut-off run and comment, then proved again; - a restart-orphaned run.

Left out

• The pull page itself shows the wait only through next and the comment; the page has no separate proof row.
• listRuns with no kind now includes proofs for every caller that omits one.
• A waiting row is created only when another proof is already running. That is the existing rule for taking a slot, and I kept it.

To try

• Push a pull with an approved, green check on a busy forge.
• Open the runs list or call MCP runs: the proof appears there.
• Open the pull and read its comments and next.

This round addresses all seven review points. A proof is a run of kind proof: queued while no check slot is spare, then running, then ok, failed or cancelled. It says on the pull why it waited or couldn't start. Type check is clean, and the proof, next-actor, MCP runs/tools, runs-list and terminal-runs tests pass. scripts/fast.ts said the diff is too broad to name tests, so I ran the covering files by hand. I did not run the whole suite; the forge's check does that.

1. kind=proof accepted at the doors.

- RUN_KINDS now includes proof. - MCP runs takes a kind argument and refuses an unknown one; the API accepts ?kind=proof. - The web runs list has ?kind=proof and a "Proofs" link. - test/proof-runs.test.ts lists and filters proofs through MCP runs, the API and the terminal runs screen.

1. Superseded proofs end. Opening a proof run for a new head cancels any queued or running proof of an older head with "superseded by a push". A test covers it, in startProof and directly.
2. Cut-off comment once per head and reason. A second cut-off on the same head ends its run but does not post again. A test covers two cut-offs giving one comment.
3. README and terminal. The README has a short section on what a proof run is, its states, and where its summary says why it waited. The terminal runs list shows proof rows as "Proof of <head>" with their summary, and a test checks that.
4. Proof merge is opt-in. listRuns mixes proofs into a kind-less list only with withProofs: true. The web runs list, the terminal runs screen, the API without kind, and MCP runs without kind pass it. Counts and "latest run" callers read the run table alone as before. A proof has no environment, so env returns no proofs. A pagination test pages the merged list with cursor and limit and checks no run is lost or repeated.
5. Tests tightened.

- The toBeDefined() check is gone; tests now assert the exact why through the exported proofWords. - A badge test covers Green, Cut off and Queued. - /runs/<id> opens a proof run and the API returns it.

1. Reason and summary kept apart. The regex hack is replaced by a cutOff(x, runId, head, reason) helper that builds the summary from the reason.

Beyond what was asked, I gave proofs a "Proof of <head>" title on the web run page, and regenerated docs/MCP.md for the new kind argument.

Left out: ?kind=check is still not accepted by the API.

A proof is now a run of kind proof, kept in its own proof_run table, which is new in src/core/proof_runs.ts and its migration. Before this change, proofs lived only in an in-memory map in src/checks/proof.ts, so the runs list never showed one. A proof's run moves through these states:

• queued: no check slot is spare.
• running
• ok: shown as Green.
• failed: shown as red.
• cancelled: shown as Cut off. This means the deadline passed or the forge restarted, and the pull is proved again on the next sweep.

A push cancels the old head's unfinished proof with the summary "superseded by a push".

When a proof cannot start, its summary says why: no check slot is spare, or the head does not merge onto the base tip. A cut-off proof gets the same treatment. Each reason reaches the pull once per head, as a comment, and in the pull API's next, which names the wait instead of "queue, approved and green" (src/flow/next_actor.ts).

Where proofs show:

• the runs list with ?kind=proof
• the terminal's Runs screens
• GET …/runs?kind=proof
• MCP runs with kind: "proof"

Proofs join the other kinds only in those lists, not by default.

Tests in test/proof-runs.test.ts and test/merge-queue-proof.test.ts cover:

• a proof that waits while every check slot is taken and starts when one frees;
• an interrupted proof that leaves a cut-off run and one comment, and is proved again on the next sweep;
• a push cancelling the old head's proof;
• a head that does not merge, reported once.

bun x tsc --noEmit passes, and so do the 33 tests across those two files and test/next_actor.test.ts. The branch merges onto the current main without conflicts.

Not done: the run table itself is unchanged. Proofs are read as a Run from their own table, so the scheduler's run sweeps never pick them up.

To try it, open a pull while every check slot is busy, then look at /…/runs?kind=proof and at the pull's comments and next.

No code changed since the last push. The latest message on the issue only filed it under P0 Trust, which it already serves through #7673.

🤖 Generated with Claude Code

A proof is now a run with a state (queued, running, ok, failed, cancelled), shown as kind proof in the runs list, the pull, the TUI and MCP runs. A proof that cannot start, or is cut off, says why on the pull once per head. This round fixes the four points from @sentinel's review.

1. Proofs end when the pull leaves open. A new endProofRunsForPull in src/core/proof_runs.ts marks the pull's queued or running proofs cancelled. It runs in two places:

- closeAsMerged in src/core/pulls.ts, with the summary "pull landed". - The core setIssueState in src/core/issues.ts, with "pull closed". Every close path goes through it, not only the checks service's event handler, which some setups don't run. The summary words match what the checks service already writes on check runs.

1. A gate that fails to answer is told to the pull. That path in startProof now goes through cutOff(), so the pull hears it once per head.
2. Tell-once covers every run of the head. refuse now asks whether any run of this head already waited or failed for the same reason, using a new endedBefore. cutOffBefore now uses the same check. A head that fails to merge, then waits for a slot, then fails to merge again tells the pull twice, once per reason.
3. The told guard is testable. It moved out of proofWait into an exported toldWhileOpen in src/crew/autonomy.ts; its behaviour is unchanged.

Tests. Five new tests in test/merge-queue-proof.test.ts cover:

• a gate that fails to answer, run twice: cut off both times, told once;
• the merge-fail, slot-wait, merge-fail sequence: told twice, once per reason;
• landing a pull ends its waiting proof;
• closing a pull ends its waiting proof;
• toldWhileOpen comments on the current head, and stays silent after a push or a close.

The first four fail without this change. The toldWhileOpen test locks in a guard that already worked, so it passes either way. bun x tsc --noEmit is clean and 196 tests pass across the merge-queue, checks, autonomy, issues and pulls suites. scripts/fast.ts named 1407 test files because core/issues.ts reaches almost everything, so I chose those suites myself instead of the full set.

🤖 Generated with Claude Code

A proof is now a run with a state. A pull that can't start its proof, or whose proof is cut off, gets a message saying why. Proof runs can be reached through every door: the REST runs list, MCP and CLI. This push merges main back in; the only conflict was the runs list endpoint in src/http/api.ts.

The conflict: this branch changed that endpoint to accept kind=proof and to include proof runs in an unfiltered list (withProofs: true). Meanwhile main rewrote it to add each row's agent and its pull or issue (nameRuns). The merged version does both: it keeps main's code and adds the proof kind filter and the default proof inclusion. No other file conflicted.

The type check is clean, and 57 tests across 10 files pass. Those files cover the runs list, the named rows, proof runs, the merge queue's proof, what a stranger sees, timing, MCP, CLI, the gate doors and the OpenAPI document. I didn't run the full suite; the forge's check runs it on this push.

To try it: GET /api/v1/repos/trevato/forge/runs should list proof runs alongside deploy and agent runs, each named with its pull. ?kind=proof should list only proofs. Both work on the preview at https://lab--7708--forge-trevato-apps.open-platform.sh.

🤖 Generated with Claude Code

A proof is now a run with a state. A pull that can't start its proof, or whose proof is cut off, gets a message saying why. Proof runs can be reached through every door: the runs list, the terminal's Runs screen, the API and the MCP runs tool.

This push merges main again. Only README.md conflicted, at the same spot in "What works today": this branch added a paragraph on proof runs, and main added one on how a pasted model key is cleaned up. Both are kept. Together they put the README over the 60 KB limit that test/readme-front-door.test.ts checks. So the proof paragraph moved, unchanged, into docs/CREW.md, right after the merge-queue paragraph about proofs. The README is now 61,129 bytes.

The type check is clean, and 45 of the 46 tests in the proof, runs-list and MCP runs files plus the README test passed. The one failure was that size limit, which is now fixed: after the move, the README and docs tests (19, including the size test) all pass. I didn't run the full suite after the move; the forge's check runs it on this push.

To try it: GET /api/v1/repos/trevato/forge/runs?kind=proof on https://lab--7708--forge-trevato-apps.open-platform.sh lists only proof runs. Without kind, they are listed alongside deploy and agent runs.

🤖 Generated with Claude Code