From 2a1cf9be2eed1860ffb1a435084907128387d3ce Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Thu, 30 Jul 2026 18:58:17 -0400 Subject: [PATCH] =?UTF-8?q?docs(process):=20framing=20revision=204=20?= =?UTF-8?q?=E2=80=94=20record=20what=20implementing=20found?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Not a new design round. Every bet resolved, and one acceptance turned out to be satisfiable vacuously. Acceptance 2's in-drain clause said "the live descendant's named late output absent" without saying how the descendant stays live. It does not, by default: `poll_one` TERMs the whole group on leader exit. The first fixture's marker was therefore absent on both paths, and the pin would have stayed green with the collapse fixed. Bets 1 and 2 hold — every site took a directed outcome without restructuring, and every consequence is reachable, so the lane does not shrink. Bet 3 resolves the shutdown coupling as real and measured. Bet 4 is falsified exactly as its own clause anticipated: `ProcessEvent` is keyed by `ProcessId` while the ledger is keyed by pgid and is deliberately independent of managed records, every production consumer polls per known id, and `take_all_events` has no production consumer at all. Q#RL3 is answered accordingly and reporting is parked as its own lane. Also records the four sites and the two reusable lessons in `docs/agent-handoff.md` — that a seam for a background loop has to be directed, and that an absence assertion is only as good as its fixture's ability to produce the thing. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T --- docs/active-work.md | 28 +++++++-- docs/agent-handoff.md | 55 +++++++++++++++++ docs/reap-ledger-silent-failures-framing.md | 67 +++++++++++++++++++-- 3 files changed, 139 insertions(+), 11 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 0f8b195..fc17960 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -333,14 +333,32 @@ compatible. githubsucks/test-ambient-config-isolation ``` -## Reap-ledger silent failures — FRAMING OPEN, revision 3 +## Reap-ledger silent failures — IMPLEMENTED, PR OPEN - **Branch `reap-ledger-silent-failures`**, worktree `../pmacs-reap-ledger`, based on `githubsucks/main` @ `22df6ab`. - **Framing only; no code, no PR yet.** - `docs/reap-ledger-silent-failures-framing.md`, revision 3; two review - rounds closed (round 1: three blocking, two major; round 2: two - blocking, two major; all accepted). + `docs/reap-ledger-silent-failures-framing.md`, **revision 4**; + approved at revision 3 after two review rounds (round 1: three + blocking, two major; round 2: two blocking, two major; all accepted). + Revision 4 records implementation findings, not a new design round. +- **All four bets resolved.** Bet 1 (every site takes a directed + outcome) and Bet 2 (every consequence is reachable) hold. **Bet 3 + resolves the shutdown coupling as real and measured** — under 500ms + with a failed force-kill plus an errored probe, versus the full 2s + bound with only the force-kill failing. **Bet 4 is falsified: no + reporting channel exists**, so reporting becomes its own lane. +- **The in-drain pin's first fixture was vacuous, and the bite caught + it.** `poll_one` TERMs the group on leader exit, so an untrapped + descendant died before writing its late marker — absent on *both* + paths. With the seam reverted the pin failed only the consumed-plan + check, never the content assertion. Fixed with `trap '' TERM` behind + the readiness gate. +- **Gates: 10/10 green** on the pushed tree, all five bootstrap-storage + variables controlled — fmt, diff-check, clippy, `--lib` (1888), + `--lib --features crdt` (2073), compile-mode (67), copy-mode in both + feature configurations (18/19), M4 with the basedpyright skip (149), + required GPU (221). The five new process pins ran **15/15** as a + repetition set, since supervisor tests are load-sensitive. - **Unparked from PR #200's §5.** #200 retired the premise that justified the ledger's leniency and deliberately changed no disposition; this lane owns what it refused. diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index b4629f5..f2af131 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -257,6 +257,61 @@ commands, read `docs/active-work.md` immediately after this file. disagree — and it still establishes no identity, because it is read inside the same read-then-act window and no portable mechanism closes that for a *group* (`pidfd` covers a process; macOS has neither). +- **Reap-ledger silent failures — DIAGNOSTIC, in flight** + (`docs/reap-ledger-silent-failures-framing.md`). The lane #200's + framing §5 parked and its evidence unparked. **Four `kill(2)` results + are discarded in the group reap ledger**, and each discard has its own + consequence — three in the persistent ledger, one in the in-drain + twin: + - `tick_reap_ledger`'s probe cannot tell `ESRCH` (the group is gone — + correct) from any other errno (we could not ask — not correct), and + `retain` deletes the entry either way, cancelling escalation. + - The deadline escalation sets `killed = true` whether or not the + `SIGKILL` landed, so a failed one is **never retried by anything**. + - `shutdown()`'s force-kill does the same, on the path written + specifically to stop a leak at editor exit. + - `final_drain_runtime`'s twin collapses every errno into "dead", + which quiesces the drain and **cancels the readers** — truncated + output rather than a leaked process, and terminal for that drain + where a later tick could revisit the ledger. + - **None of the four has been observed to fire.** #200's evidence is an + explicit `SIGTERM` failing in `signal()`, not any ledger call. What + it retires is the *reason* ("EPERM cannot happen for our own + children"), not the behaviour. + - **`shutdown()`'s loop exit depends on the silent drop, and this is + now measured.** It runs while `any_running() || !reap_ledger.is_empty()`, + so an early exit needs the ledger empty **and** no live managed + record — the leader-exited-survivor case the ledger exists to serve. + With a failed force-kill followed by an errored probe it exits in + under 500ms instead of holding its 2s bound, having concluded + cleanup finished because the probe failed. Making the probe strict + without touching the loop converts that silent early exit into a + guaranteed 2s stall at every editor exit that hits it: **the two + cannot be changed independently.** + - **There is no channel for a background tick to report on.** + `ProcessEvent` is keyed by `ProcessId`, while the ledger is keyed by + pgid and is deliberately independent of managed records, so in the + case that matters there is no id to attribute to. Every production + consumer polls `take_events(id)` per known id; `take_all_events` + would sidestep the keying but **has no production consumer at all** + (two test call sites only). `pmacs.error` is dead. Reporting is + therefore its own lane, as the framing's Bet 4 anticipated. + - **A test seam for a background loop has to be directed.** + `shutdown()` signals every managed process before it reaches its + ledger force-kill, so one undirected "next kill fails" slot is eaten + by the wrong call and the test passes while proving nothing. The + persistent sites take a FIFO each (the coupling pin needs two + outcomes pending at once); the in-drain site needs one outcome that + **repeats for a whole drain**, because a one-shot is consumed by the + next 1ms probe and can never survive the 50ms window `quiesced` + requires. + - **An absence assertion needs a fixture that could have produced the + thing.** The in-drain pin's first fixture had no `trap '' TERM`, so + `poll_one`'s leader-exit group TERM killed the descendant before it + wrote its late marker: the marker was absent on *both* paths and the + pin would have stayed green with the collapse fixed. The bite caught + it — the reverted seam failed only the consumed-plan check, not the + content assertion. That is what the consumed-plan check is for. - **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b, 4a, 4b ALL LANDED** (`docs/lean4-mode-framing.md`; #160, #161, #167, #170, #179, #181). pmacs edits Lean 4: `arborium-lean` highlighting, a `lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language diff --git a/docs/reap-ledger-silent-failures-framing.md b/docs/reap-ledger-silent-failures-framing.md index 299c356..8d0dbdb 100644 --- a/docs/reap-ledger-silent-failures-framing.md +++ b/docs/reap-ledger-silent-failures-framing.md @@ -1,8 +1,9 @@ # Framing — group cleanup fails silently at four sites -**Revision 3.** Status: awaiting review round 3. Proposed lane: +**Revision 4.** Status: **APPROVED at revision 3; implemented.** Lane `reap-ledger-silent-failures`, worktree `../pmacs-reap-ledger`, based on -`githubsucks/main` @ `22df6ab` (a reading; re-measure at branch time). +`githubsucks/main` @ `22df6ab`. Revision 4 records what implementation +found; it is not a new design round. **Parked by PR #200's framing §5 and unparked by its evidence.** #200 retired the premise that justified the ledger's leniency; it deliberately @@ -10,6 +11,53 @@ changed no disposition, and said so. This lane owns what it refused. ## Revision history +**Revision 3 → 4**, found **while implementing**, not a new design +round. Every bet resolved; one acceptance turned out to be satisfiable +vacuously. + +- **Acceptance 2's in-drain clause could be met by a vacuous fixture, + and was.** "The live descendant's named late output absent" says + nothing about how the descendant stays live — and `poll_one` sends + `SIGTERM` to the whole group on leader exit, so an untrapped + descendant dies before it can write. The marker was then absent on + *both* paths and the pin would have stayed green with the collapse + fixed. The bite is what caught it: with the seam reverted, the pin + failed only the consumed-plan check, never the content assertion. The + fixture now uses `trap '' TERM` behind `survivor_script`'s readiness + gate. **The lesson generalises past this pin: an absence assertion is + only as good as the fixture's ability to produce the thing.** +- **Bet 1 holds.** All four sites took a directed outcome with no + restructuring. `final_drain_runtime` — the one §3 named as at risk, + being a free function — needed only a shared handle on the context it + already receives. +- **Bet 2 holds, in the direction that keeps the lane.** All four + consequences are reachable; none was already foreclosed by an earlier + guard. The lane does not shrink. +- **Bet 3 resolves: the coupling is real and measured.** With a failed + force-kill and an errored probe, `shutdown()` returns in **under + 500ms** instead of holding its 2s bound, with the survivor alive. With + only the failed force-kill it burns the full bound. §1.3's warning + stands: making the probe strict without touching the loop converts a + silent early exit into a guaranteed 2s stall. +- **Bet 4 is falsified, exactly as its own clause anticipated: no + channel exists.** `ProcessEvent` is keyed by `ProcessId` while the + ledger is keyed by pgid and is deliberately independent of managed + records, so in the leader-exited-survivor case there is no id to + attribute to. Every production consumer polls `take_events(id)` per + known id (`lua_bindings/mod.rs:8933`, `:10731`, `mcp.rs:361`). + `take_all_events` would sidestep the keying but **has no production + consumer at all** — its only two call sites are tests, despite a doc + comment naming a `*processes*` buffer. `pmacs.error` was already + known dead. **Reporting becomes its own lane** (§5), and this PR ships + instrumentation plus tests without it, which is what §7 said it would + do in this case. +- **The in-drain `SIGKILL` is still unpinned**, as §1.2a promised. Its + `group_killed` flag stays local and the persistent ledger retries in + the same outer tick, so pinning the local non-retry still needs a + call-count assertion or a direct free-function test. Unchanged, and + restated here so a later reader does not mistake the shipped seam for + covering it. + **Revision 2 → 3**, after review round 2 (two blocking, two major). All four accepted; all four verified in the code first. @@ -271,10 +319,17 @@ noted so a red run on it is not mistaken for this lane's doing.* *Unknown. `killed = true` on a failed `SIGKILL` is clearly wrong as bookkeeping; what should replace it is a policy question, not an obvious fix.* -- **Q#RL3** — How does a background tick report anything? *The ledger - emits no events and has no status channel. `pmacs.error` is defined - only by a test stub and is dead at 15 call sites, so it is not the - answer. This is the lane's real design question.* +- **Q#RL3** — How does a background tick report anything? **ANSWERED at + revision 4: it cannot, today.** `ProcessEvent` is keyed by + `ProcessId`; the ledger is keyed by pgid and is deliberately + independent of managed records, so in the leader-exited-survivor case + — the one the mechanism exists for — there is no id to attribute to. + All three production consumers poll `take_events(id)` per known id + (`lua_bindings/mod.rs:8933`, `:10731`, `mcp.rs:361`). + `take_all_events` would sidestep the keying but has **no production + consumer**; its only call sites are two tests, notwithstanding a doc + comment naming a `*processes*` buffer. `pmacs.error` was already dead + at 15 sites. Reporting is therefore parked as its own lane (§5). - **Q#RL4** — Does the `shutdown()` loop need its own termination condition if (a) becomes strict? *Almost certainly (§1.3), and that coupling is why the two cannot be changed independently.*