From aff3a60332892c63913194d2b693512524183679 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 16:01:18 -0400 Subject: [PATCH] docs: correct the purge's reachable-leak claim; record the 3a lane MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rev 5 said acceptance 34's second edge was a killed buffer. Implementing it showed that is false: the Rust core fires exactly five hooks — buffer.after-edit, buffer.after-load, buffer.after-switch, frontend.detached, process.after-tick — and there is **no buffer-kill hook**, so lsp.lua never tears an attachment down and the drain keeps reaching that server. The premise (the drain builds its sid list from `attachments`) was right; the inference needed attachments to be removed on kill, and nothing removes them. The reachable leak has the same root cause by a different path. `attach_buffer` drops a sid from `attachments` the moment `server_is_live` reports false and rebuilds against a fresh server — so `crashed` / `stopped` is the event *least* likely to be drained, and an event-driven purge leaks in exactly the case it exists for. The purge therefore polls `pmacs.lsp.list()`, which enumerates the manager directly. Acceptance 34's second half now exercises a server in **no** attachment, which is the shape that discriminates: bitten, an event-driven purge fails it while the attached case still passes. §0.1 finding 6, Q#LN9, and acceptance 34 all updated; the wrong wording is left visible with its correction rather than quietly replaced, since the mistake is the useful part. Ledger gains the Stage 3a lane: branch, worktree, what ships, both corrected claims, the `install_async` load-order trap, the recorded bites, the one knowingly unpinned guard, and gate results. --- docs/active-work.md | 54 +++++++++++++++++++++++++++- docs/lean4-mode-framing.md | 74 ++++++++++++++++++++++++++------------ 2 files changed, 104 insertions(+), 24 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index b426f38..3cf1a8e 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -54,7 +54,7 @@ git status --short --branch The `git log` command must expose `0dd16a5` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #161) +## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; Stage 3a IN REVIEW - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review round, all twelve checks green). Branch `githubsucks/lean4-stage1` @@ -188,6 +188,58 @@ If it does not, stop and repair the remote/fetch configuration. suites**; `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` and `-- --skip basedpyright`. +### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`) + +- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @ + `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first + two commits, then the implementation, then a bite-driven correction. +- **Stage 2 merged as #161** (`main` @ `46a1b8f`, 2026-07-25, two review + rounds). COHERENCE.md §7 records the slice; §1.2 records the dead + `pmacs.error` channel found landing it. +- **Framing rev 5 splits Stage 3 into 3a and 3b** because rev 4 broke its + own §4 rule — the row read "two `lsp.lua` generalizations" under prose + claiming Stage 3 was Lean-only. One generalization shipped as Stage 2; + the other (Q#LN9's seams) is the shared event drain, so it is now its + own substrate stage. 3a and 3b are **strictly sequential** — 3b's + subscriber is written against 3a's seam and both touch `lsp.lua`. +- Ships: `pmacs.lsp.on_notification` / `on_response`, two arms in + `handle_server_requests`, a pending-response purge, and + `pmacs.fs.canonicalize` (Q#LN20). No protocol change, no Lean content. +- **Two framing claims were corrected during implementation**, both + recorded in §0.1 finding 6 and in the round-2 commit: + 1. The reachable leak is **not** a killed buffer. The Rust core fires + exactly five hooks (`buffer.after-edit`, `buffer.after-load`, + `buffer.after-switch`, `frontend.detached`, `process.after-tick`) — + **there is no buffer-kill hook**, so nothing tears an attachment + down and the drain keeps reaching that server. The real path is + `attach_buffer` dropping a dead sid from `attachments` and + rebuilding against a fresh server, which makes `crashed`/`stopped` + the event *least* likely to be drained. Hence the purge polls + `pmacs.lsp.list()` rather than riding the drain. + 2. Acceptance 32 does **not** pin "removed before invocation" — + `pcall` catches the raise either way, so before/after is + unobservable without a re-entrant drain. It pins removal being + **unconditional**; renamed accordingly. +- **`pmacs._fs` is installed from `install_async`, not `install_project`**, + purely for load order: `make_workspace` runs *after* `fs.lua` is + evaluated, so a canonicalizer placed there reads nil. This cost one + failing run to discover and is the kind of thing to check first. +- Bites recorded (all against the committed tree): removal gated on a + clean return → acc32 fails 2 != 1; an event-driven purge → the + no-attachment case fails "never called" while the attached case still + passes; a resolver without `canonicalize` → two servers (34b's own + falsification, which ships as a test). +- **Known unpinned:** the purge's generation (`attempt`) check. Reaching + it needs a crash *and* its restart to fall in a gap with no + `_async.tick`; the backoff is 500ms, so any tick sees `crashed` first + and the absent-or-terminal arm fires. Labelled as defensive in the + code rather than left looking covered. +- Verification on this branch: `cargo fmt --check` clean; strict + workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; + dispatch seams 14/14; multi-root 13/13; M4 121; required GPU 155; + **isolated-config workspace sweep 3,188 across 93 suites, zero + failures**; `git diff --check` clean. + ## Dired lane — framing APPROVED; Stage 0 MERGED, Stage 1 next - Approved framing: `docs/dired-framing.md` (revision 5), landing as its diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 317d74f..4869252 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -241,11 +241,26 @@ Confirmations, recorded because each was load-bearing and unverified: narrowing is load-bearing.** `handle_server_requests` builds its sid list from `attachments`, and `push_event` appends with no cap. So a subscriber fires only for a server with a live attachment, and an - unattached server's event queue grows unboundedly. This bites - acceptance 34 directly: kill the buffer with a request outstanding - and the pending purge never runs — the leak that criterion exists to - prevent. Q#LN9 now states the contract and acceptance 34 drives it - through the buffer-kill path rather than the server-death path alone. + unattached server's event queue grows unboundedly. + + *Corrected during implementation (rev 5, round 2).* Rev 5 first + claimed the reachable leak was a killed buffer. **That was wrong.** + The Rust core fires exactly five hooks — `buffer.after-edit`, + `buffer.after-load`, `buffer.after-switch`, `frontend.detached`, + `process.after-tick` — and **there is no buffer-kill hook at all**, + so `lsp.lua` never tears an attachment down and the drain keeps + reaching that server. The premise was right and the inference was + not: it needed attachments to be removed on kill, and nothing + removes them. + + The reachable leak is a different path with the same root cause. + `attach_buffer` drops a sid from `attachments` the moment + `server_is_live` reports false, rebuilding against a fresh server — + so the `crashed` / `stopped` event that should trigger a purge is + **precisely the one most likely to go undrained**. An event-driven + purge leaks exactly when it matters. Q#LN9 therefore drives the + purge off `pmacs.lsp.list()`, which enumerates the manager directly + and is unaffected by attachment bookkeeping. 7. **The `cfg.restart` gap is still open** (recorded landing #161): `ensure_server` never forwards `pmacs.lsp.config[lang].restart` to `pmacs.lsp.spawn`, so the field is silently dropped on auto-attach. @@ -264,9 +279,9 @@ rather than a bare root), `ensure_server` 527 → **610**, 12798 → **12827**, `pair.lua` 213 → **229**, and `compile.lua` 264 → **266**. Verified good and left alone: `listview.lua:138`, `src/lsp.rs:264`, `src/diag.rs:50`, `src/process.rs:193`, -`src/project.rs:145`, and the `mod.rs` binding-block citations. The pre-#161 line numbers inside Q#LN15 are -left as written: that stage has landed and its citations are historical -record, not navigation. +`src/project.rs:145`, and the `mod.rs` binding-block citations. The +pre-#161 line numbers inside Q#LN15 are left as written: that stage has +landed and its citations are historical record, not navigation. ## 1. What ships @@ -1018,13 +1033,24 @@ attachment.** `handle_server_requests` builds its sid list from `attachments`, so a server with no attached buffer is never drained — and `push_event` appends with no cap, so that server's queue grows unboundedly. Both facts are pre-existing and neither is Stage 3a's to -fix, but the second one turns the first into a leak with a name: **a -buffer killed while a request is outstanding never runs the purge**, -because the purge rides the drain that the attachment was gating. That is -the exact failure acceptance 34 exists to prevent, reachable through the -ordinary `C-x k`. So the purge is driven from both edges — the server-death -transition *and* attachment teardown — and acceptance 34 exercises the -buffer-kill path, which is the one a user can actually reach. +fix. What they change is where the purge may be wired. + +**The purge must not ride the drain.** `attach_buffer` removes a sid +from `attachments` as soon as `server_is_live` reports false and rebuilds +the attachment against a fresh server, so a `crashed` / `stopped` event +is the event *least* likely to be drained — the drain stops visiting +that server at almost exactly the moment the event is queued. A purge +triggered by observing that event therefore leaks in the case it exists +to handle. + +So the purge polls **`pmacs.lsp.list()`** after each drain instead. That +call enumerates the manager directly and is unaffected by attachment +bookkeeping, which is what makes it the right authority: a sid that is +absent, terminal, or running a new generation settles its pending +one-shots with an error, whether or not anything ever drained it. +Acceptance 34's second half exercises a server that is in **no** +attachment, because that is the shape an event-driven purge fails and a +polled one survives. The uncapped queue is recorded as a named deferral (§6) rather than fixed here: bounding it is a policy question about which events may be dropped, @@ -1629,14 +1655,16 @@ the blast radius. registered, `workspace/applyEdit` in the same drain is still handled; a raising response handler does not stop later events in that drain. Mirrors the notification-side pins above. -- **34.** **Pending-purge pin, both edges.** A server that dies with a response - outstanding invokes the pending one-shot with an error and clears it. - **And** — the case round 4 found reachable and rev 4 missed — killing - the *buffer* with a request outstanding does the same, rather than - stranding the registration behind a drain that no longer runs for - that server. The second half must be shown to fail against a - purge wired only to the server-death transition; otherwise this - criterion is satisfied by the implementation that leaks. +- **34.** **Pending-purge pin, both edges.** A server that dies with a + response outstanding invokes the pending one-shot with an error and + clears it. **And** a server that is in **no attachment** does the + same, rather than stranding the registration behind a drain that never + visits it. The second half must be shown to fail against a purge + wired to a death event seen in the drain; otherwise this criterion is + satisfied by the implementation that leaks. (Rev 5 first worded the + second edge as a killed buffer; there is no buffer-kill hook, so + nothing removes the attachment and that path does not leak. Corrected + in round 2 — see §0.1 finding 6.) - **34a.** **Canonicalizer pin (Q#LN20).** `pmacs.fs.canonicalize` resolves a symlinked and dot-segmented path to the same string as the real path, and returns nil for a nonexistent one. Fixture builds the symlink