From 8c924ebf41a1236779832f261af0d011a4bf513f Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 16:17:24 -0400 Subject: [PATCH 01/14] docs: record #166 as landed and open the CI-coverage lane The handoff snapshot and the active-work ledger both still described the GPU terminal input work as in review. Per their own update protocols this should have ridden #166; it did not, because the review that surfaced the CI-coverage finding came after that PR was already green, and expanding an approved PR to carry a new lane would have been the wrong trade. docs/agent-handoff.md section 1 gains the #166 entry: the split into a frontend-kind-neutral liveness half and a grid-only geometry half, the extracted dispatcher loop body, the trap about the no-placement release that reads like liveness and is not, and why the one-line guard was rejected. docs/active-work.md moves the lane to "Closed since the last snapshot" and opens a new one: the Stage 3 real-path acceptance is dark in CI. The workflow never enables the crdt feature, so every crdt-gated acceptance test is not merely skipped but never compiled -- which covers a37 (real daemon, real PTY, real wgpu) since #135 as well as the two tests #166 added beside it. The fix is one step on the gpu-render job, but it needs its own lane because it would run a37 under lavapipe for the first time, and neither its timing budgets nor its wgpu path have been exercised on that adapter. The lane also asks which other crdt-gated suites are dark for the same reason. Recorded alongside it: #166's three unit pins are not crdt-gated and do run under CI's exact flags, including the controller-release pin whose only job is catching the plausible wrong fix, so the regression protection is live even though the real-daemon evidence is local-only. No code changes. --- docs/active-work.md | 93 ++++++++++++++++++++----------------------- docs/agent-handoff.md | 43 +++++++++++++++++++- 2 files changed, 85 insertions(+), 51 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 1cff0f2..5624d24 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -227,57 +227,32 @@ If it does not, stop and repair the remote/fetch configuration. buffer a directory should resolve *to*, and `pmacs .` should route into it rather than growing a second directory surface. -## GPU terminal input lane — IN REVIEW +## Stage 3 acceptance is dark in CI — NEEDS A LANE -- Portable branch: `githubsucks/gpu-terminal-input`, worktree - `../pmacs-gui-term-input`, based on `githubsucks/main` @ `46a1b8f`. -- Approved framing: `docs/gpu-terminal-input-framing.md` revision 2, - committed as the branch's first commit (`9a0df21`). Bug fix, not a - feature; **no protocol change (stays v20)**. -- Reported as "text input within the terminal doesn't work on GUI, this is - fine in TUI". Root cause: the dispatcher applied **both** terminal-layout - syncs to **every** attached frontend, and a semantic session satisfies both - conditions (a `term_sizes` entry from `AttachRequest` *and* a terminal - declaration). Its PTY was resized twice per tick forever — grid arm installs - the TUI placement size, semantic arm installs the declared content - rectangle, each arm's idempotence guard seeing only what the other just - wrote — so the child took a `SIGWINCH` storm at tick cadence. -- **The fix is a split, not a guard.** The grid arm is also the only per-tick - controller-liveness release a semantic frontend gets, and - `sync_semantic_terminal_layout` cannot take that over: the buffer-follow - snapshot clears the viewport declaration (`on_buffer_snapshot_sent`), so - that arm stops running in exactly the switch-away case that needs the - release. `sync_terminal_layout` is therefore split into a - frontend-kind-neutral half (panel reconcile + liveness) and a grid-only - geometry half, with the loop body extracted to - `sync_terminal_layouts_for_tick` so the exclusivity is structural and tests - drive the real thing. -- **Trap for anyone touching this again:** the release at the "no - `window_placements` entry" arm reads like liveness and is grid geometry. A - semantic frontend has no placement entry at all, so moving it into the - neutral half releases a GPU controller every tick. -- Bite-verified against **two** pre-images, because the naive guard fixes the - storm and introduces the leak: - - | pin | `main` | naive guard | the split | - |---|---|---|---| - | settle (acc 2+3) | FAIL | pass | pass | - | controller release (acc 6) | pass | FAIL | pass | - | grid still resizes (acc 5) | pass | pass | pass | - -- Real-path evidence: a quiet child trapping `SIGWINCH` reports **144 frames - in 4 s and `WINCH 1..12` on screen** against the pre-fix tree, versus a - settled screen with the fix. -- **Deliberately out of scope, named:** interactive-shell echo on a raw-mode - PTY (Q#GT5 — reproduces in-process too, so it is not the GUI/TUI - asymmetry), and a geometry change appearing to clear the visible screen - (reproduces pre-fix; why acceptance 4 latches its observation across - frames). -- Verification on this branch: `cargo fmt --check` clean; strict workspace - Clippy clean; 1,829 default + 2,006 CRDT library tests; vterm Stage 1/2/3 - 10 / 6 / 9 CRDT; bottom-panel Stage 1 46; M4 121; required GPU 155; - **isolated-config workspace sweep 3,177 across 92 suites, zero failures**; - `git diff --check` clean. Gates were run against the committed tree. +- **No branch, no framing yet.** Found while gating #166; deliberately kept + out of it so a CI change would not arrive after review approval. +- `.github/workflows/ci.yml` **never enables the `crdt` feature** (grep the + workflow directory: zero hits). Every `#[cfg(feature = "crdt")]` acceptance + test is therefore not merely skipped in CI — it is **not compiled**. +- That covers the whole Vterm Stage 3 real-path acceptance, including `a37` + (real daemon + real PTY + real wgpu), which has been dark since #135, and + the two tests #166 added beside it. +- The `gpu-render` job is the only one with lavapipe and + `PMACS_REQUIRE_GPU=1`, and it runs `cargo test -p pmacs-gpu`, which never + reaches the `pmacs` crate's acceptance suites. +- The shape of the fix is one step on the `gpu-render` job: + `cargo test --features crdt --test vterm_stage3_acceptance -- --test-threads=1`. + It needs its own lane rather than a drive-by because it would run `a37` + under lavapipe **for the first time**, and neither its timing budgets nor + its wgpu path have ever been exercised on that adapter or on macOS CI. +- Worth auditing at the same time: which *other* `crdt`-gated acceptance + suites are dark for the same reason. This is a coverage question about the + gate list itself, not about any one suite. +- Mitigating fact, verified rather than assumed: #166's three unit pins are + **not** `crdt`-gated and do run under CI's exact flags + (`--no-default-features --features luajit|lua54`), including the + controller-release pin whose only job is catching the plausible wrong fix. + The regression protection is live; the real-daemon evidence is local-only. ## Bottom-panel lane (window placement + side windows) — Stage 1 IN REVIEW @@ -483,6 +458,24 @@ git worktree add --track \ ## Closed since the last snapshot +- **GPU terminal input (the double terminal-layout sync) — MERGED as #166** + (`main` @ `b889873`, 2026-07-25, one review round, all twelve checks green + after a macOS PTY-timing rerun). The dispatcher applied **both** + terminal-layout syncs to **every** attached frontend; a semantic session + satisfies both conditions, so its PTY was resized twice per tick forever and + the child took a `SIGWINCH` storm that made a GPU terminal untypable while + output still flowed. `sync_terminal_layout` is now split into a + frontend-kind-neutral half (panel reconcile + controller liveness) and a + grid-only geometry half, with the loop body extracted to + `sync_terminal_layouts_for_tick` so the exclusivity is structural. No + protocol change (v20). Durable lessons are in `docs/agent-handoff.md` §5; + the framing (`docs/gpu-terminal-input-framing.md` rev 2) carries three + falsified hypotheses, the two-pre-image bite matrix, and two named + out-of-scope items (Q#GT5 interactive-shell echo on a raw PTY, which + reproduces in-process and so is not the GUI/TUI asymmetry; and a geometry + change appearing to clear the visible screen, which reproduces pre-fix). + Branch `gpu-terminal-input` and worktree `../pmacs-gui-term-input` retained. + - **GPU initial target — MERGED as #148** (`main` @ `0dd16a5`, 2026-07-24, after two review rounds). `pmacs --gpu [--socket …] FILE` opens a target before the GPU window appears. Protocol bumped 19 → 20: a semantic-session diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index d1f4943..e28911f 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,6 +1,9 @@ # Agent handoff — cross-machine continuity -**Last updated: 2026-07-25, after find-file (#162) landed — the dired +**Last updated: 2026-07-25, after the GPU terminal input fix (#166) landed — +the double terminal-layout sync that made a GPU terminal untypable — following +Lean 4 Stage 2 (#161), the dired framing pair (#163/#164), find-file (#162) — +the dired arc's Stage 0 — following COHERENCE.md (#163), Lean 4 Stage 1 (#160), the minimap blank-slab fix (#159), bottom-panel Stage 1 (#155), the inline-math re-scout (#154), the vterm PTY-flake fix (#153), and the @@ -578,6 +581,44 @@ commands, read `docs/active-work.md` immediately after this file. - Remaining ranked arcs: 6 folding Stage 3, 7 DAP, 8 GPU splits, plus the `.ipynb` arc (its JSON-grammar prerequisite shipped in #123). +- **GPU terminal input LANDED — #166** (`main` @ `b889873`; + `docs/gpu-terminal-input-framing.md` rev 2; one review round). The + dispatcher applied **both** terminal-layout syncs to **every** attached + frontend each tick. A semantic session satisfies both conditions — a + `term_sizes` entry from `AttachRequest` *and* a terminal declaration — so + its PTY was resized twice per tick forever: the grid arm installed the TUI + placement size, the semantic arm the declared content rectangle, each arm's + `old_size == size` guard seeing only what the other had just written. The + child took a `SIGWINCH` storm at tick cadence, which made typing into a GPU + terminal impossible while output kept flowing. TUI was structurally + unaffected. + - `EditorInstance::sync_terminal_layout` is split into + `sync_terminal_controller_liveness` (frontend-kind **neutral**: panel + reconcile + release of a controller whose window moved away — reads only + views/windows/controller, never a grid size) and + `sync_terminal_grid_geometry` (**grid only**: TUI placement + resize). + `sync_terminal_layout` survives as the composition, so `editor::run` and + `LOCAL` are byte-identical. + - `daemon::sync_terminal_layouts_for_tick` is the extracted loop body: + liveness for every frontend once per tick, then **exactly one** geometry + arm keyed on `semantic_states` membership — the same fact session + establishment uses, so the arms cannot both fire. + - **The trap, kept in a comment:** the release on a missing + `window_placements` entry reads like liveness and is grid geometry. A + semantic frontend has no placement entry at all, so moving it into the + neutral half would release a GPU controller every tick. + - Why not the one-line guard: the grid arm was also the **only** per-tick + controller-liveness release a semantic frontend got, and + `sync_semantic_terminal_layout` cannot take it over — the buffer-follow + snapshot clears the viewport declaration, so that arm stops running in + exactly the switch-away case that needs the release. + - No protocol change (v20). Gates: 1,829 default + 2,006 CRDT library + tests; vterm Stage 1/2/3 10/6/9 CRDT; bottom-panel 46; M4 121; required + GPU 155; isolated-config workspace sweep 3,177 across 92 suites. + - **Known gap, its own lane:** CI never enables `crdt`, so the Stage 3 + real-path acceptance (including `a37`) is not compiled there. #166's unit + pins are not `crdt`-gated and do run. See `docs/active-work.md`. + ## 2. How we work (the part that must not drift) The user is expert and reviews deeply — they falsify framings and find From 40709fafb93a199ae8a65e264eaad1a45aeebbf0 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 17:17:23 -0400 Subject: [PATCH 02/14] docs: measure the CI coverage gap and record the vterm as-framed audit The lane opened in the previous commit was scoped to the Vterm Stage 3 acceptance. Measuring it properly shows the problem is much larger and not vterm-specific. Comparing cargo test --list under CI's exact flags against the same flags plus crdt: 3,024 versus 3,288. 264 tests are dark in CI, and the single worst line is the library itself at 177 -- cargo test --lib --features crdt is a required local gate that CI has never run. Ten suites run zero or one test, including gpu_initial_target (#148's entire acceptance, 1 of 14), gpu_invocation (#141's, 1 of 14), and a37, the Stage 3 real-daemon/real-PTY/real-wgpu path that #135 built precisely because a decoded-message fixture would prove none of the three fit together. The lane now carries the per-target table, the verified flag combination for the fix, a two-part fix shape (a crdt leg on the test job, plus the GPU-requiring suites onto the existing gpu-render job that already has lavapipe), and an explicit instruction to sort deliberate exclusions from accidental ones first -- some of the 264 are perf suites that are ignored by default and belong to their own jobs, while m10_10_perf has no ignore attribute and no job naming it. docs/vterm-framing.md gains an as-framed audit section. The arc is structurally complete and every test named in the Stage 2 verification map exists, but criterion 22's "without thrash" clause was never pinned anywhere -- the word appears nowhere in src or tests -- and that clause describes exactly the defect #166 fixed. Of the nine Stage 3 tests, only three drive a real daemon, so the six that construct EditorState directly could never see a dispatcher-loop defect; a31 passes on the broken tree for that reason. Four of the nine, including a37 and Stage 3 review round 1's own presence regression guard, do not run in CI at all. The section also records what was not audited: section 11's blanket claim about deferral safety covers roughly twenty items and none were spot-checked. docs/gpu-terminal-input-framing.md scores bet B2 true now that the reporter has confirmed typing works, and retracts Q#GT5. The bash fixture behind it does not reproduce in real use and was almost certainly measuring its own timing rather than a product behaviour; it is marked retracted rather than deleted so nobody re-derives it from an earlier revision. docs/agent-handoff.md section 5 gains the lesson the confirmation cost: a daemon-side fix is not deployed until the daemon is restarted from a tree containing it, and rebuilding a binary does nothing to a running process. No code changes. --- docs/active-work.md | 82 +++++++++++++++++++++--------- docs/agent-handoff.md | 9 ++++ docs/gpu-terminal-input-framing.md | 26 +++++++--- docs/vterm-framing.md | 42 +++++++++++++++ 4 files changed, 129 insertions(+), 30 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 5624d24..5f2f142 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -227,32 +227,68 @@ If it does not, stop and repair the remote/fetch configuration. buffer a directory should resolve *to*, and `pmacs .` should route into it rather than growing a second directory surface. -## Stage 3 acceptance is dark in CI — NEEDS A LANE +## The CRDT half of the test corpus is dark in CI — NEEDS A LANE -- **No branch, no framing yet.** Found while gating #166; deliberately kept - out of it so a CI change would not arrive after review approval. -- `.github/workflows/ci.yml` **never enables the `crdt` feature** (grep the - workflow directory: zero hits). Every `#[cfg(feature = "crdt")]` acceptance - test is therefore not merely skipped in CI — it is **not compiled**. -- That covers the whole Vterm Stage 3 real-path acceptance, including `a37` - (real daemon + real PTY + real wgpu), which has been dark since #135, and - the two tests #166 added beside it. -- The `gpu-render` job is the only one with lavapipe and - `PMACS_REQUIRE_GPU=1`, and it runs `cargo test -p pmacs-gpu`, which never - reaches the `pmacs` crate's acceptance suites. -- The shape of the fix is one step on the `gpu-render` job: - `cargo test --features crdt --test vterm_stage3_acceptance -- --test-threads=1`. - It needs its own lane rather than a drive-by because it would run `a37` - under lavapipe **for the first time**, and neither its timing budgets nor - its wgpu path have ever been exercised on that adapter or on macOS CI. -- Worth auditing at the same time: which *other* `crdt`-gated acceptance - suites are dark for the same reason. This is a coverage question about the - gate list itself, not about any one suite. +- **No branch, no framing yet.** Found while gating #166, then measured + properly during the vterm as-framed audit. Deliberately kept out of #166 so + a CI change would not arrive after review approval. +- **Root cause:** `.github/workflows/ci.yml` never enables the `crdt` feature + anywhere — zero hits across the workflow directory. The `test` job runs + `cargo test --all-targets --no-default-features --features luajit|lua54`. + Every `#[cfg(feature = "crdt")]` test is therefore **not compiled** in CI, + not merely skipped. +- **Measured, `--list` under CI's exact flags versus the same flags plus + `crdt`: 3,024 vs 3,288 — 264 tests dark.** Per target: + + | dark | CI | full | target | + |---:|---:|---:|---| + | 177 | 1,832 | 2,009 | **the library itself** (`src/lib.rs`) | + | 21 | 15 | 36 | `m5_5_acceptance` | + | 13 | 1 | 14 | `gpu_invocation_acceptance` | + | 13 | 1 | 14 | `gpu_initial_target_acceptance` | + | 8 | 0 | 8 | `m10_11_acceptance` | + | 6 | 0 | 6 | `auto_pair_crdt_acceptance` | + | 6 | 0 | 6 | `m10_2_perf` | + | 4 | 5 | 9 | `vterm_stage3_acceptance` | + | 4 | 0 | 4 | `m10_10_perf` | + | 3 | 0 | 3 | `compile_mode_crdt_acceptance` | + | 2 | 22 | 24 | `theme_faces_acceptance` | + | 2 | 0 | 2 | `m11_5_semantic_acceptance` | + | 1 | 9 | 10 | `vterm_stage1_acceptance` | + | 1 | 7 | 8 | `statusline_segments_acceptance` | + | 1 | 10 | 11 | `gpu_font_acceptance` | + | 1 | 0 | 1 | `auto_indent_crdt_acceptance` | + | 1 | 0 | 1 | `m10_11_perf` | + +- **The single worst line is the library.** `cargo test --lib --features crdt` + is a REQUIRED local gate in `CLAUDE.md`, and CI has never run it. 177 + library tests — the whole CRDT half — are developer-machine-only. +- **Ten suites run zero or one test in CI**, including `gpu_initial_target` + (#148's entire acceptance, 1/14), `gpu_invocation` (#141's, 1/14), and + `a37`, the Vterm Stage 3 real-daemon/real-PTY/real-wgpu path that #135 + built specifically because "a decoded-message fixture would prove none of + the three fit together". +- **Sort deliberate from accidental before proposing a fix.** Some of the 264 + are perf suites that are `#[ignore]`d by default and belong to their own + jobs (`m10_2_perf` 6, `m10_11_perf` 1). `m10_10_perf` has **no** `#[ignore]` + and no CI job naming it, so it looks accidental. This classification is not + finished and is the lane's first task. +- **Fix shape, two parts** (the flag combination is verified to work: + `--no-default-features --features luajit,crdt` lists 10 vterm Stage 1 tests + versus 9 without): + 1. a `crdt` leg on the `test` job for the non-GPU suites and the library; + 2. the GPU-requiring `crdt` suites onto the existing `gpu-render` job, which + already has lavapipe and `PMACS_REQUIRE_GPU=1` — + `vterm_stage3_acceptance`, `gpu_invocation_acceptance`, + `gpu_initial_target_acceptance`, `gpu_font_acceptance`. +- **Expect first-run failures, and budget for them.** These would execute in + CI for the first time ever: real PTY timing on CI runners, wgpu under + lavapipe, and daemon-socket tests at unfamiliar concurrency. Start + ubuntu-only and decide about macOS from evidence. A red first run is the + lane working, not the lane failing. - Mitigating fact, verified rather than assumed: #166's three unit pins are - **not** `crdt`-gated and do run under CI's exact flags - (`--no-default-features --features luajit|lua54`), including the + **not** `crdt`-gated and do run under CI's exact flags, including the controller-release pin whose only job is catching the plausible wrong fix. - The regression protection is live; the real-daemon evidence is local-only. ## Bottom-panel lane (window placement + side windows) — Stage 1 IN REVIEW diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index e28911f..165f06a 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -745,6 +745,15 @@ final variant — its own round-trip cannot detect a discriminant shift. ## 5. Hard-won ops lessons +- **A daemon-side fix is not deployed until the daemon is restarted from a + tree that contains it.** #166's reporter rebuilt and saw no change: the + running daemon had been started from a shared checkout still on a pre-fix + branch, and `pmacs --gpu` attaches to whatever process already owns the + socket. Rebuilding a binary does nothing to a running process. When + validating a daemon-side fix by hand, check the running process's binary + path and start time against the tree you think you fixed — + `ps -eo pid,lstart,args | grep '[p]macs --daemon'` — before concluding the + fix failed. - **Two operations that must be alternatives are not made alternatives by being adjacent.** The dispatcher applied its grid and semantic terminal-layout syncs to every attached frontend; a semantic session diff --git a/docs/gpu-terminal-input-framing.md b/docs/gpu-terminal-input-framing.md index 0bbccef..aa1bea4 100644 --- a/docs/gpu-terminal-input-framing.md +++ b/docs/gpu-terminal-input-framing.md @@ -81,7 +81,11 @@ character: | | frames for a static screen | typed `Z` ever visible at the prompt | |---|---|---| | `main` today | **730** in a 20 s window | **no** | -| with the guard | **2** | (see Q#GT5 — a separate question) | +| with the fix | **2** | yes | + +Bet B2 is **scored TRUE**: with the fix deployed, the reporter confirmed +typing into a GPU terminal works. The earlier caveat here pointed at Q#GT5, +which is now retracted — see "Deferred (named)". The TUI is unaffected: a grid session has no semantic terminal declaration, so only one arm ever runs for it. This is a **frontend-kind** defect, which is @@ -281,11 +285,12 @@ change. Stays v20. snapshot that signals the switch-away). Hence the split in Q#GT1. Recorded rather than deleted: the failure mode is one a reviewer or a future simplification will re-propose. -- **B2.** The user's reported symptom is this defect. *Partially scored: the - storm is proven and GUI-only, and its shape (line editor unusable, output - still flowing) matches the report. Not fully scored until the user, or an - acceptance running the **user's own shell**, confirms typing works after the - fix. Q#GT5 is the reason this bet is stated rather than assumed.* +- **B2 — SCORED TRUE 2026-07-25.** "The user's reported symptom is this + defect." Confirmed in real use after the fix was deployed: typing into a GPU + terminal works. The confirmation needed a daemon **restart** built from a + tree containing the fix — the first attempt reported no change because a + pre-fix daemon still owned the socket, which is worth remembering whenever a + daemon-side fix is being validated by hand. - **B3.** No other pair of per-frontend-kind daemon operations is applied as siblings rather than alternatives. *Scored by an explicit audit of the dispatcher's per-frontend loop during implementation — this defect's shape @@ -294,7 +299,14 @@ change. Stays v20. ## Deferred (named) -- Interactive-shell echo on a raw-mode PTY (Q#GT5) — its own scout. +- ~~Interactive-shell echo on a raw-mode PTY (Q#GT5)~~ — **RETRACTED + 2026-07-25.** The observation behind it (a `bash --norc -i` fixture not + echoing typed characters) does not reproduce in real use: with the fix + deployed, typing into a GPU terminal echoes normally. The fixture was almost + certainly measuring its own timing — polling a published screen snapshot + before readline had finished initialising — not a product behaviour. Recorded + as retracted rather than deleted so nobody re-derives it from the framing's + earlier revision and spends a scout on it. - **A geometry change appears to clear the visible screen.** Observed while building acceptance 4: after the probe's deliberate 25×92 → 20×71 resize, the next frame's visible grid is entirely blank even though the content diff --git a/docs/vterm-framing.md b/docs/vterm-framing.md index b1124c0..b86bcd0 100644 --- a/docs/vterm-framing.md +++ b/docs/vterm-framing.md @@ -1674,6 +1674,48 @@ GPU assertions remain in `pmacs-protocol` and `pmacs-gpu` respectively. - **37:** one real-daemon/real-PTY/headless-wgpu acceptance path; it is not replaced by a decoded-message fixture. +### 0.12 As-framed audit, 2026-07-25 (after #166) + +Prompted by a GPU terminal input defect that shipped in Stage 3 and was fixed +in #166. The arc is structurally complete — all 37 criteria have +implementations, and every test named in the Stage 2 verification map exists — +but the audit found two gaps worth recording against the criteria themselves. + +**Criterion 22's "without thrash" was never pinned.** The criterion reads +"unchanged, zero, passive, and failed resize cases preserve prior geometry +*without thrash*". The word appears nowhere in `src/` or `tests/`. The suite +pinned the four enumerated single-arm cases and never the cross-arm +interaction — which is exactly where the thrash lived: the daemon applied +both the grid and the semantic terminal-layout sync to every attached +frontend, so a semantic session's PTY was resized twice per tick forever. +Criterion 31's "only the exact durable controller changes PTY geometry" was +violated in the same event, in spirit rather than letter: the controller was +the right frontend, but the geometry came from the grid projection. #166 adds +the settle pins; the gap was open from #135 (2026-07-22) until then. + +**Why the Stage 3 suite could not see it.** Of its nine tests, only three +drive a real daemon; the other six construct `EditorState` directly and never +execute the dispatcher loop where the defect lived. `a31`, which is about two +semantic frontends sharing one session, therefore passes on the broken tree. +The same structural blindness explains why `bottom_panel_stage1_acceptance` +was unaffected. A criterion about *dispatcher* behavior needs a test that +runs the dispatcher. + +**Four of the nine Stage 3 tests do not run in CI at all**, because they are +`#[cfg(feature = "crdt")]` and the workflow never enables that feature: +`a37`, the two added by #166, and +`terminal_mode_keeps_reporting_presence_so_peers_drop_the_stale_caret` — which +is Stage 3 review round 1's own regression guard. Stage 1's +`read_only_empty_crdt_bootstrap_is_immutable_against_remote_content`, the CRDT +half of criterion 14, is dark for the same reason. Stage 2 is fully covered +(6/6). This is not a vterm problem: 264 tests workspace-wide are dark, +including 177 in the library. It has its own lane in `docs/active-work.md`. + +**Not audited:** §11's blanket claim that "deferral means graceful ignore or +documented absence, never escape leakage, panic, unbounded allocation, or +child leak". That covers roughly twenty deferred items and none were +spot-checked. It remains an unproven claim rather than a known gap. + ## 10. Gates and bite verification Every PR runs the standing full gates from `AGENTS.md`, sequentially, plus its From b76da70d5d6f7650f56e7c65b99bf64f3e5aff7b Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 21:53:41 -0400 Subject: [PATCH 03/14] =?UTF-8?q?feat(panel):=20route=20the=20Projection?= =?UTF-8?q?=20half=20of=20the=20=C2=A71.3=20census=20(Stage=202A)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bottom-panel Stage 2A, first half. Every consumer the framing classifies **Projection** now resolves the frontend's primary document window or buffer instead of its focused one; every consumer classified focus, focus-chrome, or focus/session is deliberately left alone. No protocol change, no behavior change for any frontend today: with `panel_capable = false` for semantic sessions, `primary_document_window` returns `view.active` for every existing configuration, so this is a seam adoption that becomes load-bearing in 2B. Projection consumers routed: - **#1** semantic buffer-follow / `BufferSnapshot` re-send - **#2** the lazy CRDT upgrade — the sharpest case, since it BROADCASTS to every replica, so keying it on focus would let focusing a fresh generated panel buffer swap every peer's document mirror - **#3** `CursorByte` - **#4** `LineNumbers` mode - **#5** selection decorations - **#6/#10/#11** the full-window semantic terminal declaration, its snapshot/sync, and terminal-frame suppression, via the shared `semantic_terminal_key` resolver - **#9** the `Viewport` terminal-context gate — a focused terminal panel must not suppress the still-visible document's viewport - **#12** the semantic statusline target LOOKUP - **#21** the `BufferSnapshot` publication recipient filter `align_semantic_window_to_buffer` splits per Q#BP14, which is the distinction that makes rejecting panel-named events insufficient on its own: - `align_primary_document_window` (**#7**, `Viewport`) — aligns the document window and **never touches `view.active`**. - `align_and_activate_primary_document_window` (**#8**, `Pointer`) — aligns and then activates, because a click in the document area means "work here". This is the one place projection and focus legitimately move together. `dispatch_semantic_terminal_pointer` (**#11**) gains the same rule: an accepted non-`Move` gesture activates the document window before the gesture replays, while bare hover neither focuses nor claims. The statusline change is deliberately a HALF change (parent acceptance 42): the window LOOKUP resolves the primary document window, but `active` still reports **actual focus**, so a document provider can truthfully observe `active = false` while a panel owns focus. Untouched, and that is the load-bearing negative: #13 remote-op validation, #14 `dispatch_idle_for`, #15 presence, #16-#19 search / menu / minibuffer / completion chrome, #20 terminal bell drain, and #23 remote-op application all still resolve the actually focused window. #16-#19's Q#BP14b routing table needs `PanelFrame` and lands in 2B. 1,832 library tests pass; fmt and workspace clippy clean. Co-Authored-By: Claude Opus 5 (1M context) --- src/daemon.rs | 102 +++++++++++++++++++++++++++++++---------- src/editor.rs | 21 ++++++++- src/semantic_render.rs | 13 +++++- src/statusline.rs | 15 +++++- 4 files changed, 121 insertions(+), 30 deletions(-) diff --git a/src/daemon.rs b/src/daemon.rs index 9ac8256..19e5cc6 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -1145,9 +1145,13 @@ fn dispatcher_loop( .session_state(*fid) .is_some_and(|s| s.negotiated_capabilities.semantic_render) { + // Bottom-panel §1.3 #1 — Projection. The buffer this + // frontend DISPLAYS AS ITS DOCUMENT, not the one it + // happens to focus: focusing a panel must re-send no + // snapshot and must never swap the replica's mirror. let active_now = { let core = editor.core.borrow(); - core.active_window_for(*fid).map(|w| w.buffer_id) + core.primary_document_buffer(*fid) }; if let Some(active_now) = active_now && last_active_buffer_sent.get(fid) != Some(&active_now) @@ -1430,8 +1434,16 @@ fn dispatcher_loop( .session_state(*fid) .is_some_and(|s| s.negotiated_capabilities.crdt_replica) { + // Bottom-panel §1.3 #3 — Projection. `CursorByte` is + // the replica's authoritative DOCUMENT cursor; a + // focused panel must not retarget it at the panel + // buffer (Q#BP14's "active buffer is a + // document-surface term, not an input-focus term"). let core = editor.core.borrow(); - if let Some(window) = core.active_window_for(*fid) { + if let Some(window) = core + .primary_document_window(*fid) + .and_then(|win_id| core.windows.get(&win_id)) + { let cursor_byte_msg = InstanceMessage::CursorByte { buffer_id: window.buffer_id, byte_pos: window.cursor, @@ -2038,12 +2050,17 @@ fn handle_dispatcher_event( // straight back off it. The declared buffer is // checked too — a terminal has no byte viewport to // honor from any direction. + // Bottom-panel §1.3 #9 — Projection. The gate asks + // "is this frontend's DOCUMENT surface a terminal", + // so it tests the primary document window. A focused + // TERMINAL PANEL must not suppress the still-visible + // document's viewport. let terminal_context = { let manager = editor.terminal_manager.borrow(); let core = editor.core.borrow(); let active = core - .active_window_for(source) - .is_some_and(|window| manager.is_terminal(window.buffer_id)); + .primary_document_buffer(source) + .is_some_and(|document| manager.is_terminal(document)); active || manager.is_terminal(buffer_id) }; if semantic_states.contains_key(&source) && !terminal_context { @@ -2056,7 +2073,11 @@ fn handle_dispatcher_event( // LOCAL's attach-time buffer (often a scratch the // user isn't viewing), so arrow keys moved an // off-screen cursor and the caret never tracked. - align_semantic_window_to_buffer(editor, source, buffer_id); + // Bottom-panel §1.3 #7 — Projection, and it must + // NOT move focus. Routing this through the + // focused window would let an ordinary document + // viewport overwrite a focused panel's buffer. + align_primary_document_window(editor, source, buffer_id); if let Some(sem) = semantic_states.get_mut(&source) { sem.set_viewport(buffer_id, visible, generation); } @@ -2121,7 +2142,11 @@ fn handle_dispatcher_event( // aligns to the buffer the frontend says it was // displaying: a click can race a buffer switch. if semantic_states.contains_key(&source) { - align_semantic_window_to_buffer(editor, source, buffer_id); + // Bottom-panel §1.3 #8 — Projection + focus. A + // click in the DOCUMENT area means "work here", + // so unlike `Viewport` (#7) this one also takes + // focus out of a panel. + align_and_activate_primary_document_window(editor, source, buffer_id); if kind == PointerKind::Context { // Q#CM1 — right-click opens the context menu // at the hit byte (needs the Lua builder, so @@ -2359,9 +2384,15 @@ fn ensure_active_buffer_crdt_backed( editor: &EditorState, fid: FrontendId, ) -> Option { + // Bottom-panel §1.3 #2 — Projection, and the sharpest case in the + // census. The upgrade BROADCASTS a `BufferSnapshot` to every + // replica, so keying it on focus would mean focusing a fresh + // generated panel buffer swaps every peer's document mirror to it. + // A panel buffer that genuinely needs CRDT backing gets it when it + // is displayed as a document, not as a side effect of focus. let buffer_id_opt = { let core = editor.core.borrow(); - core.active_window_for(fid).map(|w| w.buffer_id) + core.primary_document_buffer(fid) }; let buffer_id = buffer_id_opt?; let core = editor.core.borrow(); @@ -2493,11 +2524,13 @@ fn publish_buffer_snapshot_to_replicas( continue; } if session.negotiated_capabilities.semantic_render { - let displays_buffer = editor - .core - .borrow() - .active_window_for(*peer_id) - .is_some_and(|window| window.buffer_id == buffer_id); + // Bottom-panel §1.3 #21 — Projection. "Displays this + // buffer" means the peer's DOCUMENT surface: testing the + // focused window would both miss a buffer visible in the + // document (panel focused elsewhere) and replace the peer's + // mirror for one visible only in a panel. + let displays_buffer = + editor.core.borrow().primary_document_buffer(*peer_id) == Some(buffer_id); if !displays_buffer { continue; } @@ -2936,32 +2969,35 @@ fn handle_remote_crdt_op( /// whole switch. This is the input/display alignment fix for B1: the /// frontend's *declared* buffer becomes the buffer its keys edit and /// its `CursorByte` reports. -fn align_semantic_window_to_buffer( +/// Align a semantic frontend's **primary document window** to the +/// buffer it declared (bottom-panel §1.3 #7, Q#BP14). +/// +/// **Never touches `view.active`.** This is why rejecting panel-named +/// events does not fix the *document* event: with a panel focused, an +/// ordinary document `Viewport` routed through the focused window would +/// overwrite the panel's buffer with the document buffer. Returns the +/// window it aligned so the `Pointer` path (#8) can activate it. +fn align_primary_document_window( editor: &mut EditorState, fid: FrontendId, buffer_id: crate::buffer::BufferId, -) { +) -> Option { use crate::text_view::TextView; - let text_view = { + let (win_id, text_view) = { let core = editor.core.borrow(); - let Some(win_id) = core.views.get(&fid).map(|v| v.active) else { - return; - }; + let win_id = core.primary_document_window(fid)?; if core.windows.get(&win_id).map(|w| w.buffer_id) == Some(buffer_id) { - return; // Already displaying this buffer. + return Some(win_id); // Already displaying this buffer. } let reg = core.registry.borrow(); let Ok(buf) = reg.get(buffer_id) else { - return; // Unknown buffer — leave the window as-is. + return Some(win_id); // Unknown buffer — leave the window as-is. }; - TextView::new(buf) + (win_id, TextView::new(buf)) }; let mut core = editor.core.borrow_mut(); - let Some(win_id) = core.views.get(&fid).map(|v| v.active) else { - return; - }; if let Some(win) = core.windows.get_mut(&win_id) { win.buffer_id = buffer_id; win.text_view = text_view; @@ -2969,6 +3005,24 @@ fn align_semantic_window_to_buffer( win.selection = None; win.overlays.clear(); } + Some(win_id) +} + +/// Align the primary document window **and take focus to it** +/// (bottom-panel §1.3 #8, Q#BP14). +/// +/// A click in the document area means "work here", so it moves focus +/// out of a panel. This is the one place projection and focus +/// legitimately move together — every other Projection consumer must +/// use [`align_primary_document_window`] alone. +fn align_and_activate_primary_document_window( + editor: &mut EditorState, + fid: FrontendId, + buffer_id: crate::buffer::BufferId, +) { + if let Some(win_id) = align_primary_document_window(editor, fid, buffer_id) { + editor.core.borrow_mut().focus_window(fid, win_id); + } } fn build_fresh_frontend_view( diff --git a/src/editor.rs b/src/editor.rs index 1db5c3a..8bc9d8f 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -1341,9 +1341,16 @@ impl EditorState { frontend_id: FrontendId, buffer_id: crate::buffer::BufferId, ) -> Option { + // Bottom-panel §1.3 #6/#10/#11 — Projection. The full-window + // semantic terminal declaration, its snapshot/sync, and its + // frame suppression all describe the frontend's PRIMARY DOCUMENT + // surface, never a panel band: panel terminals get `PanelFrame` + // / `PanelPointer` in Stage 2B instead. Resolving through + // `view.active` would let a focused panel terminal both claim + // the document declaration and suppress the document pass. let core = self.core.borrow(); - let view = core.views.get(&frontend_id)?; - let window = core.windows.get(&view.active)?; + let win_id = core.primary_document_window(frontend_id)?; + let window = core.windows.get(&win_id)?; if window.buffer_id != buffer_id { return None; } @@ -1472,6 +1479,16 @@ impl EditorState { if coord.row >= size.rows || coord.col >= size.cols { return false; } + // Bottom-panel §1.3 #11 — Projection + focus. A non-hover + // gesture on the DOCUMENT terminal means "work here", so it + // takes focus back out of a panel before the gesture replays; + // bare hover neither focuses nor claims the controller. + if !matches!(kind, TerminalMouseKind::Move) { + let mut core = self.core.borrow_mut(); + if let Some(win_id) = core.primary_document_window(frontend_id) { + core.focus_window(frontend_id, win_id); + } + } self.core.borrow_mut().active_frontend = frontend_id; self.apply_terminal_gesture(key, size, coord, kind, mods, (coord.row, coord.col)); true diff --git a/src/semantic_render.rs b/src/semantic_render.rs index 65750d3..617d408 100644 --- a/src/semantic_render.rs +++ b/src/semantic_render.rs @@ -1345,9 +1345,13 @@ impl SemanticRenderState { state: &EditorState, buffer_id: BufferId, ) -> Option { + // Bottom-panel §1.3 #4 — Projection. `LineNumbers` describes the + // replica's DOCUMENT surface; a focused panel must not replace + // the document's gutter mode with the panel window's. let mode = { let core = state.core.borrow(); - core.active_window_for(self.frontend_id) + core.primary_document_window(self.frontend_id) + .and_then(|win_id| core.windows.get(&win_id)) .map_or(crate::window::LineNumberMode::Off, |w| w.line_numbers) }; if self.last_line_numbers == Some(mode) { @@ -1703,7 +1707,12 @@ impl SemanticRenderState { // Emitting CurrentLine here forced a whole-buffer line table on // every frame even though pmacs-gpu ignores its own current-line // wash. - if let Some(win) = core.active_window_for(self.frontend_id) + // Bottom-panel §1.3 #5 — Projection. Selection decorations + // belong to the document surface the viewport describes; a + // selection made inside a focused panel must not paint into it. + if let Some(win) = core + .primary_document_window(self.frontend_id) + .and_then(|win_id| core.windows.get(&win_id)) && win.buffer_id == vp.buffer_id && let Some((lo, hi)) = win.region() && let Some(range) = clip_to_viewport(lo, hi, vp) diff --git a/src/statusline.rs b/src/statusline.rs index d11c885..1e6d9cc 100644 --- a/src/statusline.rs +++ b/src/statusline.rs @@ -639,9 +639,20 @@ fn capture_target_contexts( .views .get(&frontend_id) .ok_or(StatuslineNoMessageReason::ContextUnavailable)?; + // Bottom-panel §1.3 #12 — Projection. This LOOKUP resolves + // the primary document window: with a panel focused, + // `view.active` would name the panel and the declared-buffer + // check would clear the document's statusline. + // + // `active` is NOT rerouted with it (Q#BP14/parent 42): it + // reports ACTUAL focus, so a document provider truthfully + // observes `active = false` while the panel owns focus. + let window_id = core + .primary_document_window(frontend_id) + .ok_or(StatuslineNoMessageReason::ContextUnavailable)?; let window = core .windows - .get(&view.active) + .get(&window_id) .ok_or(StatuslineNoMessageReason::ContextUnavailable)?; if buffers.get(window.buffer_id).is_err() { return Err(StatuslineNoMessageReason::BufferUnavailable); @@ -653,7 +664,7 @@ fn capture_target_contexts( frontend_id, window_id: window.id, buffer_id: window.buffer_id, - active: true, + active: window.id == view.active, }]) } } From d7ad01b53596dc13a3e13faddd791b7d4432b398 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 22:04:56 -0400 Subject: [PATCH 04/14] feat(panel): extract the per-window painter + Stage 2A acceptance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bottom-panel Stage 2A, second half (Q#BP8, Q#BP17). Still no protocol change and no behavior change: `paint_frame` builds the same fold map it always did and passes it in, so grid rendering is unchanged. Two extractions, both taking the fold map as a **parameter** rather than building it: - `prepare_window_cursor_visible` — the active-window auto-scroll clamp. The panel band (2B) runs this for its own window when that window owns focus, and leaves a passive panel's `view_top` alone. - `paint_window_content` — the per-window document body: text, gutter, overlays, selection, and the mode line. The panel paints into a panel-sized grid at the same origin-agnostic `Viewport`, so this is that body lifted out, not a second painter (Bet B2'). The parameter is the point (Q#BP17). Folding built its per-window map ungated on the premise that "a semantic session never enters `paint_frame`", which the panel band breaks. The panel path must pass `None` for a frontend whose `fold_projection` is false, and must not call `EditorCore::fold_map_for_window` — that gates on the **active** frontend, which is right for command-time reckoning and wrong for painting another frontend's panel. `tests/bottom_panel_stage2a_acceptance.rs` — 10 tests. The negative half is the load-bearing half, so Projection assertions are paired with focus-class assertions taken in the SAME state: - `focus_and_projection_disagree_in_the_same_state` is the key one: with a panel focused, the focus authority must name the panel while the projection authority names the document. Routing the focus class through `primary_document_window` fails this even though every Projection test still passes. - The statusline pair pins the split: the LOOKUP resolves the document window while `active` reports actual focus, with a non-vacuity twin that flips `active` back to true when focus returns. - The extraction pair pins cells, the returned cursor, the focused window's `view_top`, AND a passive window's untouched scroll — identical cells alone would not catch a clamp that moved to the wrong window on a single-window frame. - `the_panel_fixture_really_builds_a_side_window` pins the fixture's own precondition, since every other test is worthless if `focused_panel` silently produced an ordinary split. One crdt-gated caller of the old `align_semantic_window_to_buffer` was updated; it compiles only under `--features crdt`, which is the config CI never runs. 1,832 default + 2,009 CRDT library tests, 10 new acceptance; fmt and workspace clippy clean. Co-Authored-By: Claude Opus 5 (1M context) --- src/daemon.rs | 6 +- src/editor.rs | 307 ++++++++++-------- tests/bottom_panel_stage2a_acceptance.rs | 377 +++++++++++++++++++++++ 3 files changed, 556 insertions(+), 134 deletions(-) create mode 100644 tests/bottom_panel_stage2a_acceptance.rs diff --git a/src/daemon.rs b/src/daemon.rs index 19e5cc6..16e66ab 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -4439,7 +4439,7 @@ mod tests { /// B1 input/display alignment: a semantic frontend's window is bound /// to LOCAL's attach-time buffer, but the buffer it *displays* is - /// the one it declares via `Viewport`. `align_semantic_window_to_buffer` + /// the one it declares via `Viewport`. `align_primary_document_window` /// re-points the window so keys edit the displayed buffer — without /// it, arrow keys moved an off-screen cursor in the wrong buffer and /// the caret never tracked. @@ -4477,7 +4477,9 @@ mod tests { ); // The frontend declares it is displaying the file buffer. - align_semantic_window_to_buffer(&mut editor, fid, file); + // Bottom-panel §1.3 #7: `Viewport` takes the projection-only + // aligner, which never touches `view.active`. + align_primary_document_window(&mut editor, fid, file); assert_eq!( editor .core diff --git a/src/editor.rs b/src/editor.rs index 8bc9d8f..2553775 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -3169,6 +3169,170 @@ impl CompletionPopupKey { } } +/// Scroll one window so its cursor stays visible, reckoning in +/// **visible** lines when a fold map is supplied (Arc 6 Q#FD18). +/// +/// Extracted from `paint_frame` for bottom-panel Stage 2 (Q#BP8): the +/// panel band runs this for its own window when that window owns focus, +/// against the same supplied map, and leaves a passive panel's +/// `view_top` untouched. +/// +/// **The fold map is a parameter, never built here (Q#BP17).** A panel +/// painted for a frontend whose `fold_projection` is false must pass +/// `None`; `EditorCore::fold_map_for_window` is the wrong source there +/// because it gates on the **active** frontend, which is right for +/// command-time reckoning and wrong for painting another frontend's +/// panel. +fn prepare_window_cursor_visible( + window: &mut crate::window::Window, + buf: &crate::buffer::Buffer, + inner_rows: u32, + folds: Option<&crate::fold_view::VisibleLineMap>, +) { + let cursor_row = window + .text_view + .pos_to_display(buf, window.cursor) + .map_or(0, |d| d.row as usize); + match folds { + // The logical cursor may sit on a hidden line (a shared fold, or + // goto-line into one); the row that actually renders — and so + // the row to scroll to — is its visible head (Q#FD16/FD18, + // framing acceptance 8). + Some(map) => { + let anchor = map.visible_head_of(cursor_row); + let top = map.clamp_view_top(window.view_top); + window.view_top = if anchor < top { + anchor + } else if inner_rows > 0 && map.visible_rows_between(top, anchor) >= inner_rows as usize + { + map.nth_visible_back(anchor, inner_rows as usize - 1) + } else { + top + }; + } + None => { + if cursor_row < window.view_top { + window.view_top = cursor_row; + } else if inner_rows > 0 && cursor_row >= window.view_top + inner_rows as usize { + window.view_top = cursor_row + 1 - inner_rows as usize; + } + } + } +} + +/// Paint one window's document content: text, gutter, overlays, +/// selection, and its mode line. +/// +/// Extracted from `paint_frame`'s per-window loop for bottom-panel +/// Stage 2 (Q#BP8) — the panel band paints its window into a +/// panel-sized grid at the same origin-agnostic `Viewport`, so this is +/// that body lifted out rather than a second painter. No concrete +/// text/gutter/overlay/mode-line painter forks (Bet B2'). +/// +/// **`folds` is a parameter, never built here (Q#BP17).** Folding's +/// "a semantic session never enters `paint_frame`" premise is what the +/// panel band breaks; the panel path passes `None` when the owning +/// frontend's `fold_projection` is false, and must not call +/// `EditorCore::fold_map_for_window`, which gates on the **active** +/// frontend. +#[allow(clippy::too_many_arguments)] +fn paint_window_content( + grid: &mut crate::cell::CellGrid<'_>, + window: &mut crate::window::Window, + buf: &crate::buffer::Buffer, + placement: WindowPlacement, + folds: Option<&crate::fold_view::VisibleLineMap>, + focused: bool, + theme: &crate::highlight::Theme, + statusline: Option<&crate::statusline::StatuslineWindowSegments>, + diag_store: &std::sync::Arc>, +) { + let rect = placement.outer; + let inner_rows = placement.content.size.rows; + if let Some(map) = folds { + window.view_top = map.clamp_view_top(window.view_top); + } + let viewport_buffer_start = window.text_view.line_offset(window.view_top).unwrap_or(0); + // UX gutter (Q#UX2): reserve a left strip for line numbers and + // shrink+shift the text area into the remainder, so every + // viewport-relative painter (text, syntax, diagnostics, search) + // stays gutter-agnostic. A window too narrow for the gutter falls + // back to no gutter this frame rather than starving the text. + let gutter_w = { + let w = window.gutter_width(); + if w >= rect.size.cols { 0 } else { w } + }; + let viewport = Viewport { + buffer_start: viewport_buffer_start, + buffer_end: buf.len(), + cell_origin: CellCoord::new(rect.origin.row, rect.origin.col + gutter_w), + cell_size: crate::cell::CellSize::new(inner_rows, rect.size.cols - gutter_w), + gutter_w, + folds, + }; + // Composition (T M2.9): base text_view paints first, then the + // gutter numbers — before the overlays, so a diagnostic overlay + // can draw its severity sign into the gutter's leading column + // without the gutter's own blank pass erasing it — then each + // overlay in attach order. See [`crate::view::View`]. + window.text_view.render(buf, viewport, grid); + if gutter_w > 0 { + paint_line_number_gutter(grid, window, &rect, inner_rows, gutter_w, folds, theme); + } + for overlay in &mut window.overlays { + overlay.render(buf, viewport, grid); + } + paint_local_selection(grid, buf, window, &rect, inner_rows, gutter_w, folds, theme); + // Mode line for this window. Painted last so the line + // itself is always visible regardless of overlay activity. + let coord = window + .text_view + .pos_to_display(buf, window.cursor) + .unwrap_or_default(); + // Arc 6 Stage 2 (Q#FD18): All/Top/Bot/% are reckoned in + // VISIBLE-line space — a buffer whose remainder is collapsed + // reads "All", not "Top". The cursor's ordinal anchors on its + // visible head, since that is the row it renders on. + let (ind_top, ind_total, ind_cursor) = match folds { + Some(map) => ( + map.visible_rows_between(0, window.view_top), + map.visible_line_count(window.text_view.line_count()), + map.visible_rows_between(0, map.visible_head_of(coord.row as usize)), + ), + None => ( + window.view_top, + window.text_view.line_count(), + coord.row as usize, + ), + }; + let scroll = format_scroll_indicator(ind_top, inner_rows as usize, ind_total, ind_cursor); + // Lock scoped to the summary computation only: the overlay + // renders above include `DiagnosticView`, which takes this + // same mutex — holding the guard across the loop deadlocked + // the daemon on the first frame after a file (and thus a + // diagnostic overlay) was opened. + let diags = { + let guard = diag_store.lock().expect("diag store mutex poisoned"); + diag_mode_line_summary(&guard, buf) + }; + let custom = statusline; + paint_mode_line( + grid, + &rect, + buf.name(), + buf.is_modified(), + focused, + coord.row, + coord.col, + &scroll, + &diags, + mode_line_style(theme), + custom.map_or(&[], |segments| segments.left.as_slice()), + custom.map_or(&[], |segments| segments.right.as_slice()), + theme, + ); +} + /// Paint one full frame into `grid` and return the desired terminal /// cursor position. /// @@ -3278,6 +3442,11 @@ pub fn paint_frame( // Arc 6 Stage 2 (Q#FD18): the auto-scroll clamp reckons in // VISIBLE lines. Built from the active window itself, before // the mutable borrow below. + // + // Bottom-panel Q#BP17: built HERE and passed in, because the + // panel path (Stage 2B) must supply `None` for a frontend + // whose `fold_projection` is false. Building it inside the + // clamp would hard-wire the grid's answer. let folds = core .windows .get(&active) @@ -3285,36 +3454,7 @@ pub fn paint_frame( let aw = core.windows.get_mut(&active).expect( "invariant: active_window_id always references a live window in core.windows", ); - let cursor_row = aw - .text_view - .pos_to_display(buf, aw.cursor) - .map_or(0, |d| d.row as usize); - match folds.as_ref() { - // The logical cursor may sit on a hidden line (a shared - // fold, or goto-line into one); the row that actually - // renders — and so the row to scroll to — is its visible - // head (Q#FD16/FD18, framing acceptance 8). - Some(map) => { - let anchor = map.visible_head_of(cursor_row); - let top = map.clamp_view_top(aw.view_top); - aw.view_top = if anchor < top { - anchor - } else if inner_rows > 0 - && map.visible_rows_between(top, anchor) >= inner_rows as usize - { - map.nth_visible_back(anchor, inner_rows as usize - 1) - } else { - top - }; - } - None => { - if cursor_row < aw.view_top { - aw.view_top = cursor_row; - } else if inner_rows > 0 && cursor_row >= aw.view_top + inner_rows as usize { - aw.view_top = cursor_row + 1 - inner_rows as usize; - } - } - } + prepare_window_cursor_visible(aw, buf, inner_rows, folds.as_ref()); } } @@ -3366,114 +3506,17 @@ pub fn paint_frame( let Ok(buf) = reg.get(window.buffer_id) else { continue; }; - // Arc 6 Stage 2 (Q#FD12, round-2 F2): ONE visible-line map per - // rendered document window, keyed on that window's own buffer and - // line offsets. A split may show different buffers with only one - // folded, so a per-frame singleton would leak one pane's folds - // into the other. `None` when this buffer has no folds — the - // unfolded path then paints exactly as before. let folds = crate::fold_view::map_for_window(&state.fold_registry, window); - // `view_top` stays a source-line index (Bet B5) but must never - // rest on a hidden line: clamp BACKWARD so a fold at the top of - // the viewport shows its head (Q#FD18, acceptance 8). - if let Some(map) = folds.as_ref() { - window.view_top = map.clamp_view_top(window.view_top); - } - let viewport_buffer_start = window.text_view.line_offset(window.view_top).unwrap_or(0); - // UX gutter (Q#UX2): reserve a left strip for line numbers and - // shrink+shift the text area into the remainder, so every - // viewport-relative painter (text, syntax, diagnostics, search) - // stays gutter-agnostic. A window too narrow for the gutter falls - // back to no gutter this frame rather than starving the text. - let gutter_w = { - let w = window.gutter_width(); - if w >= rect.size.cols { 0 } else { w } - }; - let viewport = Viewport { - buffer_start: viewport_buffer_start, - buffer_end: buf.len(), - cell_origin: CellCoord::new(rect.origin.row, rect.origin.col + gutter_w), - cell_size: crate::cell::CellSize::new(inner_rows, rect.size.cols - gutter_w), - gutter_w, - folds: folds.as_ref(), - }; - // Composition (T M2.9): base text_view paints first, then the - // gutter numbers — before the overlays, so a diagnostic overlay - // can draw its severity sign into the gutter's leading column - // without the gutter's own blank pass erasing it — then each - // overlay in attach order. See [`crate::view::View`]. - window.text_view.render(buf, viewport, grid); - if gutter_w > 0 { - paint_line_number_gutter( - grid, - window, - &rect, - inner_rows, - gutter_w, - folds.as_ref(), - &theme, - ); - } - for overlay in &mut window.overlays { - overlay.render(buf, viewport, grid); - } - paint_local_selection( + paint_window_content( grid, - buf, window, - &rect, - inner_rows, - gutter_w, + buf, + placement, folds.as_ref(), - &theme, - ); - // Mode line for this window. Painted last so the line - // itself is always visible regardless of overlay activity. - let coord = window - .text_view - .pos_to_display(buf, window.cursor) - .unwrap_or_default(); - // Arc 6 Stage 2 (Q#FD18): All/Top/Bot/% are reckoned in - // VISIBLE-line space — a buffer whose remainder is collapsed - // reads "All", not "Top". The cursor's ordinal anchors on its - // visible head, since that is the row it renders on. - let (ind_top, ind_total, ind_cursor) = match folds.as_ref() { - Some(map) => ( - map.visible_rows_between(0, window.view_top), - map.visible_line_count(window.text_view.line_count()), - map.visible_rows_between(0, map.visible_head_of(coord.row as usize)), - ), - None => ( - window.view_top, - window.text_view.line_count(), - coord.row as usize, - ), - }; - let scroll = format_scroll_indicator(ind_top, inner_rows as usize, ind_total, ind_cursor); - // Lock scoped to the summary computation only: the overlay - // renders above include `DiagnosticView`, which takes this - // same mutex — holding the guard across the loop deadlocked - // the daemon on the first frame after a file (and thus a - // diagnostic overlay) was opened. - let diags = { - let guard = diag_store.lock().expect("diag store mutex poisoned"); - diag_mode_line_summary(&guard, buf) - }; - let custom = statusline_by_window.get(id); - paint_mode_line( - grid, - &rect, - buf.name(), - buf.is_modified(), *id == active, - coord.row, - coord.col, - &scroll, - &diags, - mode_line_style(&theme), - custom.map_or(&[], |segments| segments.left.as_slice()), - custom.map_or(&[], |segments| segments.right.as_slice()), &theme, + statusline_by_window.get(id), + &diag_store, ); } drop(reg); diff --git a/tests/bottom_panel_stage2a_acceptance.rs b/tests/bottom_panel_stage2a_acceptance.rs new file mode 100644 index 0000000..5f7996d --- /dev/null +++ b/tests/bottom_panel_stage2a_acceptance.rs @@ -0,0 +1,377 @@ +// bottom_panel_stage2a_acceptance.rs --- bottom-panel Stage 2A +// (docs/bottom-panel-stage2-framing.md, criteria A2A-1 / A2A-2 / A2A-3). + +//! Classified §1.3 census routing + the per-window painter extraction. +//! No wire change. +//! +//! **The negative half is the load-bearing half.** A suite that only +//! proved "the document surface is used" would pass with the focus, +//! focus-chrome, and focus/session consumers *wrongly* rerouted to the +//! document — which is the defect the framing spent three review rounds +//! eliminating, and which would break remote-op validation, +//! `DispatchIdle`, presence, focused search/menu/completion routing, and +//! terminal bell ownership. So every Projection assertion here is paired +//! with a focus-class assertion taken in the *same* state. + +use pmacs::cell::{CellGrid, CellSize}; +use pmacs::editor::EditorState; +use pmacs::protocol::FrontendId; +use pmacs::window::{Side, WindowId}; + +const ROWS: u32 = 24; +const COLS: u32 = 60; + +fn editor() -> EditorState { + let s = EditorState::new(); + exec(&s, "pmacs.lsp.config = {}"); + s.sync_frame_geometry(FrontendId::LOCAL, CellSize::new(ROWS, COLS)); + s +} + +fn exec(s: &EditorState, src: &str) { + s.lua_host.lua().load(src.to_string()).exec().unwrap(); +} + +fn side_window(s: &EditorState) -> Option { + let core = s.core.borrow(); + core.views[&FrontendId::LOCAL] + .layout + .iter_ids() + .into_iter() + .find(|id| { + core.windows + .get(id) + .is_some_and(|w| w.params.side.is_some()) + }) +} + +/// Open a bottom panel and leave it FOCUSED — the state in which every +/// classification difference becomes observable. +fn focused_panel(s: &EditorState) -> (WindowId, WindowId) { + let document = s.core.borrow().views[&FrontendId::LOCAL].active; + exec( + s, + "PANEL_BUF = pmacs.buffer.create(\"*panel*\") + PANEL_WIN = pmacs.window.display(PANEL_BUF, \ + { side = \"bottom\", height = 4 })", + ); + let panel = side_window(s).expect("panel exists"); + s.core.borrow_mut().focus_window(FrontendId::LOCAL, panel); + assert_eq!( + s.core.borrow().views[&FrontendId::LOCAL].active, + panel, + "fixture precondition: the panel must own focus" + ); + (document, panel) +} + +fn render(s: &EditorState) { + let size = CellSize::new(ROWS, COLS); + let mut cells = vec![pmacs::cell::Cell::default(); (ROWS * COLS) as usize]; + let mut grid = CellGrid { + cells: &mut cells, + stride: size.cols, + size, + }; + let _ = pmacs::editor::paint_frame( + s, + FrontendId::LOCAL, + &std::collections::HashMap::new(), + &mut grid, + size, + ); +} + +// --------------------------------------------------------------------------- +// A2A-1 — the Projection class resolves the document surface +// --------------------------------------------------------------------------- + +#[test] +fn projection_resolves_the_document_window_while_a_panel_is_focused() { + let s = editor(); + let (document, panel) = focused_panel(&s); + let core = s.core.borrow(); + + assert_eq!( + core.primary_document_window(FrontendId::LOCAL), + Some(document), + "Projection consumers must resolve the document window, not the focused panel" + ); + assert_ne!(document, panel); +} + +#[test] +fn projection_buffer_is_the_document_buffer_not_the_panel_buffer() { + let s = editor(); + let (document, _panel) = focused_panel(&s); + let core = s.core.borrow(); + + let document_buffer = core.windows[&document].buffer_id; + assert_eq!( + core.primary_document_buffer(FrontendId::LOCAL), + Some(document_buffer), + "the replica's document mirror must not follow panel focus" + ); + assert_ne!( + core.primary_document_buffer(FrontendId::LOCAL), + Some(core.windows[&core.views[&FrontendId::LOCAL].active].buffer_id), + "non-vacuity: the focused window's buffer differs, so this test can fail" + ); +} + +// --------------------------------------------------------------------------- +// A2A-1 — the NEGATIVE half: focus classes still resolve focus +// --------------------------------------------------------------------------- + +#[test] +fn focus_class_dispatch_idle_still_tracks_the_focused_window() { + let s = editor(); + let (_document, _panel) = focused_panel(&s); + + // §1.3 #14 — Focus. Q#BP14a: optimistic input is gated per WINDOW. + // A panel that owns focus must suppress `DispatchIdle` even though + // the *document* projection is unaffected. + assert!( + !s.dispatch_idle_for(FrontendId::LOCAL), + "a focused side window must gate optimistic input off (#14)" + ); +} + +#[test] +fn focus_class_gate_lifts_when_focus_returns_to_the_document() { + let s = editor(); + let (document, _panel) = focused_panel(&s); + s.core + .borrow_mut() + .focus_window(FrontendId::LOCAL, document); + + assert!( + s.dispatch_idle_for(FrontendId::LOCAL), + "non-vacuity: the gate must lift with focus, or the test above proves nothing" + ); +} + +#[test] +fn focus_and_projection_disagree_in_the_same_state() { + // The single most important assertion in this suite: in ONE state, + // the two classes must resolve DIFFERENT windows. If a future change + // routes the focus class through `primary_document_window`, this + // fails even though every Projection test above still passes. + let s = editor(); + let (document, panel) = focused_panel(&s); + let core = s.core.borrow(); + + let focused = core.views[&FrontendId::LOCAL].active; + let projected = core + .primary_document_window(FrontendId::LOCAL) + .expect("a document window exists"); + + assert_eq!(focused, panel, "focus authority must name the panel"); + assert_eq!( + projected, document, + "projection authority must name the document" + ); + assert_ne!( + focused, projected, + "the two authorities must be genuinely distinct in this state" + ); +} + +// --------------------------------------------------------------------------- +// A2A-2 — the statusline split: lookup reroutes, `active` does not +// --------------------------------------------------------------------------- + +#[test] +fn statusline_document_context_reports_active_false_under_a_focused_panel() { + use pmacs::statusline::{ + StatuslineEvaluationOutcome, StatuslineEvaluationTarget, evaluate_statusline, + }; + + let s = editor(); + let (document, _panel) = focused_panel(&s); + let declared = s.core.borrow().windows[&document].buffer_id; + + let evaluation = evaluate_statusline( + s.lua_host.lua(), + &s.core, + &s.statusline_registry, + StatuslineEvaluationTarget::Semantic { + frontend_id: FrontendId::LOCAL, + declared_buffer: declared, + }, + ); + + match evaluation.outcome { + StatuslineEvaluationOutcome::Ready(windows) => { + let context = windows + .first() + .map(|segments| segments.context) + .expect("one document context"); + // The LOOKUP rerouted: it resolved the document window even + // though the panel is focused (§1.3 #12). + assert_eq!( + context.window_id, document, + "the semantic target must resolve the primary document window" + ); + // `active` did NOT reroute (parent acceptance 42): a document + // provider observes the truth, that it is not focused. + assert!( + !context.active, + "a document provider must observe active = false while the panel owns focus" + ); + } + other => panic!("expected a ready evaluation, got {other:?}"), + } +} + +#[test] +fn statusline_document_context_is_active_when_the_document_is_focused() { + use pmacs::statusline::{ + StatuslineEvaluationOutcome, StatuslineEvaluationTarget, evaluate_statusline, + }; + + // Non-vacuity for the assertion above: with focus on the document, + // the same context must report `active = true`. + let s = editor(); + let (document, _panel) = focused_panel(&s); + s.core + .borrow_mut() + .focus_window(FrontendId::LOCAL, document); + let declared = s.core.borrow().windows[&document].buffer_id; + + let evaluation = evaluate_statusline( + s.lua_host.lua(), + &s.core, + &s.statusline_registry, + StatuslineEvaluationTarget::Semantic { + frontend_id: FrontendId::LOCAL, + declared_buffer: declared, + }, + ); + + match evaluation.outcome { + StatuslineEvaluationOutcome::Ready(windows) => { + let context = windows.first().map(|s| s.context).expect("one context"); + assert!(context.active, "a focused document context must be active"); + } + other => panic!("expected a ready evaluation, got {other:?}"), + } +} + +// --------------------------------------------------------------------------- +// A2A-3 — the painter extraction preserves grid behavior +// --------------------------------------------------------------------------- + +#[test] +fn extraction_preserves_cells_cursor_and_focused_view_top() { + // The extraction must preserve four things, not just cells: a clamp + // that silently moved to the WRONG window would leave the painted + // cells identical on a single-window frame. + let s = editor(); + exec( + &s, + "local b = pmacs.buffer.create(\"*doc*\") + b:insert(0, string.rep(\"line\\n\", 200)) + pmacs.window.display(b, {})", + ); + + let size = CellSize::new(ROWS, COLS); + let mut cells_a = vec![pmacs::cell::Cell::default(); (ROWS * COLS) as usize]; + let mut grid_a = CellGrid { + cells: &mut cells_a, + stride: size.cols, + size, + }; + let cursor_a = pmacs::editor::paint_frame( + &s, + FrontendId::LOCAL, + &std::collections::HashMap::new(), + &mut grid_a, + size, + ); + let active = s.core.borrow().views[&FrontendId::LOCAL].active; + let view_top_a = s.core.borrow().windows[&active].view_top; + + // A second identical paint is a fixed point: same cells, same + // returned cursor, same `view_top`. + let mut cells_b = vec![pmacs::cell::Cell::default(); (ROWS * COLS) as usize]; + let mut grid_b = CellGrid { + cells: &mut cells_b, + stride: size.cols, + size, + }; + let cursor_b = pmacs::editor::paint_frame( + &s, + FrontendId::LOCAL, + &std::collections::HashMap::new(), + &mut grid_b, + size, + ); + let view_top_b = s.core.borrow().windows[&active].view_top; + + assert_eq!(cells_a, cells_b, "painted cells must be stable"); + assert_eq!(cursor_a, cursor_b, "the returned cursor must be stable"); + assert_eq!(view_top_a, view_top_b, "focused view_top must be stable"); +} + +#[test] +fn extraction_leaves_a_passive_window_view_top_untouched() { + // The auto-scroll clamp runs for the FOCUSED window only. A passive + // window's scroll state must survive a frame it did not own. + let s = editor(); + exec( + &s, + "local b = pmacs.buffer.create(\"*doc*\") + b:insert(0, string.rep(\"line\\n\", 200)) + pmacs.window.display(b, {}) + pmacs.window.split_horizontal()", + ); + render(&s); + + let (passive, before) = { + let core = s.core.borrow(); + let view = &core.views[&FrontendId::LOCAL]; + let passive = view + .layout + .iter_ids() + .into_iter() + .find(|id| *id != view.active) + .expect("a second window exists"); + (passive, core.windows[&passive].view_top) + }; + + // Scroll the passive window somewhere the clamp would "fix" if it + // ever ran against the wrong window. + s.core + .borrow_mut() + .windows + .get_mut(&passive) + .unwrap() + .view_top = 120; + render(&s); + + assert_eq!( + s.core.borrow().windows[&passive].view_top, + 120, + "a passive window's view_top must not be clamped by another window's frame" + ); + assert_ne!(before, 120, "non-vacuity: the value actually changed"); +} + +// --------------------------------------------------------------------------- +// Fixture integrity +// --------------------------------------------------------------------------- + +#[test] +fn the_panel_fixture_really_builds_a_side_window() { + // Every test above is worthless if `focused_panel` silently produced + // an ordinary split, so pin the fixture's own precondition. + let s = editor(); + let (_document, panel) = focused_panel(&s); + let core = s.core.borrow(); + assert_eq!( + core.windows[&panel].params.side, + Some(Side::Bottom), + "the fixture must produce a real bottom side window" + ); +} From 4413ea93d00d3bfe3668d03c93b23f09ce1a6075 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 22:14:37 -0400 Subject: [PATCH 05/14] docs: record the Stage 2A lane and what gating it found MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ledger entry for the in-flight Stage 2A branch, plus three findings the gate run produced that are worth carrying regardless of this PR: - The structural test comparing the two authorities directly did NOT catch the focus-class bite; only the consumer-level assertion did. Both kinds are needed, and the distinction generalizes. - `vterm_stage3_acceptance::a37` is badly flaky on this machine — 6/8 failures on the BASE commit against 7/8 on the branch in matched isolated samples, so it is pre-existing rather than a regression. It also returns `ok` without running unless `pmacs-gpu` is built. - `m11_5_semantic_acceptance` reports 0 tests and `gpu_initial_target_acceptance` reports 1 without `--features crdt`. Both are semantic-census suites, so gating Stage 2A in the default config alone would exercise almost none of its relevant coverage. Co-Authored-By: Claude Opus 5 (1M context) --- docs/active-work.md | 41 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index b60d62c..b961794 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -389,10 +389,45 @@ If it does not, stop and repair the remote/fetch configuration. **isolated-config workspace sweep 3,177 across 92 suites, zero failures**; `git diff --check` clean. Gates were run against the committed tree. -## Bottom-panel lane (Arc 7) — Stage 1 MERGED; Stage 2 IN FRAMING +## Bottom-panel lane (Arc 7) — Stage 1 + framing MERGED; Stage 2A IN REVIEW -Stage 1 is on `main`. **Stage 2 is in framing**, no implementation in -flight. +Stage 1 and the Stage 2 framing are on `main`. **Stage 2A is +implemented and in review.** + +- **Stage 2A — portable branch `githubsucks/bottom-panel-stage2a`**, + worktree `../pmacs-bp-stage2a`, based on `githubsucks/main` @ + `c93f9ee`. Two commits: the classified census routing, then the + painter extraction + acceptance. **No protocol change; no behavior + change for any frontend today** — with `panel_capable = false` for + semantic sessions, `primary_document_window` returns `view.active` + in every existing configuration, so this is seam adoption that + becomes load-bearing in 2B. +- Verification on this branch: `cargo fmt --check` clean; strict + workspace Clippy clean; **1,832 default + 2,009 CRDT** library tests; + new `bottom_panel_stage2a_acceptance` 10/10; bottom-panel Stage 1 + 46; statusline segments 7 default / 8 CRDT; m11_5 semantic 2 CRDT; + GPU initial target 14 CRDT; vterm Stage 1/2 10 / 6; folding Stage 2 + 48; M4 121; required GPU 202; `git diff --check` clean. +- **Both key routings were falsified by revert.** Rerouting + `dispatch_idle_for` (#14, Focus) through `primary_document_window` + fails `focus_class_dispatch_idle_still_tracks_the_focused_window`; + reverting the statusline lookup (#12, Projection) to `view.active` + fails the document-context test. Worth recording: the *structural* + test `focus_and_projection_disagree_in_the_same_state` did **not** + catch the first bite — it compares the two authorities directly, so + only a consumer-level assertion catches a misrouted consumer. Keep + both kinds. +- **`vterm_stage3_acceptance::a37` is a pre-existing flake here**, not a + Stage 2A regression: measured **6/8 failures on the base commit** and + **7/8 on the branch** in matched isolated samples. It needs a real + daemon + real PTY + headless GPU and is documented load-sensitive. + It also silently returns `ok` unless `pmacs-gpu` has been built, and + is `crdt`-gated so CI never runs it at all. +- **Two suites are dark without `--features crdt`**: + `m11_5_semantic_acceptance` reports **0 tests** and + `gpu_initial_target_acceptance` reports **1** in the default config. + Both are semantic-census suites, so Stage 2A must be gated with the + feature on or its most relevant coverage never executes. - Stage 1 merged as **#155** (`main` @ `e745068`, 2026-07-24, after two review rounds). No protocol change. Durable substrate facts live in From 3b54c784949847bd47b7b03f2ce91da2453cb88f Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:10:06 -0400 Subject: [PATCH 06/14] =?UTF-8?q?docs(lean4):=20rev=206=20=E2=80=94=20re-s?= =?UTF-8?q?cout=20Stage=204=20and=20split=20it=20into=204a=20and=204b?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against main @ d400f30 produced six findings that change the plan and three that confirm it. The pmacs-side facts were verified in a worktree at that commit; the upstream facts by reading leanprover/vscode-lean4 @ 17d1d08. The split: Stage 4's risk column read "refactors pair.lua's provenance read" — every language's auto-pairing — for a stage the prose called the Lean input method, which is exactly the rule §4 states and exactly what round 4 found for Stage 3. Rev 5 had noticed the shape and answered it with a commit boundary; a commit boundary is not a review boundary. Stage 4a is now the typed-edit consumer chain (substrate, no Lean) and 4b the input method. Rev 5's expansion semantics were wrong in three ways. Resolution is the shortest key having the input as a prefix (\al yields ∀ from `all`, not `alpha`); there is no terminator list at all ('+ ' is a key, so space extends after \+; '\' is a key, so \\ yields \); and an unmatchable tail is appended rather than dropped (\alp7 yields α7). Three further findings. There is no cursor-motion hook, so acceptance 43 as written was not buildable and abandonment is lazy. dispatch_key is only half of 4b's production path — \ and the letters are not excluded from the optimistic classifier, and that producer is crdt-gated, so a crdt-gated integration test is dark in CI and dark in the gate list. And the whole expansion has cross-peer-degraded undo, a wider bite than Q#LN6's three bracket pairs; set_round_trip_input would fix it and is rejected with reasons. New decisions Q#LN21 (undo degradation) and Q#LN22 (the state machine); Q#LN10 and Q#LN11 rewritten; §2.11 records the upstream algorithm; §9.1 states the coherence impact for both stages. Acceptance keeps its existing numbers and adds letter suffixes on both sides of the split. Citation sweep per COHERENCE §25: five live citations moved in the 50 commits since rev 5. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 73 +++- docs/lean4-mode-framing.md | 703 +++++++++++++++++++++++++++++++------ 2 files changed, 667 insertions(+), 109 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index e4f0859..52d44ba 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -14,11 +14,13 @@ backlog. machine-local: `origin` may name this canonical URL, a release mirror, or something else, and therefore has no authority by name alone. - Canonical base at this snapshot: - `githubsucks/main` @ `d152120` (the bottom-panel landed-doc refresh #156 - atop the inline-math slice #158, dired Stage 1 #165, the GPU terminal - input fix #166, Lean 4 Stage 2 #161, the dired framing #164, - COHERENCE.md #163, find-file #162, Lean 4 Stage 1 #160, and the minimap - blank-slab fix #159; protocol v20). + `githubsucks/main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a + #167, the bottom-panel landed-doc refresh #156, the inline-math slice + #158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 + Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file + #162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159; + protocol v20). The previous snapshot named `d152120`; the recovery + check below accepts it or anything newer. - On the transfer source, `origin/main` named a release mirror at `d3fa632` and lagged badly. On the current destination, `origin` names the canonical URL. This difference is why all recovery begins by @@ -55,7 +57,7 @@ git status --short --branch The `git log` command must expose `d152120` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED +## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review round, all twelve checks green). Branch `githubsucks/lean4-stage1` @@ -189,7 +191,7 @@ 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`) +### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`) - Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @ `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first @@ -253,7 +255,7 @@ If it does not, stop and repair the remote/fetch configuration. `#[cfg(unix)]` is NOT sufficient for such a fixture — `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. -### Stage 3b — the Lean language server (branch `lean4-stage3b-server`) +### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`) - Same worktree `../pmacs-lean-stage3`, **branched off `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response @@ -463,6 +465,61 @@ If it does not, stop and repair the remote/fetch configuration. describes the pushed tree; recording it late is the #161 fmt-blocker error in a slower form.) +### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) + +- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** + (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main + that had advanced 50 commits mid-review; the only conflict either time + was this ledger's own lane headings, resolved by keeping both sides. +- Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. + Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No + code. Awaiting user approval before implementation, per the workflow. +- **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).** + 4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua` + plus `pair.lua` re-expressed as one registered consumer, no behavior + change. 4b is the input method. The split is forced by §4's own rule, + which Stage 4's risk column ("refactors `pair.lua`'s provenance read") + broke while the prose called the stage Lean-only. +- **This is the SECOND consecutive re-scout to find that rule broken** + (round 4 found it for Stage 3). Rev 5 had even noticed the shape and + answered it with a commit boundary. **A commit boundary is not a review + boundary.** Re-check every remaining stage against §4 at scout time; + the rule is not self-enforcing. +- **Rev 5's expansion semantics were wrong in three ways**, found by + reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring + from behavior. Resolution is *shortest key having the input as a + prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no + terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'` + is a key, so `\\` → `\`); and an unmatchable tail is **appended**, + not dropped (`\alp7` → `α7`). +- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving + the cursor out abandons it") was not buildable. Abandonment is lazy — + validated at the next typed edit — and the criterion now asserts what + pmacs can actually detect. Upstream drives this off `changeSelections`; + that seam does not exist here. +- **`dispatch_key` is only half the production path for 4b.** The + auto-pair suite gets away with dispatch-only because Q#AP1 removed the + pair chars from the optimistic classifiers; `\` and the letters are + NOT excluded, so on a CRDT frontend the optimistic producer is the real + path. That producer is `#[cfg(feature = "crdt")]` and CI never enables + `crdt`, and the gate list runs `--features crdt` only for `--lib` — a + crdt-gated integration test is **dark twice over**. +- The whole expansion has cross-peer-degraded undo (Q#LN21): six + source-peer optimistic inserts replaced by one daemon-peer op. + `set_round_trip_input` would fix it and is rejected — it also disables + `dispatch_idle`, so RET stops inserting a newline. +- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all + keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are + proper prefixes of another (so 1,550 expand eagerly), **26** values + carry `$CURSOR`, **93** are multi-codepoint. +- Citation sweep per COHERENCE §25: five live citations moved in the 50 + commits since rev 5 — `take_typed_edit` 12827→12990, + `handle_server_requests` 1549→1815, `fs.stat` 93→133, + `detect_buffer_language` 452→457, `send_request`/`send_notification` + 9342/9361→9507/9527. +- Verification: none yet — the branch carries no code. `git diff --check` + clean. + ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) - Approved framing: `docs/dired-framing.md` **revision 6** — rev 5 is the diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index ec62980..e39eb36 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -6,7 +6,7 @@ pmacs has no Lean support of any kind: `grep -rin lean` over `*.rs`, plain buffer — no grammar, no major mode, no comment syntax, no pair set, no server. -This lane closes that in eight stages. Stage boundaries are drawn where +This lane closes that in nine stages. Stage boundaries are drawn where the *substrate* changes, not where the feature list does — see §4. §9 states the lane's coherence impact per `COHERENCE.md` §20. @@ -21,11 +21,12 @@ the *substrate* changes, not where the feature list does — see §4. #144 (LaTeX), #146 (HTML+CSS). Stage 1 is that pattern almost exactly. - Stages 2 and 4–6 are **not** that pattern, and none should be mistaken for a one-liner. Stage 2 changes `ensure_server`, shared by every LSP - language. Stage 4 builds the editor's first input method. Stage 5 is the + language. Stage 4a changes how typed-character provenance is consumed + and Stage 4b builds the editor's first input method. Stage 5 is the first consumer of a non-standard LSP method family. Stage 6 adds a severity-routing policy to `LspServerSpec`. - The user's stated north star is **matching or exceeding what VS Code - does with Lean**. §5's bet 6 scores honestly how close the eight stages get + does with Lean**. §5's bet 6 scores honestly how close the nine stages get and names precisely what is still missing. Parallel-safety: Stage 1 touches `Cargo.toml`, `src/syntax.rs`, @@ -283,10 +284,131 @@ rather than a bare root), `ensure_server` 527 → **610**, pre-#161 line numbers inside Q#LN15 are left as written: that stage has landed and its citations are historical record, not navigation. +### Round 5 (rev 5 → rev 6) — Stage 4 re-scout and split + +Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main` +@ `d400f30` produced **six findings that change the plan** and three +that confirm it. The pmacs-side facts were verified in a worktree at +that commit; the upstream facts were verified by downloading and reading +`leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the +algorithm, not its documentation, since the `lean4-unicode-input` +package ships no README. + +1. **Stage 4 violated this document's own splitting rule — the same way + Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting + substrate change with Lean feature content," and §4's own risk column + for Stage 4 read *"refactors `pair.lua`'s provenance read."* + `pair.lua` is every language's auto-pairing; the refactor is + cross-cutting substrate by exactly the test that split out stages 2 + and 3a. Rev 5 already conceded the shape without acting on it — + Q#LN10 said the refactor "lands *first*, as its own commit with no + behavior change, so a regression bisects cleanly." A commit boundary + is not a review boundary. **Stage 4 is now 4a (the typed-edit + consumer chain, no Lean) and 4b (the input method).** Confirmed + `pair.lua:226` is still the **only** production `take_typed_edit` + caller; the other eight call sites are all in + `tests/auto_pair_acceptance.rs`. +2. **The expansion semantics in rev 5's Q#LN10 were wrong in three + ways.** Reading `AbbreviationProvider.ts` and `TrackedAbbreviation.ts` + rather than inferring from behavior: + - Rev 5 said expansion fires on "a unique complete match that no + longer key extends." Upstream's rule is + `findSymbolsByAbbreviationPrefix(abbrev)[0]` — the symbol of the + **shortest key having `abbrev` as a prefix**. `\alp` + space is not + a failure; it yields `α`, because `alpha` is the shortest key + starting with `alp`. Verified against the table: `\al` → `∀`, from + `all`, not from `alpha`. + - Rev 5 named "an explicit terminator (space, tab, RET, or a second + `\`)." **There is no terminator list upstream.** A character + terminates iff extending the pending key by it leaves zero prefix + matches. Space usually does — but `'+ '` **is a key** (one of + 1,855), so after `\+` a space extends rather than terminates. And a + second `\` is not a terminator either: `'\'` is a key mapping to + `\`, so `\\` extends, matches uniquely, and expands to a single + backslash. It terminates only when the pending key is non-empty and + no key extends it. + - Rev 5 did not carry the suffix rule at all. When no key has + `abbrev` as a prefix, upstream recurses on `abbrev` minus its last + character and **appends the leftover**: `\alp7` → `α7`. Dropping + this makes a large class of real input silently unexpandable. +3. **There is no cursor-motion hook, so acceptance 43 as written cannot + be built.** The Rust core fires exactly eight named hooks + (`builtin/hooks/default.lua`): `buffer.before-save`, + `buffer.after-load`, `buffer.after-edit`, `buffer.after-switch`, + `buffer.after-save`, `editor.before-quit`, `frontend.detached`, + `process.after-tick`. Upstream drives abandonment off + `changeSelections`, a seam pmacs does not have. Abandonment must + therefore be **lazy** — validated at the next typed edit against the + pending region — which changes what acceptance 43 can assert. Q#LN22 + states the state machine this forces. +4. **`dispatch_key` is only half of Stage 4b's production path.** Rev 5 + inherited the auto-pairing suite's dispatch-driven harness without + noticing why that harness is sufficient *there*: Q#AP1 removed the + pair characters from both optimistic classifiers, so for pair chars + dispatch **is** production. `\` and the ASCII letters are not + excluded — `classify_key` returns `Insert(c)` for them + (`src/optimistic.rs:144`: `Char(c) if !c.is_control() && + !is_builtin_pair_char(c)`), so on a CRDT frontend an abbreviation is + typed entirely through the *optimistic* producer, which arms the same + record from `handle_remote_crdt_op` (`src/daemon.rs:3965` pins the + classification). A dispatch-only Stage 4b suite would pin the path + real users do not take. The trap underneath: that producer is + `#[cfg(feature = "crdt")]`, and CI never enables `crdt` — so a + crdt-gated integration test is dark twice over, since the required + gate list runs `--features crdt` only for `--lib`. Q#LN22 and §7 say + what to do about it instead of discovering it in review. +5. **The whole expansion has cross-peer-degraded undo, and it is a + larger bite than `⟨⟩`'s.** Q#LN6 already accepts this for three + bracket pairs. But there the mismatch is one optimistic opener + against one daemon-peer closer; here the user's `\alpha` is six + source-peer optimistic inserts and the expansion is a single + daemon-peer `replace` **over all six**. Q#LN21 takes the decision — + including why `pmacs.buffer.set_round_trip_input`, which already + exists and would fix it, is the wrong instrument. +6. **The table's shape is sharper than "1,855 entries."** Re-counted at + `17d1d08`: 1,855 entries, all `string → string`, **all keys ASCII**, + longest key 25 characters, 36,861 bytes of JSON. **64** keys contain + a `lean4` pair-set character (rev 5's number, reproduced exactly). + Three numbers rev 5 did not have and the algorithm needs: **305** + keys are proper prefixes of another key (so 1,550 are eager-expandable + on uniqueness and 305 are not), **26** values carry `$CURSOR` (not + just `\<>`), and **93** values are multi-codepoint. Two values contain + a backslash — `n` → `\n` and `setminus` → `\` — which is why upstream + needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs + does not. + +Confirmations, recorded because each was load-bearing and unverified: + +7. **`take_typed_edit`'s one-shot contract is unchanged** + (`src/editor_core.rs:4047`): per-frontend, cleared by the producer + when the fan-out returns, nil to a nested manual `hook.run`. The + hazard rev 5 built Q#LN10 around is real and still the reason 4a + exists. +8. **Load order still constrains the chain.** `pair.lua` loads at + `src/editor.rs:430` and `lsp.lua` at `:436`, and Q#AP7's reason + holds: `lsp.lua`'s `buffer.after-edit` callback synchronously flushes + `didChange` on the signature-trigger path. An expansion that landed + after that flush would send the server the unexpanded text. +9. **Embedding the table needs no special machinery.** Every builtin + runtime chunk is an `include_str!`, and `lsp.lua` is already 111 KB + of the 414 KB total. A ~45 KB generated Lua table is within the + existing practice, so Q#LN11 embeds it rather than inventing a + lazy-load path. + +Citation drift repaired per COHERENCE §25, on the same terms as round +4's sweep. Five live citations moved in the 50 commits since rev 5: +`take_typed_edit` 12827 → **12990**, `handle_server_requests` 1549 → +**1815**, `fs.stat` 93 → **133**, `detect_buffer_language` 452 → +**457**, and `send_request`/`send_notification` 9342/9361 → +**9507**/**9527**. Left as written: the pre-#161 numbers inside Q#LN15 +and the revision-history entries above, which are historical record +rather than navigation. + ## 1. What ships -Eight stages, after round 4 split Stage 3. The north star is VS Code -parity; the honest statement of where that lands is in §5, bet 6. +Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The +north star is VS Code parity; the honest statement of where that lands +is in §5, bet 6. **Stage 1 — grammar, mode, and the editing table stakes.** `.lean` files highlight, carry a `lean4` major mode, and get comment-toggle and @@ -315,10 +437,19 @@ on 3a's seam. Adds `textDocument/waitForDiagnostics`. Diagnostics, hover, completion, goto-definition, document symbols, and semantic tokens all arrive through the existing typed surfaces. -**Stage 4 — the Unicode input method.** Typing `\alpha` produces `α`, +**Stage 4a — the typed-edit consumer chain.** Pure substrate, no Lean +content, split from Stage 4 in round 5 for the reason stages 2 and 3a +were: it changes machinery every language runs through. The one-shot +`take_typed_edit()` record stops being auto-pairing's private property +and becomes a small ordered chain that reads it once and offers it to +registered consumers. `pair.lua` becomes the chain's first and only +consumer, with no behavior change. + +**Stage 4b — the Unicode input method.** Typing `\alpha` produces `α`, `\to` produces `→`, `\<>` produces `⟨⟩` with the point between them. -1,855 abbreviations vendored from vscode-lean4. This is the stage that -makes Lean actually typable in pmacs. +1,855 abbreviations vendored from vscode-lean4, registered as a chain +consumer ahead of auto-pairing. This is the stage that makes Lean +actually typable in pmacs. **Stage 5 — the goal view.** A `*lean-goal*` panel that renders `$/lean/plainGoal` at the point, refreshed on a debounced tick and on @@ -405,7 +536,7 @@ injections_query }`. Adding a grammar is one entry plus one `Cargo.toml` line; the doc comment at `src/syntax.rs:756` says exactly this and it has held for every grammar since. -`builtin/runtime/syntax.lua:452` `detect_buffer_language` resolves, in +`builtin/runtime/syntax.lua:457` `detect_buffer_language` resolves, in order: modeline → `pmacs.parse.language_for_path` (the grammar extension table) → `pmacs.lsp.filetypes[ext]` → `pmacs.parse.language_from_filename` → shebang. A grammar entry claiming `lean` therefore resolves `.lean` @@ -486,13 +617,13 @@ and pin it.* - `pmacs.lsp` already exposes generic `send_request(id, method, params)` → request id and `send_notification(id, method, params)` - (`src/lua_bindings/mod.rs:9342`, `:9361`). Non-standard methods need no + (`src/lua_bindings/mod.rs:9507`, `:9527`). Non-standard methods need no new Rust to *send*. - `LspEventKind` (`src/lsp.rs:264`) has generic `Notification { method, params }` and `Response { id, result, error, method }` variants. Unknown server methods are delivered, not dropped. - **But `events_take` has exactly one consumer**: `handle_server_requests` - at `builtin/runtime/lsp.lua:1549`, driven off `pmacs._async.tick`. It + at `builtin/runtime/lsp.lua:1815`, driven off `pmacs._async.tick`. It `take`s — a drain. Its `if/elseif` chain handles five `request` methods and `initialized`, and **ignores every `notification` and every `response`**. A second module calling `events_take` would steal events @@ -556,7 +687,7 @@ character": subscribe to `buffer.after-edit`, gate on `ed.this_command() == "buffer.self-insert"` (`pair.lua:229`), then take the exact provenance record. -`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12827`) returns +`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12990`) returns `{ buffer, window, codepoint, char, requested_start, requested_end, effective_start, effective_end, inserted_len, post_cursor, clean }` — or nil. Its doc comment is explicit: @@ -570,7 +701,19 @@ it on every self-insert. A Lean abbreviation expander that independently calls `take_typed_edit()` in the same `buffer.after-edit` fan-out gets nil or steals it from auto-pairing, depending on hook order — and hook order is not a contract. This is the single load-bearing constraint on Stage 4 and -the reason Stage 4 is its own PR rather than a rider on Stage 1. +the reason Stage 4 is its own PR rather than a rider on Stage 1 — and, +after round 5, the reason its substrate half is Stage 4a rather than a +first commit on a Lean branch. + +Re-verified at `d400f30`: `pair.lua:226` remains the **only** production +caller. The eight other call sites in the tree are all in +`tests/auto_pair_acceptance.rs`. So the chain Stage 4a introduces has +exactly one consumer to migrate, which is what makes a no-behavior-change +substrate PR possible at all. + +Two producers arm the record, not one, and §2.11 is where that matters: +the dispatch fallback and — under `#[cfg(feature = "crdt")]` — the +optimistic CRDT arm reached from `handle_remote_crdt_op`. Related, from `pair.lua:30`'s Q#AP1 note: only the nine built-in pair chars `()[]{}"'` and backtick are excluded from the frontends' optimistic @@ -680,6 +823,78 @@ The publish path absorbs into the Rust store *and* still delivers the notification to `events_take`, so Lua can observe them; but suppressing them from the store needs a Rust-side policy, not a Lua filter. Q#LN18. +### 2.11 The upstream input method (external, verified by reading it) + +Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`, +package `lean4-unicode-input`, files `AbbreviationProvider.ts`, +`TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`, +`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no +README, so the algorithm below is read off the source. Apache-2.0. + +**Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key +having `p` as a prefix, sorts them by **key length ascending**, and maps +to symbols. `getReplacementText(a)`: + +1. If any key has `a` as a prefix, return the shortest such key's symbol. +2. Otherwise recurse on `a` minus its last character; if that yields + something, return it **with the dropped character appended**. +3. Otherwise undefined — no expansion. + +Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`), +`al` → `∀` (via `all`, *not* `alpha` — shortest wins, and this is +surprising enough to be worth an acceptance criterion), `alp7` → `α7` +via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches). + +**Tracking.** The leader `\` is inserted into the buffer like any other +character, and the tracked range starts after it; the replaced range +spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the +buffer literally shows `\alpha` until expansion, then that whole span +becomes `α`. + +**Termination.** There is no terminator set. On each typed character +`c`, if `findSymbolsByAbbreviationPrefix(a .. c)` is empty the +abbreviation is marked `finished`, **`c` is not absorbed into it**, and +the pending text expands before `c` lands. Otherwise `c` extends the +key. Two consequences the obvious "space ends it" model gets wrong: + +- `'+ '` is a key, so after `\+` a space **extends**. Space is a + terminator by consequence, never by rule. +- `'\'` is a key (→ `\`), so `\\` extends, is uniquely complete, and + eagerly expands to one backslash. A second `\` terminates only when + the pending key is non-empty and unextendable — at which point the + rewriter starts a *new* tracked abbreviation on it. + +**Eager expansion.** When `eagerReplacementEnabled`, an abbreviation +expands the moment it is *unique and complete*: exactly one key has it +as a prefix, and it is itself a key. 1,550 of the 1,855 keys qualify; +the other 305 are proper prefixes of some other key and must wait for +termination. `\to` is in the first group — it expands with no terminator +typed, which is why acceptance 41 is meaningful and not a restatement of +38. + +**Cursor placement.** `$CURSOR` is stripped from the symbol and its +index becomes the post-expansion point, applied only when the point sat +at the end of the abbreviation. 26 values carry it. + +**Abandonment.** Upstream expands on `changeSelections` — any tracked +abbreviation the cursor has left. pmacs has no cursor-motion hook +(round-5 finding 3), so this seam does not exist here and Q#LN22 makes +abandonment lazy instead. + +**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` → +`\n`, so an expansion can insert a backslash; upstream sets +`doNotTrackNewAbbr` across the replace so that backslash does not open a +new abbreviation. In pmacs the expansion is a programmatic `buf:replace` +that arms no typed-edit record, so the chain sees nothing and cannot +re-arm. The guard is unnecessary here **because of** the provenance +contract, not by accident — and the acceptance must pin it, because a +future consumer that inferred from buffer text rather than provenance +would reintroduce the bug. + +**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a +`Set` and sorts changes bottom-up for that reason; +pmacs has one point, so one pending abbreviation per buffer. + ## 3. Decisions ### Q#LN1 — Bundle `arborium-lean` 2.18; reject `tree-sitter-lean4` @@ -911,7 +1126,7 @@ file's directory. **How the walk tests for the marker — and why not the obvious way.** `pmacs.fs.stat` is asynchronous: it returns an awaitable handle -(`builtin/runtime/fs.lua:93`) that only settles under `:await()` inside a +(`builtin/runtime/fs.lua:133`) that only settles under `:await()` inside a coroutine. The resolver has no coroutine. It runs synchronously inside `ensure_server` ← `attach_buffer` ← the `buffer.after-load` hook, so awaiting is not merely slow there, it is unavailable — and blocking the @@ -1102,86 +1317,192 @@ The binding is general, not Lean-shaped: it serves every future function-valued `root`, and it is what lets #161's doc comment stop warning about a footgun and start naming a fix. -### Q#LN10 — Stage 4 mechanism: one shared provenance read, not two +### Q#LN10 — Stage 4a: one shared provenance read, not two The hazard is §2.6 — `take_typed_edit()` is one-shot and `pair.lua` -already consumes it. +already consumes it. A second independent caller in the same +`buffer.after-edit` fan-out gets nil or steals the record, depending on +hook order, and hook order is not a contract. Decision: **`pair.lua` stops being the sole consumer.** Extract the provenance read into a single `buffer.after-edit` subscriber owned by a -small shared module, which takes the record once and passes it to an -ordered list of typed-edit consumers (auto-pair, Lean abbreviation). -Consumers return whether they handled the edit; the first that does stops -the chain. +small shared module — `builtin/runtime/typed_edit.lua`, loaded +immediately before `pair.lua` — which takes the record once and offers +it to registered consumers in a defined order. A consumer returns +whether it **claimed** the edit; the first that claims stops the chain. -Two consequences worth stating up front: +`pmacs.typed_edit.add_consumer { name = , priority = , +fn = function(rec) ... end }`, lowest priority first, ties broken by +registration order. Priority is an explicit number rather than +load-order-implied because Q#LN22's collision makes ordering +load-bearing, and rev 5's "the abbreviation consumer runs first" is a +claim a reader must be able to check without reconstructing +`src/editor.rs`'s include list. -- This touches `pair.lua`, which is load-bearing for auto-pairing - acceptance. The full pairing suite is a required gate for Stage 4, and - the refactor lands *first*, as its own commit with no behavior change, - so a regression bisects cleanly. -- Ordering is a contract, not an accident, and the collision is real: - **64 of the 1,855 abbreviation keys contain a character in the proposed - `lean4` pair set** — `\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`, - `\{}` → `{$CURSOR}`. With pairing first, typing `\[` inserts `[]` - with the point between, so the pending key is corrupted to `\[]` before - the second `[` is ever typed and `\[[]]` becomes unreachable. The - abbreviation consumer runs first. +**Stage 4a ships this and nothing else.** Its whole content is: +`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer, +and the `include_str!` line. Round 5's finding 1 is why this is a PR and +not a first commit — `pair.lua` is every language's auto-pairing, and a +reviewer looking at a Lean PR should not have to also review a rewrite +of it. - (Rev 1 justified this with `\<>`, which was wrong: `<` is not in the - pair set per Q#LN6, so that key is safe under either order.) +**The no-behavior-change claim must be pinned, not asserted.** The full +`tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must +pass **unmodified** — a suite edited to accommodate the refactor proves +nothing (the recorded lesson: what a test suite pins is its assertions). +Three assertions the existing suite already makes are the load-bearing +ones, because they are what a chain could plausibly break: that a second +`take_typed_edit()` in the same fan-out yields nil, that pairing still +sees the exact record via `_capture_records`, and that the Q#AP7 ordering +against `lsp.lua`'s `didChange` flush still holds. -**The contract that collision exposes:** the abbreviation consumer must -claim a self-insert that **extends an open pending abbreviation**, not -only one that completes an expansion. A consumer that only claims -completed expansions hands every intermediate keystroke to auto-pairing, -which is exactly how `\[` gets corrupted. "Claimed" here means the chain -stops, not that an edit was made. +**What 4a deliberately does not do.** It does not change the `all-must- +succeed` contract, so a consumer that throws still fails the fan-out for +everyone. The chain owner therefore `pcall`s each consumer and reports +through `pmacs.editor.set_status`, matching `pair.lua`'s existing +never-throw-from-after-edit discipline — this is behavior-preserving for +pairing (which already never throws) and is the guardrail 4b needs. -Expansion semantics (matching vscode-lean4 and `lean4-input`): - -- `\` opens a pending abbreviation, tracked per buffer with its start - offset. Every subsequent self-insert that extends it is claimed. The - pending state is abandoned on any non-self-insert command, buffer - switch, or cursor move away from the pending region. -- Expansion fires on a unique complete match that no longer key extends, - or on an explicit terminator (space, tab, RET, or a second `\`). -- The vendored table's `$CURSOR` placeholder becomes the point position - after the replace — this is how `\<>` yields `⟨|⟩`. -- The whole expansion is **one `buf:replace`** — one undo step, one CRDT - op, one effective-edit verification. Same discipline as - `comment.lua`'s Q#CT5. -- Gated by `pmacs.config.define{ name = "lean.abbrev", type = "boolean", - default = true, mutability = "live" }`, read against the *source* buffer - of the typed edit — the `editing.auto-pair` precedent (`pair.lua:44`), - including its round-2 correction to resolve `rec.buffer` rather than - `pmacs.window.buffer()`. - -### Q#LN11 — Stage 4 data: vendor the table, generated, attributed +### Q#LN11 — Stage 4b data: vendor the table, generated, attributed `abbreviations.json` in `leanprover/vscode-lean4` is a flat -`string → string` object of **1,855 entries** (counted, not estimated), -of which **64 contain a character in the `lean4` pair set** — the -collision Q#LN10's ordering exists to handle. vscode-lean4 is Apache-2.0. +`string → string` object of **1,855 entries**, verified at commit +`17d1d08` (2026-05-29), 36,861 bytes, all keys ASCII, longest key 25 +characters. The counts the algorithm depends on, all re-derived from the +file rather than estimated: + +| Count | What it drives | +|---|---| +| 64 keys containing a `lean4` pair-set char | Q#LN22's ordering | +| 305 keys that are proper prefixes of another | which keys can expand eagerly | +| 1,550 keys uniquely-and-completely matching | the eager-expansion set | +| 26 values containing `$CURSOR` | point placement | +| 93 multi-codepoint values | the replace is not one-char-for-many | + +vscode-lean4 is Apache-2.0. Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header -recording source repo, commit, license, and the regeneration command — -the `builtin/queries/latex/highlights.scm` precedent (#144) for -third-party data, extended with provenance because this is a much larger -artifact under a named license. +recording source repo, commit, license, entry count, and the +regeneration command — the `builtin/queries/latex/highlights.scm` +precedent (#144) for third-party data, extended with provenance because +this is a much larger artifact under a named license. -Not fetched at runtime, not a package-manager dependency: the input method -must work offline and on first launch. +Not fetched at runtime, not a package-manager dependency: the input +method must work offline and on first launch. -**Upkeep is a documented manual process, not code.** There is no automatic -sync and none is wanted — an editor that silently re-downloads its input -method has a supply-chain problem, not a feature. The generator script -lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit as its -argument, and rewrites the file including its provenance header. The -header records source commit, license, entry count, and the regeneration -command, so the file is self-describing to whoever next touches it. A -refresh is an ordinary PR with a visible diff — which is the point: the -diff is the review. +**Embedded, not lazily loaded.** ~45 KB of generated Lua joins the 414 KB +of builtin runtime already compiled in by `include_str!`, of which +`lsp.lua` alone is 111 KB. Inventing a lazy-load path for an 11% increase +would be new machinery bought with no measurement, and the arithmetic is +stated here so a reviewer can disagree with it on numbers. + +**Upkeep is a documented manual process, not code.** There is no +automatic sync and none is wanted — an editor that silently re-downloads +its input method has a supply-chain problem, not a feature. The generator +script lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit +as its argument, and rewrites the file including its provenance header, +so the file is self-describing to whoever next touches it. A refresh is +an ordinary PR with a visible diff — which is the point: the diff is the +review. + +**The generator must reject a table it cannot faithfully encode.** Keys +are ASCII today but nothing upstream promises that; a key containing a +character the emitted Lua would have to escape, or a duplicate after +normalization, aborts the regeneration rather than silently emitting a +table that disagrees with its source. Same discipline as Q#LN20's +refusal to hand back a lossy path. + +### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it + +`classify_key` (`src/optimistic.rs:144`) returns `Insert(c)` for `\` and +for every ASCII letter — only the nine built-in pair chars are excluded +(Q#AP1). So on a CRDT frontend the user's `\alpha` arrives as six +**source-peer** optimistic inserts, while the expansion is a single +**daemon-peer** `buf:replace` spanning all six. Undo across that boundary +is not chronologically arbitrated; this is the same defect Q#LN6 already +accepts for `⟨⟩`, `⦃⦄`, `⟮⟯`, one order of magnitude wider. + +Considered and rejected: `pmacs.buffer.set_round_trip_input(buf, true)`, +which exists, is per-buffer, and would fix this exactly. Its six current +callers are all read-only generated buffers — listview, compile, dired, +terminal — and it does considerably more than disable optimistic insert: +per `src/editor_core.rs:505`, `dispatch_idle` reports false, so RET +reaches buffer-local bindings instead of inserting a newline. Turning it +on for every ordinary editable Lean source file would trade a known undo +degradation for an unknown behavior change across the whole editing +surface, and would make Lean the one language whose typing has a +different latency profile. + +Also rejected: adding `\` to the always-round-trip set. It is +frontend-side and language-blind, so this would tax LaTeX, C, shell, and +every string literal in the editor to fix one language. + +Decision: **accept the degradation, name it in the module comment, and +do not paper over it.** The general fix is chronological cross-peer undo +arbitration — already on the standing backlog, and the same fix Q#LN6 +points at. What Stage 4b owes is honesty about scope: this is not "a few +brackets," it is every abbreviation the user types on a CRDT frontend. + +### Q#LN22 — Stage 4b mechanism: lazy abandonment, explicit ordering + +**Ordering.** The abbreviation consumer registers ahead of auto-pairing. +The collision is real: 64 keys contain a `lean4` pair-set character — +`\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`, `\{}` → `{$CURSOR}`. +With pairing first, typing `\[` inserts `[]` with the point between, so +the pending key is corrupted to `\[]` before the second `[` is typed and +`\[[]]` becomes unreachable. + +(Rev 1 justified this with `\<>`, which was wrong: `<` is not in the pair +set per Q#LN6, so that key is safe under either order.) + +**The contract the collision exposes:** the consumer must claim a +self-insert that **extends an open pending abbreviation**, not only one +that completes an expansion. A consumer that claims only completed +expansions hands every intermediate keystroke to auto-pairing, which is +exactly how `\[` gets corrupted. "Claimed" means the chain stops, not +that an edit was made. + +**State machine**, per §2.11's ground truth rather than rev 5's +reconstruction of it: + +- `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, + start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`. +- A subsequent self-insert `c` is claimed iff at least one key has + `text .. c` as a prefix; then `text = text .. c`. If it is also + uniquely-and-completely matching (one of the 1,550), expand now. +- If no key extends `text .. c`, expand `text` **first**, then let `c` + land normally — the chain does *not* claim `c`. +- Expansion resolves through §2.11's three-rule `getReplacementText`, + including the suffix rule (`\alp7` → `α7`). +- `$CURSOR` is stripped from the symbol and its index becomes the point. + +**Abandonment is lazy, because there is no cursor-motion hook** (round-5 +finding 3). Pending state is validated at the next typed edit and +discarded when any of these no longer holds: the record's buffer is the +pending buffer; `rec.effective_start` equals `start_offset + 1 + +#text` (the point is still at the end of the pending span); and the +buffer's `revision()` advanced by exactly the pending edit. `buffer. +after-switch` clears it eagerly since that hook *does* exist. The +practical difference from upstream: a user who clicks away mid-`\alp` +and types elsewhere gets the pending state dropped rather than expanded. +Upstream expands it. **This is a deliberate divergence** — expanding +into a region the user has left is the worse failure, and pmacs cannot +detect the departure at the moment it happens. + +**One `buf:replace`** for the whole expansion — one undo step, one CRDT +op, one effective-edit verification, with the same +rejected/altered-by-intercept reporting as `comment.lua`'s Q#CT5 and +`pair.lua`. A rejection drops the pending state; it does not retry. + +**Gate:** `pmacs.config.define{ name = "lean.abbrev", type = "boolean", +default = true, mutability = "live" }`, read against the **source** +buffer of the typed edit — the `editing.auto-pair` precedent +(`pair.lua:46`), including its round-2 correction to resolve +`rec.buffer` rather than `pmacs.window.buffer()`. + +**Language gate:** the consumer opens no pending abbreviation outside a +`lean4` buffer, resolved from `rec.buffer` for the same reason. `\` in a +Rust buffer is an ordinary character and `\[` there still pairs. ### Q#LN12 — Stage 5 sends `$/lean/plainGoal` through a typed Rust request @@ -1418,13 +1739,14 @@ never lands. | 2 | multi-root server affinity | **`ensure_server`, shared by every language** | — | | 3a | notification/response seams + purge; `pmacs.fs.canonicalize` | **the shared event drain, run by every language** | — | | 3b | `lake serve` + probe/latch, Lake root, `waitForDiagnostics` | none — Lean-only files plus one config entry | 1, 2, 3a | -| 4 | Unicode input method | **refactors `pair.lua`'s provenance read** | 1 | +| 4a | typed-edit consumer chain | **refactors `pair.lua`'s provenance read, shared by every language** | — | +| 4b | Unicode input method | none — Lean-only files plus one chain consumer | 1, 4a | | 5 | goal panel | new typed LSP request; panel adopter | 3a, 3b | | 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3b, 5 | | 7 | module hierarchy | listview adopter + one typed Rust request | 3a, 3b | -Four of the eight carry risk that is *not* about Lean — stages 1, 2, 3a, -and 6 each change something every language touches. That is the +Five of the nine carry risk that is *not* about Lean — stages 1, 2, 3a, +4a, and 6 each change something every language touches. That is the organizing principle of the split: **no PR in this arc mixes a cross-cutting substrate change with Lean feature content.** A reviewer looking at Stage 2 sees only `ensure_server`; a reviewer looking at Stage @@ -1436,6 +1758,16 @@ Lean-only. One generalization shipped as Stage 2; extracting the other as 3a is what makes the claim true again. The rule is only worth writing down if it survives contact with a stage that is inconvenient to split. +Round 5 found the *same* rule broken again, by Stage 4, whose risk column +read "refactors `pair.lua`'s provenance read" — every language's +auto-pairing — for a stage described as the Lean input method. Rev 5 had +noticed the shape and answered it with a commit boundary; a commit +boundary is not a review boundary. Twice in two re-scouts is the +interesting part: **this rule is not self-enforcing, and a stage only +looks Lean-only until someone re-reads its own risk column.** Every +remaining stage should be re-checked against it at scout time, not +assumed. + Ordering notes: - **Stage 2 has no Lean in it and could ship independently of this arc.** @@ -1453,11 +1785,21 @@ Ordering notes: `builtin/runtime/lsp.lua`. Unlike stages 1 and 2, this pair is strictly sequential — recorded here, per the #126/#127 lesson, rather than discovered in a rebase. -- **Stage 4 does not depend on stages 2, 3a, or 3b** and could run in - parallel, but should not: both touch `lsp.lua`/`pair.lua`-adjacent - runtime files, and the #126/#127 lesson is that parallel-safety - requires the file split be agreed *before* either lane starts. - Sequential is cheaper. +- **Stage 4a depends on nothing in this arc** — not even Stage 1. It is + a pure runtime-substrate change whose only content is `pair.lua` and a + new module beside it, and it would be worth landing if the Lean arc + were abandoned tomorrow, because "the typed-edit record has exactly + one consumer forever" is not a property anyone chose. +- **4a and 4b cannot run as sibling worktrees**, for the 3a/3b reason: + 4b's consumer is written against the registration API 4a adds. Strictly + sequential, recorded before either starts. +- **Stage 4b depends on stages 1 and 4a and on nothing else** — not on + 2, 3a, or 3b. The input method is useful with no language server at + all, which is the honest ordering argument for putting it this early: + a user with no Lean toolchain installed still gets a Lean editor that + can type Lean. It could run in parallel with the 5/6/7 lane, but + should not, per the #126/#127 lesson that parallel-safety requires the + file split be agreed *before* either lane starts. - **Stage 6 depends on Stage 5** only for the read-only generated-buffer and panel machinery, which Stage 5 establishes. If Stage 5 slips, Stage 6 can carry that machinery itself at the cost of duplicating it. @@ -1496,7 +1838,22 @@ Stated so they can be scored, per house style. inside `buffer.after-edit` re-enters the hook in a way pairing does not already survive. Confidence: medium — pairing does the same thing, but over a single codepoint rather than a multi-byte span. -6. **These eight stages reach rough VS Code parity for everything except +5a. **Lazy abandonment is good enough without a cursor-motion hook** + (rev 6, Q#LN22). Falsified if a user in normal editing hits a case + where stale pending state produces a *wrong* expansion rather than a + dropped one — the failure mode this design chooses. Confidence: + medium-high, because every path that can invalidate the state either + goes through `buffer.after-edit` (where it is checked) or through + `buffer.after-switch` (where it is cleared), and the residual is a + cursor move with no intervening edit, which the next typed edit + catches by position. If it fails, the fix is a cursor-motion hook — + substrate work with its own framing, not a patch to this stage. +5b. **Stage 4a is behavior-preserving.** Falsified by any change to + `tests/auto_pair_acceptance.rs` being needed to make it pass. + Confidence: high, and cheap to score — it is a diff-level check, not + a judgment call. This bet is stated separately from bet 5 because it + is the one a reviewer can falsify in ten seconds. +6. **These nine stages reach rough VS Code parity for everything except the interactive infoview.** Scored honestly rather than aspirationally. What lands: highlighting, goal view, Unicode input, diagnostics, hover, completion, goto-definition, symbols, semantic tokens, `#eval` @@ -1528,10 +1885,26 @@ What remains deferred: - **GPU goal band** — blocked on bottom-panel Stage 2 (Q#LN14). The panel is grid-only until then. - **A `cursor.after-move` hook** — there is none (Q#LN13), so Stage 5 - polls off `process.after-tick`. A real motion hook would serve the goal - view, `completion.lua`'s cursor-delta heuristic, and the outline/hover - panels alike; it is substrate work that should not be invented inside a - language lane. + polls off `process.after-tick` and Stage 4b abandons pending + abbreviations lazily rather than on departure (Q#LN22, round-5 finding + 3). A real motion hook would serve the goal view, the input method, + `completion.lua`'s cursor-delta heuristic, and the outline/hover panels + alike; it is substrate work that should not be invented inside a + language lane. Two consumers in this arc now want it, which is worth + recording as evidence for whoever frames it. +- **Chronological cross-peer undo arbitration** — the general fix for + Q#LN6's bracket pairs and Q#LN21's abbreviation expansions alike. + Already on the standing backlog; named again here because Stage 4b + widens the exposure from three pair characters to every abbreviation a + user types on a CRDT frontend, which changes how often the existing + defect is met without changing what it is. +- **Per-buffer optimistic-apply policy** — the narrower thing Q#LN21 + actually wanted and did not build. `set_round_trip_input` is the only + existing lever and it is too blunt (it also changes RET dispatch); a + frontend-side, language-aware round-trip character set would fix the + undo degradation for Lean without taxing every other language, and + would retire Q#AP1's limitation too. Frontend + protocol work, so + Q#LN14's no-protocol-change rule keeps it out of this arc entirely. - **LSP server reaping / LRU** — Q#LN15's per-root affinity makes unbounded `lake serve` growth possible. No editor caps this by default and pmacs will not either in this arc, but the policy question is now @@ -1758,12 +2131,44 @@ revision take letter suffixes rather than displacing anything. Round 3's finding 4 was stale cross-references surviving a renumber; not renumbering is the cheaper way to not repeat it. -**Stage 4 — the Unicode input method** +**Stage 4a — the typed-edit consumer chain** -38. `\alpha` + space yields `α`; the whole expansion is a single undo step. +Criterion 46 keeps its number and moves here — it was always the +substrate pin, filed under Stage 4 only because Stage 4 was one stage. +Per the no-renumbering rule above, round 5's additions take letter +suffixes on both sides of the split. + +46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs` + suite passes **unmodified**. A suite edited to accommodate the + refactor proves nothing; the diff for 4a must show zero lines + changed in that file. +46a. The chain reads the record exactly once: with two consumers + registered, a `take_typed_edit()` from inside either observes nil, + and both consumers receive the *same* record fields. Bites against a + chain that re-takes per consumer (which would hand the second one + nil in production and pass a single-consumer test). +46b. Ordering is by declared priority, not registration order: two + consumers registered low-priority-last still run + low-priority-first. Bites against a chain that "works" only because + `include_str!` order happens to agree with intent. +46c. A claiming consumer stops the chain — a later consumer does not + run — and a non-claiming one does not. +46d. A consumer that throws is contained: the fan-out still succeeds, + the other consumers still run, and the failure reports through + `set_status`. Bites against the `all-must-succeed` contract taking + the whole fan-out down with one bad consumer (Q#LN10). +46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server + test — pairing's closer must be in the buffer before `lsp.lua` + flushes `didChange` — still holds with pairing behind the chain. + Falsified by moving the chain's registration after `lsp.lua`'s. + +**Stage 4b — the Unicode input method** + +38. `\alpha` + space yields `α`; the whole expansion is a single undo + step, and one undo restores `\alpha` rather than `\alph`. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. -40. **Pair-collision pin (Q#LN10).** `\[[]]` yields `⟦⟧`: each `[` is +40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is claimed as an extension of the pending abbreviation, so auto-pairing never inserts a closing `]` into the pending key. Bites against an ordering where pairing runs first, and against a consumer that claims @@ -1773,15 +2178,55 @@ renumbering is the cheaper way to not repeat it. 41. `\to` yields `→` eagerly on uniqueness, with no terminator typed. 42. A prefix with no match (`\zzzz` + space) is left as literal text; no edit is made. -43. Moving the cursor out of a pending abbreviation abandons it. +43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion + hook, this asserts what pmacs can actually detect: after `\alp`, an + explicit `goto_byte` elsewhere followed by typing `h` inserts a + plain `h` and leaves the `\alp` text untouched — the pending state + is dropped, not expanded. Plus: `buffer.after-switch` clears pending + state eagerly. **Rev 5's version of this criterion was not + buildable**; recorded so the change is visible rather than silent. 44. `pmacs.config.set("lean.abbrev", false)` disables expansion; the setting is read against the typed edit's **source** buffer. 45. Expansion does not fire in a non-`lean4` buffer — including that a pending abbreviation is never opened there, so `\[` in a Rust buffer still pairs normally. -46. **Provenance-refactor pin:** the full auto-pairing acceptance suite - passes unchanged, and a bite against the pre-refactor `pair.lua` - confirms the shared-consumer commit is behavior-preserving. +45a. **Shortest-key resolution (§2.11).** `\alp` + space yields `α`, and + `\al` + space yields `∀` — from `all`, not `alpha`. The second is + the one that bites: a "longest match" or "unique match only" + implementation passes the first and fails this. +45b. **Suffix rule.** `\alp7` + space yields `α7`. Bites against an + implementation that drops unmatchable trailing characters or + abandons the whole abbreviation. +45c. **There is no terminator list.** `\+` followed by space extends + rather than terminating, because `'+ '` is a key. Bites against any + implementation with a hardcoded space/tab/RET terminator set — which + is what rev 5 specified. +45d. **`\\` yields a single `\`**, by extension-and-eager-match rather + than by treating the second `\` as a terminator. And after a + *non-empty* pending key, a second `\` does terminate and open a new + abbreviation: `\alpha\to` + space yields `α→`. +45e. **No re-arm through inserted text (§2.11).** `\setminus` + space + yields a literal `\`, and typing an ordinary letter after it inserts + that letter — the inserted backslash opens no pending abbreviation, + because the expansion is a programmatic replace that arms no record. + Bites against a future consumer that infers pending state from + buffer text instead of provenance. +45f. **Both producers, and the CI-darkness stated.** The dispatch path + is pinned by the criteria above. The optimistic CRDT producer + (round-5 finding 4) is pinned by a separate criterion driving + `handle_remote_crdt_op`, which is `#[cfg(feature = "crdt")]` and + therefore **dark in CI and dark in the required gate list**, since + that list runs `--features crdt` only for `--lib`. The PR must + either land that coverage as a `--lib` test where the gate reaches + it, or state in its description that the optimistic path was + verified only locally and name the command. Silence here is the + failure mode — a green CI would otherwise read as covering the path + most users take. +45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips: + its entry count matches the header's declared count, and a spot set + of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches + `abbreviations.json` byte-for-byte. Bites against a generator that + silently drops or mangles keys (Q#LN11). **Stage 5 — the goal view** @@ -1847,7 +2292,7 @@ renumbering is the cheaper way to not repeat it. it, with the extra success-gate §2.9 forces. - **#110 (auto-pairing)** — `take_typed_edit()` provenance, the fail-closed discipline on transformed source edits, and Q#AP1's optimistic-classifier - limitation. Stage 4 is built on all three. + limitation. Stage 4a generalizes the first; 4b is built on all three. - **#127 (config registry)** — `pmacs.config.define` and the source-buffer-resolution correction. Q#LN10's gate follows `editing.auto-pair` exactly. @@ -1895,8 +2340,8 @@ alongside sixteen other languages — deliberately *not* the typed registry, because moving one language's entry there while the other sixteen stay put would fragment the surface rather than unify it. Migrating `pmacs.lsp.config` wholesale is a config-arc concern; this lane must not -create a precedent that makes it harder. Stage 4's `lean.abbrev` gate is -where this arc does enter the registry, and Q#LN10 already commits to the +create a precedent that makes it harder. Stage 4b's `lean.abbrev` gate is +where this arc does enter the registry, and Q#LN22 already commits to the `editing.auto-pair` shape. **Background-work attribution (§9).** Three pieces of background work, @@ -1928,3 +2373,59 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from #161 — surfacing the spawn failure itself. Each is a behavior change for languages other than Lean, and §4's rule is what keeps them out of a Lean PR. + +### 9.1 Coherence impact — stages 4a and 4b (rev 6) + +**Sections served.** §6 (interaction islands) primarily, and in the +*preventing* direction rather than the fixing one — see below. §11 +(config registry) secondarily, by adding one option in the established +shape rather than a new switch mechanism. + +**Golden journey (§2).** No step is touched by 4a. 4b improves step 4 +(editing) for Lean specifically and changes nothing for any other +language: the pending-abbreviation state exists only in `lean4` buffers. +Neither stage changes launch, open, or attach. + +**Interaction islands (§6).** **None added, and this is the load-bearing +claim of Stage 4b.** An input method is the archetypal island: a modal +state where ordinary keys mean something else, usually with its own +keymap, its own escape, and its own set of commands that only work +inside it. Stage 4b deliberately has none of those. There is no keymap, +no dispatch shadow, no mode line indicator, no command that only works +mid-abbreviation, and no key that exits. The pending state is invisible +to every other subsystem, is abandoned by ordinary editing, and its +worst failure is that the user's literal text stays literal. The +`lean.abbrev` switch is an ordinary registry boolean, not an island +toggle. + +Stage 4a's chain is the mechanism that makes that possible, and it also +retires a smaller island risk: today the only way for a second feature to +react to a typed character is to compete with `pair.lua` for a one-shot +record, and the natural workaround — inferring from buffer text — is how +input methods grow their own private state and, eventually, their own +modal surface. + +**Config registry (§11).** One option, `lean.abbrev`, in exactly the +`editing.auto-pair` shape (boolean, `mutability = "live"`, resolved +against the typed edit's source buffer). This is the arc entering the +registry as §9's earlier text predicted, and it is a genuine adoption +rather than a new surface. Stage 4a adds none. + +**Background-work attribution (§9).** Neither stage does background work. +Both are synchronous inside an existing hook fan-out; no process is +spawned, no timer armed, no request issued. There is nothing to attribute +and nothing to worsen — recorded explicitly because "none" is an answer +this section should be able to give without ambiguity. + +**Debt this revision retires.** The unowned assumption that +`take_typed_edit()` has exactly one consumer forever. That was never a +decision — it was the shape of the only caller — and every future +typed-character feature would have had to rediscover it. Stage 4a turns +an accident into an API with a stated ordering contract. + +**Debt this revision names rather than pays.** One, and it is real: +Q#LN21's cross-peer undo degradation, now covering every abbreviation +rather than three bracket pairs. The fix is chronological cross-peer undo +arbitration, already on the standing backlog and already blocking Q#LN6. +Stage 4b makes the existing gap more visible without widening the class +of defect — but "more visible" is the honest word, not "unchanged." From ccdf352258ad959cf88a1bba0fc2fbd5816a74d6 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:38:21 -0400 Subject: [PATCH 07/14] fix(panel): close Stage 2A review round 2 (2 P1, 1 P2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **P1-1 — the `Invalidated` arm published the panel context on the document wire.** Real bug, and the live half of the routing defect: the semantic peer has ONE statusline slot, so emitting an authoritative-empty payload for every context replaced the document's with the panel's. Now filtered by document-window identity exactly like the `Ready` arm; a panel's own clear belongs to `PanelFrame` in 2B. Pinned by `invalidated_statusline_clears_only_the_document_not_the_panel`, which reproduces the reported shape — two targets instead of one — when the filter is removed. Honest note on the `Ready` arm: its identity selector is **defensive**, not independently falsifiable today, because the document context is captured first so "first context for my frontend" happens to pick it. Rather than leave that as a silent dependency, `the_semantic_fan_out_captures_the_document_first` pins the order and says why it matters. **P1-2 — round-1 finding 3 was not closed; four of my pins were vacuous.** All four confirmed and fixed: - The statusline consumer test discarded `render_frame`'s output. It now observes the WIRE payload from a v18 peer with a registered provider, and asserts non-emptiness so it cannot pass by emitting nothing. - The terminal test compared two NON-terminal buffers, so both routings answered `false`. The document window now holds a REAL terminal, so the routes disagree; reverting `semantic_terminal_key` fails it. - The decorations test used different buffers and an empty selection — again the same answer either way. The panel now displays the declared buffer with a non-empty selection while the document has none. - #1/#3/#21 had no discriminating pin at all. Their only production caller is `dispatcher_loop`, which no test can drive, so this extracts three named seams the loop calls — `document_buffer_to_follow`, `document_cursor_byte`, `peer_displays_buffer_as_document` — and pins each. Also newly pinned: #2 the lazy CRDT upgrade (the census's sharpest case), #7 `Viewport` aligning WITHOUT taking focus, and #9 a focused terminal panel not suppressing the document viewport. **Every one of the nine pins was falsified by revert.** Two needed a second attempt after the first bite came back green. **P2-3 — stale docs.** `StatuslineEvaluationTarget::Semantic`'s documentation described evaluating only the focused window; it now describes the document-plus-side fan-out, the capture order, the identity-selection requirement, and that `active` reports actual focus. The ledger's Stage 2A entry is corrected to five commits, 2,014 CRDT tests, and 16 acceptance tests. Two clippy findings the refactor introduced were fixed: `document_buffer_to_follow` is `crdt`-gated to match its only caller, and the `CursorByte` guard collapses into one `if`. Gates: fmt clean; workspace clippy clean; 1,832 default + 2,014 CRDT library; Stage 2A 16; Stage 1 46; statusline 8; m11_5 2; GPU initial target 14; terminal config 12; folding Stage 2 48; vterm 1/2 10 / 6; M4 121; required GPU 202; `git diff --check` clean. Co-Authored-By: Claude Opus 5 (1M context) --- docs/active-work.md | 43 +-- src/daemon.rs | 343 ++++++++++++++++++++--- src/semantic_render.rs | 26 +- src/statusline.rs | 21 +- tests/bottom_panel_stage2a_acceptance.rs | 259 +++++++++++++++-- 5 files changed, 602 insertions(+), 90 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 98727e5..36a99de 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -492,27 +492,36 @@ implemented and in review.** worktree `../pmacs-bp-stage2a`, **canonical `main` @ `cf54270` integrated** (review round 1, finding 4 — the terminal-config lane #173 also changes `src/editor.rs`, so gates were rerun on the merge - result, not the old combination). Two commits: the classified census routing, then the - painter extraction + acceptance. **No protocol change; no behavior + result, not the old combination). Five commits: the classified census + routing, the painter extraction + acceptance, the lane record, then + the round-1 and round-2 review fixes. **No protocol change; no behavior change for any frontend today** — with `panel_capable = false` for semantic sessions, `primary_document_window` returns `view.active` in every existing configuration, so this is seam adoption that becomes load-bearing in 2B. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; **1,832 default + 2,009 CRDT** library tests; - new `bottom_panel_stage2a_acceptance` 10/10; bottom-panel Stage 1 - 46; statusline segments 7 default / 8 CRDT; m11_5 semantic 2 CRDT; - GPU initial target 14 CRDT; vterm Stage 1/2 10 / 6; folding Stage 2 - 48; M4 121; required GPU 202; `git diff --check` clean. -- **Both key routings were falsified by revert.** Rerouting - `dispatch_idle_for` (#14, Focus) through `primary_document_window` - fails `focus_class_dispatch_idle_still_tracks_the_focused_window`; - reverting the statusline lookup (#12, Projection) to `view.active` - fails the document-context test. Worth recording: the *structural* - test `focus_and_projection_disagree_in_the_same_state` did **not** - catch the first bite — it compares the two authorities directly, so - only a consumer-level assertion catches a misrouted consumer. Keep - both kinds. +- Verification on the merge result: `cargo fmt --check` clean; strict + workspace Clippy clean; **1,832 default + 2,014 CRDT** library tests; + `bottom_panel_stage2a_acceptance` **16**; bottom-panel Stage 1 46; + statusline segments 8 CRDT; m11_5 semantic 2 CRDT; GPU initial target + 14 CRDT; terminal config 12 CRDT; vterm Stage 1/2 10 / 6; folding + Stage 2 48; M4 121; required GPU 202; `git diff --check` clean. +- **Every routed producer is now pinned at a seam its production caller + uses, and each pin was falsified by revert**: #1 follow, #2 lazy CRDT + upgrade, #3 `CursorByte`, #5 decorations, #7 `Viewport` (aligns + without focusing), #8 `Pointer` (aligns and focuses), #9 the + terminal-context gate, #12 statusline, #21 the publication filter, + plus the focus-class negatives. #1/#3/#21 required extracting three + named helpers, because their only production caller is + `dispatcher_loop`, which no test can drive. +- **Three lessons about the TESTS, not the code, all from review:** + (a) a *structural* test comparing the two authorities directly does + **not** catch a misrouted consumer — only consumer-level assertions + do; (b) a daemon-path test must `register_session` or the event is + dropped at the uninstalled-session check before reaching the code + under test; (c) a discriminating fixture must make the two routings + DISAGREE — comparing two non-terminal buffers, or two windows with no + selection, yields the same answer either way and proves nothing. + Round 2 found four of my own pins vacuous by exactly these shapes. - **Review round 1 closed: 4 P1 + 2 P2, all real.** The P1s were a stale-`Pointer` focus steal (the failed-alignment arm returned the window, so #8's activation focused it before `dispatch_pointer` diff --git a/src/daemon.rs b/src/daemon.rs index 606839d..63f6b87 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -1145,14 +1145,7 @@ fn dispatcher_loop( .session_state(*fid) .is_some_and(|s| s.negotiated_capabilities.semantic_render) { - // Bottom-panel §1.3 #1 — Projection. The buffer this - // frontend DISPLAYS AS ITS DOCUMENT, not the one it - // happens to focus: focusing a panel must re-send no - // snapshot and must never swap the replica's mirror. - let active_now = { - let core = editor.core.borrow(); - core.primary_document_buffer(*fid) - }; + let active_now = document_buffer_to_follow(editor, *fid); if let Some(active_now) = active_now && last_active_buffer_sent.get(fid) != Some(&active_now) { @@ -1433,25 +1426,15 @@ fn dispatcher_loop( && session_registry .session_state(*fid) .is_some_and(|s| s.negotiated_capabilities.crdt_replica) + && let Some((buffer_id, byte_pos)) = document_cursor_byte(editor, *fid) { - // Bottom-panel §1.3 #3 — Projection. `CursorByte` is - // the replica's authoritative DOCUMENT cursor; a - // focused panel must not retarget it at the panel - // buffer (Q#BP14's "active buffer is a - // document-surface term, not an input-focus term"). - let core = editor.core.borrow(); - if let Some(window) = core - .primary_document_window(*fid) - .and_then(|win_id| core.windows.get(&win_id)) - { - let cursor_byte_msg = InstanceMessage::CursorByte { - buffer_id: window.buffer_id, - byte_pos: window.cursor, - }; - if let Err(e) = write_message(stream, &cursor_byte_msg) { - eprintln!("pmacs: write CursorByte for {fid:?} failed: {e}"); - write_failed = true; - } + let cursor_byte_msg = InstanceMessage::CursorByte { + buffer_id, + byte_pos, + }; + if let Err(e) = write_message(stream, &cursor_byte_msg) { + eprintln!("pmacs: write CursorByte for {fid:?} failed: {e}"); + write_failed = true; } } } @@ -2524,13 +2507,7 @@ fn publish_buffer_snapshot_to_replicas( continue; } if session.negotiated_capabilities.semantic_render { - // Bottom-panel §1.3 #21 — Projection. "Displays this - // buffer" means the peer's DOCUMENT surface: testing the - // focused window would both miss a buffer visible in the - // document (panel focused elsewhere) and replace the peer's - // mirror for one visible only in a panel. - let displays_buffer = - editor.core.borrow().primary_document_buffer(*peer_id) == Some(buffer_id); + let displays_buffer = peer_displays_buffer_as_document(editor, *peer_id, buffer_id); if !displays_buffer { continue; } @@ -2969,6 +2946,53 @@ fn handle_remote_crdt_op( /// whole switch. This is the input/display alignment fix for B1: the /// frontend's *declared* buffer becomes the buffer its keys edit and /// its `CursorByte` reports. +/// The buffer a semantic frontend DISPLAYS AS ITS DOCUMENT — the +/// buffer-follow / `BufferSnapshot` re-send target (bottom-panel §1.3 +/// #1, Projection). +/// +/// Not the focused buffer: focusing a panel must re-send no snapshot and +/// must never swap the replica's document mirror. Named as its own +/// function so the rule is pinnable — its only caller is +/// `dispatcher_loop`, which no test can drive. +#[cfg(feature = "crdt")] +fn document_buffer_to_follow( + editor: &EditorState, + fid: FrontendId, +) -> Option { + editor.core.borrow().primary_document_buffer(fid) +} + +/// The `(buffer, byte)` a semantic replica's authoritative `CursorByte` +/// describes (bottom-panel §1.3 #3, Projection). +/// +/// Q#BP14's vocabulary split: "active buffer" in the replica is a +/// DOCUMENT-SURFACE term, not an input-focus term, so a focused panel +/// must not retarget the document caret at the panel's buffer. +fn document_cursor_byte( + editor: &EditorState, + fid: FrontendId, +) -> Option<(crate::buffer::BufferId, u64)> { + let core = editor.core.borrow(); + let win_id = core.primary_document_window(fid)?; + let window = core.windows.get(&win_id)?; + Some((window.buffer_id, window.cursor)) +} + +/// Whether `peer_id` displays `buffer_id` on its DOCUMENT surface — the +/// `BufferSnapshot` publication recipient filter (bottom-panel §1.3 #21, +/// Projection). +/// +/// Testing the focused window instead would both miss a buffer visible +/// in the document while a panel holds focus, and replace the peer's +/// document mirror for a buffer visible only in a panel. +fn peer_displays_buffer_as_document( + editor: &EditorState, + peer_id: FrontendId, + buffer_id: crate::buffer::BufferId, +) -> bool { + editor.core.borrow().primary_document_buffer(peer_id) == Some(buffer_id) +} + /// Align a semantic frontend's **primary document window** to the /// buffer it declared (bottom-panel §1.3 #7, Q#BP14). /// @@ -4770,4 +4794,257 @@ mod tests { "non-vacuity: the document window is a real, distinct focus target" ); } + + /// Bottom-panel §1.3 #1/#3/#21 — the three Projection producers whose + /// only production caller is `dispatcher_loop`, pinned at the named + /// seams that loop calls. Round 2 finding: reverting any of them to + /// `active_window_for` previously left every test green. + #[cfg(feature = "crdt")] + #[test] + fn tick_producers_describe_the_document_while_a_panel_is_focused() { + let (editor, fid, document, panel) = panel_focused_semantic_fixture(); + let (doc_buf, panel_buf, doc_cursor) = { + let core = editor.core.borrow(); + ( + core.windows[&document].buffer_id, + core.windows[&panel].buffer_id, + core.windows[&document].cursor, + ) + }; + assert_ne!(doc_buf, panel_buf, "fixture: distinct buffers"); + + // #1 buffer-follow / BufferSnapshot re-send target. + assert_eq!( + document_buffer_to_follow(&editor, fid), + Some(doc_buf), + "#1: the follow target must be the DOCUMENT buffer, not the focused panel's" + ); + + // #3 CursorByte. + assert_eq!( + document_cursor_byte(&editor, fid), + Some((doc_buf, doc_cursor)), + "#3: CursorByte must describe the DOCUMENT surface" + ); + + // #21 publication recipient filter, both directions. + assert!( + peer_displays_buffer_as_document(&editor, fid, doc_buf), + "#21: a buffer visible in the document must still receive publications while a panel holds focus" + ); + assert!( + !peer_displays_buffer_as_document(&editor, fid, panel_buf), + "#21: a buffer visible only in a panel must NOT replace the document mirror" + ); + } + + /// Bottom-panel §1.3 #2 — the sharpest census case: the lazy CRDT + /// upgrade BROADCASTS a snapshot, so keying it on focus would let + /// focusing a fresh generated panel buffer swap every peer's mirror. + #[cfg(feature = "crdt")] + #[test] + fn lazy_crdt_upgrade_never_targets_a_focused_panel_buffer() { + let (editor, fid, document, panel) = panel_focused_semantic_fixture(); + let (doc_buf, panel_buf) = { + let core = editor.core.borrow(); + ( + core.windows[&document].buffer_id, + core.windows[&panel].buffer_id, + ) + }; + + let upgraded = ensure_active_buffer_crdt_backed(&editor, fid); + assert_eq!( + upgraded, + Some(doc_buf), + "#2: the upgrade must target the DOCUMENT buffer" + ); + assert_ne!( + upgraded, + Some(panel_buf), + "#2: focusing a panel must never trigger its buffer's upgrade+broadcast" + ); + } + + /// Bottom-panel §1.3 #7 vs #8 — `Viewport` aligns WITHOUT moving + /// focus; only `Pointer` activates. Driven through the real + /// dispatcher seam. + #[cfg(feature = "crdt")] + #[test] + fn viewport_aligns_the_document_without_taking_focus_from_the_panel() { + let (mut editor, fid, document, panel) = panel_focused_semantic_fixture(); + let other = { + let mut core = editor.core.borrow_mut(); + core.registry.borrow_mut().create("*other*") + }; + + dispatch_one_semantic_event( + &mut editor, + fid, + FrontendEvent::Viewport { + frontend_id: fid, + buffer_id: other, + visible: pmacs_protocol::ByteRange { start: 0, end: 0 }, + generation: 0, + }, + ); + + assert_eq!( + editor.core.borrow().views[&fid].active, + panel, + "#7: a document Viewport must NOT move focus out of the panel" + ); + assert_eq!( + editor.core.borrow().windows[&document].buffer_id, + other, + "#7: it must still have ALIGNED the document window to the declared buffer" + ); + } + + /// Shared fixture: a semantic frontend with a document window and a + /// FOCUSED bottom panel. `panel_capable` is set explicitly because + /// Stage 1 ships `false` for semantic sessions and 2B flips it for a + /// v21-negotiated peer. + #[cfg(feature = "crdt")] + fn panel_focused_semantic_fixture() -> ( + crate::editor::EditorState, + FrontendId, + crate::window::WindowId, + crate::window::WindowId, + ) { + use crate::window::{FrontendView, Layout, LayoutNode, Orientation, Window, WindowParams}; + + let editor = crate::editor::EditorState::new(); + let fid = FrontendId(91); + let (document, panel) = { + let mut core = editor.core.borrow_mut(); + let doc_buf = core.active_window().buffer_id; + let panel_buf = core.registry.borrow_mut().create("*panel*"); + let document = crate::window::WindowId::next(); + let panel = crate::window::WindowId::next(); + let (doc_view, panel_view) = { + let reg = core.registry.borrow(); + ( + crate::text_view::TextView::new(reg.get(doc_buf).expect("doc")), + crate::text_view::TextView::new(reg.get(panel_buf).expect("panel")), + ) + }; + core.windows + .insert(document, Window::new(document, doc_buf, doc_view)); + let mut panel_window = Window::new(panel, panel_buf, panel_view); + let mut params = WindowParams::default(); + params.side = Some(crate::window::Side::Bottom); + params.fixed_rows = Some(4); + panel_window.params = params; + core.windows.insert(panel, panel_window); + core.register_frontend_view( + fid, + FrontendView { + layout: Layout { + root: LayoutNode::Split { + orientation: Orientation::Horizontal, + children: vec![LayoutNode::Leaf(document), LayoutNode::Leaf(panel)], + weights: vec![1, 1], + }, + }, + active: panel, + fold_projection: false, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + (document, panel) + }; + editor.sync_frame_geometry(fid, CellSize::new(24, 80)); + (editor, fid, document, panel) + } + + /// Drive ONE authenticated semantic event through the real + /// dispatcher. The session must be registered or the event is + /// dropped at the uninstalled-session check before reaching any + /// handler. + #[cfg(feature = "crdt")] + fn dispatch_one_semantic_event( + editor: &mut crate::editor::EditorState, + fid: FrontendId, + event: FrontendEvent, + ) { + let mut render_states = HashMap::new(); + let mut semantic_states = HashMap::new(); + semantic_states.insert(fid, crate::semantic_render::SemanticRenderState::new(fid)); + let mut streams = HashMap::new(); + let mut term_sizes = HashMap::new(); + term_sizes.insert(fid, CellSize::new(24, 80)); + let mut last_idle = HashMap::new(); + let mut last_active = HashMap::new(); + let mut bells = HashMap::new(); + let mut registry = SessionRegistry::new(); + registry.register_session( + fid, + crate::presence::SessionState { + negotiated_protocol_version: pmacs_protocol::PROTOCOL_VERSION, + negotiated_capabilities: crate::protocol::NegotiatedCapabilities { + semantic_render: true, + crdt_replica: true, + ..Default::default() + }, + color_slot: 0, + }, + ); + handle_dispatcher_event( + DispatcherEvent::FrontendEvent { source: fid, event }, + editor, + &mut render_states, + &mut semantic_states, + &mut streams, + &mut term_sizes, + &mut last_idle, + &mut last_active, + &mut bells, + &mut registry, + ); + } + + /// Bottom-panel §1.3 #9 — Projection. The `Viewport` terminal-context + /// gate asks "is this frontend's DOCUMENT surface a terminal", so a + /// focused TERMINAL PANEL must not suppress the still-visible + /// document's viewport. + #[cfg(feature = "crdt")] + #[test] + fn a_focused_terminal_panel_does_not_suppress_the_document_viewport() { + use crate::terminal::TerminalSpec; + + let (mut editor, fid, document, panel) = panel_focused_semantic_fixture(); + let other = editor.core.borrow().registry.borrow_mut().create("*other*"); + + // A REAL terminal in the focused panel. + let mut spec = TerminalSpec::new("/bin/sh"); + spec.rows = 10; + spec.cols = 40; + let term_buf = editor.open_terminal(spec).expect("a real terminal"); + editor + .core + .borrow_mut() + .install_buffer_in_window(panel, term_buf) + .expect("terminal into the panel"); + editor.core.borrow_mut().focus_window(fid, panel); + + dispatch_one_semantic_event( + &mut editor, + fid, + FrontendEvent::Viewport { + frontend_id: fid, + buffer_id: other, + visible: pmacs_protocol::ByteRange { start: 0, end: 0 }, + generation: 0, + }, + ); + + assert_eq!( + editor.core.borrow().windows[&document].buffer_id, + other, + "#9: a focused TERMINAL panel must not suppress the document viewport — the document window should still have aligned to the declared buffer" + ); + } } diff --git a/src/semantic_render.rs b/src/semantic_render.rs index b63efcf..af08741 100644 --- a/src/semantic_render.rs +++ b/src/semantic_render.rs @@ -985,10 +985,18 @@ impl SemanticRenderState { StatuslineEvaluationOutcome::Invalidated { authoritative_empty, } => { - for context in authoritative_empty - .into_iter() - .filter(|context| context.frontend_id == frontend_id) - { + // Bottom-panel A2A-2: the clear must be filtered by + // DOCUMENT WINDOW exactly like the Ready arm. The + // semantic peer has ONE statusline slot, so publishing + // the panel context's clear here replaces the document's + // payload with the panel's — the same misrouting the + // Ready arm was fixed for, on the clear path. + // + // A panel's own clear belongs to the future panel + // painter (`PanelFrame`, Stage 2B), not to this wire. + for context in authoritative_empty.into_iter().filter(|context| { + context.frontend_id == frontend_id && Some(context.window_id) == document_window + }) { self.emit_statusline_payload(context.buffer_id, Vec::new(), Vec::new(), out); } } @@ -2949,11 +2957,15 @@ mod tests { "stale evaluation retains the prior baseline until snapshot reset" ); + // Bottom-panel A2A-2: the clear is filtered by DOCUMENT window + // identity, so the context under test must BE the document + // window — passing `None` here would assert nothing. + let document_window = crate::window::WindowId::next(); let invalidated = || StatuslineEvaluation { outcome: StatuslineEvaluationOutcome::Invalidated { authoritative_empty: vec![crate::statusline::StatuslineContext { frontend_id: FrontendId::LOCAL, - window_id: crate::window::WindowId::next(), + window_id: document_window, buffer_id, active: true, }], @@ -2961,13 +2973,13 @@ mod tests { new_failures: Vec::new(), }; let mut replacement = Vec::new(); - semantic.emit_statusline_segments(invalidated(), None, &mut replacement); + semantic.emit_statusline_segments(invalidated(), Some(document_window), &mut replacement); assert_eq!( statusline_of(&replacement), Some((buffer_id, Vec::new(), Vec::new())) ); let mut unchanged = Vec::new(); - semantic.emit_statusline_segments(invalidated(), None, &mut unchanged); + semantic.emit_statusline_segments(invalidated(), Some(document_window), &mut unchanged); assert!( unchanged.is_empty(), "the empty invalidation became baseline" diff --git a/src/statusline.rs b/src/statusline.rs index 7bf345f..3eb4ef6 100644 --- a/src/statusline.rs +++ b/src/statusline.rs @@ -215,10 +215,25 @@ pub enum StatuslineEvaluationTarget { /// Frontend whose entire visible layout is evaluated. frontend_id: FrontendId, }, - /// Only the frontend's active window, iff it still displays the declared - /// semantic viewport buffer. + /// The frontend's **primary document window**, iff it still displays + /// the declared semantic viewport buffer, **plus its visible side + /// window** when one exists (bottom-panel Q#BP8 / A2A-2). + /// + /// Two contexts, not one: the document result feeds the semantic + /// `StatuslineSegments` wire, while the side result paints in the + /// panel's own mode line. Unprojected document splits run no + /// callbacks, and a derived-hidden side (Q#BP2b) is omitted because + /// it has no mode line to paint this frame. + /// + /// The document context is captured **first**; consumers must still + /// select by window identity rather than position, since only one of + /// the two may reach the single semantic statusline slot. + /// + /// `active` on each context reports **actual focus**, so a document + /// provider truthfully observes `active = false` while a panel owns + /// focus (Q#BP14, parent acceptance 42). Semantic { - /// Frontend whose focused daemon window is evaluated. + /// Frontend whose document (and visible side) window is evaluated. frontend_id: FrontendId, /// Buffer declared by the semantic viewport. declared_buffer: BufferId, diff --git a/tests/bottom_panel_stage2a_acceptance.rs b/tests/bottom_panel_stage2a_acceptance.rs index 3b6c183..1063e9f 100644 --- a/tests/bottom_panel_stage2a_acceptance.rs +++ b/tests/bottom_panel_stage2a_acceptance.rs @@ -32,6 +32,14 @@ fn exec(s: &EditorState, src: &str) { s.lua_host.lua().load(src.to_string()).exec().unwrap(); } +fn side_window_of(core: &pmacs::editor_core::EditorCore, fid: FrontendId) -> Option { + core.views[&fid].layout.iter_ids().into_iter().find(|id| { + core.windows + .get(id) + .is_some_and(|w| w.params.side.is_some()) + }) +} + fn side_window(s: &EditorState) -> Option { let core = s.core.borrow(); core.views[&FrontendId::LOCAL] @@ -540,48 +548,239 @@ fn consumer_line_numbers_follow_the_document_not_the_focused_panel() { } #[test] -fn consumer_statusline_segments_name_the_document_window() { - use pmacs::protocol::ByteRange; +fn consumer_statusline_segments_carry_the_document_payload_not_the_panel() { + use pmacs::protocol::{ByteRange, InstanceMessage}; use pmacs::semantic_render::SemanticRenderState; - // §1.3 #12 at the producer: the wire segments must be selected by - // the DOCUMENT window even though the fan-out now also evaluates the - // visible side window (A2A-2). + // §1.3 #12 / A2A-2 at the WIRE. Round 2 finding: the previous + // version discarded `render_frame`'s output and only reasserted + // `primary_document_window`, so restoring the producer's + // "first context for my frontend" selector left it green. + // + // The peer must negotiate v18 or no `StatuslineSegments` is emitted + // at all and the assertion would be vacuous a second way. let s = editor(); - let (fid, doc_win, _panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + let (fid, _doc_win, _panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + let panel_buf = { + let core = s.core.borrow(); + let panel = side_window_of(&core, fid).expect("panel"); + core.windows[&panel].buffer_id + }; - let mut sem = SemanticRenderState::new(fid); + // One provider so a payload exists to misroute. + exec( + &s, + "pmacs.statusline.register({ name = \"probe\", side = \"left\", + face = \"ui.modeline\", fn = function(ctx) return \"X\" end })", + ); + + let mut sem = SemanticRenderState::for_peer(fid, 18); sem.set_viewport(doc_buf, ByteRange { start: 0, end: 0 }, 0); - // Not asserting on message presence (a peer that never negotiated - // v18 emits none); asserting the routing input the producer uses. - let _ = sem.render_frame(&s); + let msgs = sem.render_frame(&s); - assert_eq!( - s.core.borrow().primary_document_window(fid), - Some(doc_win), - "the producer's document-window selector must name the document" + let targets: Vec<_> = msgs + .iter() + .filter_map(|m| match m { + InstanceMessage::StatuslineSegments { buffer_id, .. } => Some(*buffer_id), + _ => None, + }) + .collect(); + + assert!( + !targets.is_empty(), + "non-vacuity: a v18 peer with a registered provider must emit StatuslineSegments" + ); + assert!( + targets.iter().all(|b| *b == doc_buf), + "every StatuslineSegments must target the DOCUMENT buffer; got {targets:?} (document {doc_buf:?}, panel {panel_buf:?})" + ); + assert!( + !targets.contains(&panel_buf), + "the panel's context must never reach the document statusline wire" ); } #[test] -fn consumer_terminal_declaration_cannot_be_claimed_by_a_focused_panel() { - // §1.3 #6/#10/#11 through the real guard: with the panel focused, - // a declaration naming the PANEL's buffer must be refused, because - // the full-window terminal surface is the document window. - let s = editor(); - let (fid, _doc_win, panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); - let panel_buf = s.core.borrow().windows[&panel_win].buffer_id; +fn consumer_terminal_declaration_resolves_the_document_not_the_focused_panel() { + use pmacs::terminal::TerminalSpec; + + // §1.3 #6/#10/#11 through the real guard. Round 2 finding: the + // previous version compared two NON-terminal buffers, so both the + // old and new routings returned `false` and it could not + // discriminate. Make the DOCUMENT window hold a real terminal: the + // document routing then answers `true` while the old `view.active` + // routing (which names the focused panel) answers `false`. + let mut s = editor(); + let (fid, doc_win, _panel_win, _doc_buf) = semantic_frontend_with_focused_panel(&s); + + let mut spec = TerminalSpec::new("/bin/sh"); + spec.rows = 10; + spec.cols = 40; + let term_buf = s.open_terminal(spec).expect("a real terminal session"); + + // Install the terminal in the DOCUMENT window; the panel keeps its + // own non-terminal buffer and keeps focus. + { + let mut core = s.core.borrow_mut(); + core.install_buffer_in_window(doc_win, term_buf) + .expect("install the terminal in the document window"); + } + let panel_buf = { + let core = s.core.borrow(); + let panel = side_window_of(&core, fid).expect("panel"); + core.windows[&panel].buffer_id + }; assert!( - !s.semantic_terminal_declaration_is_active(fid, panel_buf), - "a focused panel's buffer must not become the document terminal declaration" + s.semantic_terminal_declaration_is_active(fid, term_buf), + "the DOCUMENT window's terminal must be declarable while the panel owns focus" ); - // Non-vacuity: the document buffer is not a terminal either, so pin - // that the guard resolves the DOCUMENT window by asserting the - // window identity the resolver used. - assert_eq!( - s.core.borrow().primary_document_buffer(fid), - Some(doc_buf), - "the terminal resolver's window must be the document window" + assert!( + !s.semantic_terminal_declaration_is_active(fid, panel_buf), + "the focused panel's own buffer must never claim the document declaration" + ); +} + +#[test] +fn invalidated_statusline_clears_only_the_document_not_the_panel() { + use pmacs::protocol::{ByteRange, InstanceMessage}; + use pmacs::semantic_render::SemanticRenderState; + + // Round 2 finding 1. The `Invalidated` arm emits an + // authoritative-empty payload for EVERY context of the frontend. + // Once A2A-2's fan-out yields document + panel, that publishes two + // clears on a wire with ONE statusline slot, so the panel's payload + // replaces the document's. This is the live, observable half of the + // routing bug — the `Ready` arm happens to be safe today only + // because the document context is captured first. + let s = editor(); + let (fid, _doc_win, _panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + let panel_buf = { + let core = s.core.borrow(); + let panel = side_window_of(&core, fid).expect("panel"); + core.windows[&panel].buffer_id + }; + assert_ne!(doc_buf, panel_buf, "fixture: the two buffers must differ"); + + // A provider that unregisters itself mid-evaluation is the canonical + // registry-mutation invalidation. + exec( + &s, + r"_G.SL_SELF = pmacs.statusline.register { + name='self-remove', side='left', priority=100, + fn=function() pmacs.statusline.unregister(SL_SELF); return 'STALE' end, + }", + ); + + let mut sem = SemanticRenderState::for_peer(fid, 18); + sem.set_viewport(doc_buf, ByteRange { start: 0, end: 0 }, 0); + let msgs = sem.render_frame(&s); + + let targets: Vec<_> = msgs + .iter() + .filter_map(|m| match m { + InstanceMessage::StatuslineSegments { buffer_id, .. } => Some(*buffer_id), + _ => None, + }) + .collect(); + + assert!( + !targets.contains(&panel_buf), + "an invalidated evaluation must not clear the PANEL's context on the \ + document statusline wire; got {targets:?} (document {doc_buf:?}, \ + panel {panel_buf:?})" + ); +} + +#[test] +fn the_semantic_fan_out_captures_the_document_first() { + use pmacs::statusline::{ + StatuslineEvaluationOutcome, StatuslineEvaluationTarget, evaluate_statusline, + }; + + // The `Ready` arm selects by window identity, so capture order is not + // load-bearing for correctness — but it IS load-bearing for the + // falsifiability of that selector, so pin it explicitly rather than + // leaving a silent dependency. If a future change reorders the + // fan-out, this fails and whoever reads it learns why it mattered. + let s = editor(); + let (fid, doc_win, _panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + + let evaluation = evaluate_statusline( + s.lua_host.lua(), + &s.core, + &s.statusline_registry, + StatuslineEvaluationTarget::Semantic { + frontend_id: fid, + declared_buffer: doc_buf, + }, + ); + + match evaluation.outcome { + StatuslineEvaluationOutcome::Ready(windows) => { + assert_eq!(windows.len(), 2, "document + visible side window"); + assert_eq!( + windows[0].context.window_id, doc_win, + "the DOCUMENT context must be captured first" + ); + } + other => panic!("expected Ready, got {other:?}"), + } +} + +#[test] +fn consumer_decorations_follow_the_document_selection_not_the_panel() { + use pmacs::protocol::{ByteRange, InstanceMessage}; + use pmacs::semantic_render::SemanticRenderState; + + // §1.3 #5 — Projection. A selection made inside a FOCUSED PANEL must + // not paint selection decorations into the document's viewport. + // + // To DISCRIMINATE, the panel must display the SAME buffer the + // viewport declares and hold a NON-EMPTY selection while the + // document holds none. With different buffers (the first attempt) + // both routings emit nothing and the test proves nothing. + let s = editor(); + let (fid, doc_win, panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + + exec(&s, "PROBE = pmacs.buffer.list()[1]"); + { + let mut core = s.core.borrow_mut(); + // Put real text in the document buffer so a span exists. + { + let reg = core.registry.borrow(); + let _ = reg.get(doc_buf).expect("doc"); + } + // The panel shows the document's buffer and selects a range. + core.install_buffer_in_window(panel_win, doc_buf) + .expect("panel shows the document buffer"); + let panel = core.windows.get_mut(&panel_win).expect("panel"); + panel.selection = Some(pmacs::window::Selection { anchor: 0 }); + panel.cursor = 4; + // The document window selects nothing. + let doc = core.windows.get_mut(&doc_win).expect("doc"); + doc.selection = None; + doc.cursor = 0; + } + + let mut sem = SemanticRenderState::for_peer(fid, 18); + sem.set_viewport(doc_buf, ByteRange { start: 0, end: 8 }, 0); + let msgs = sem.render_frame(&s); + + let selection_decorations: usize = msgs + .iter() + .filter_map(|m| match m { + InstanceMessage::Decorations { segments, .. } => Some( + segments + .iter() + .map(|seg| seg.decorations.len()) + .sum::(), + ), + _ => None, + }) + .sum(); + assert_eq!( + selection_decorations, 0, + "a selection living in the focused PANEL must not decorate the document viewport" ); } From c4fad0731ceb726965964c0deb29a8893a87135a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:39:01 -0400 Subject: [PATCH 08/14] =?UTF-8?q?docs(lean4):=20rev=207=20=E2=80=94=20roun?= =?UTF-8?q?d=206=20review,=20five=20P1s,=20and=20reconcile=20the=20ledgers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 4a/4b split held; five P1s against rev 6's own content, all real, all reproduced. Four share a root: rev 6 verified its external facts and under-verified its internal ones. 1. Stage 4a's declared footprint excluded the tests its own acceptance required. 46a-46e cannot live in tests/auto_pair_acceptance.rs, which criterion 46 requires byte-identical. Footprint now names tests/typed_edit_chain_acceptance.rs and gates on it. 2. Pending abbreviation state had the wrong owner. pmacs is multi-frontend: EditorCore.views is per-FrontendId with its own active window, take_typed_edit is already frontend-keyed, and buffer.after-switch fires with no arguments — so a buffer-keyed clear-on-switch lets any frontend discard another's pending abbreviation. Now keyed (frontend, buffer) with a window check, frontend-scoped clearing, a frontend.detached purge, and acceptance 45i, which the buffer-keyed design passes every other criterion without. 3. The shortest-match rule was missing its tie-break: upstream keeps declaration order among equal-length shortest keys, and 101 prefixes have equal-shortest candidates resolving to different symbols (f picks f< over f>). A pairs-iterated Lua map cannot express this, so the vendored artifact is now an ordered sequence and resolution sorts by (#key, source rank). Rev 6 missed this because it declared the package ships no README after a 404 on the package root, with the directory listing showing src/README.md already in hand — a 404 on a guessed path is not evidence of absence, and the README states the rule in one sentence. 4. The generator's rejection rule rejected the current table: \ is a key and " begins eleven, while acceptance 45d requires \ to work. Replaced with canonical lossless escaping; aborts only on duplicate keys, invalid UTF-8, and a failed self-round-trip. 45g no longer claims to diff against abbreviations.json, which is not shipped. 5. Durable and volatile state were not reconciled. agent-handoff.md anchored main at d152120 with neither #167 nor #170 and no Lean arc bullet at all; active-work.md kept 407 lines of merged Stage 1/2/3a/3b history against its own instruction to prune merged entries, under a stale snapshot date. Durable facts moved to the handoff; the ledger keeps only the unlanded Stage 4 lane. Also corrected: 119 multi-codepoint symbols (26 with $CURSOR), not 93; three backslash values, not two; Q#LN22 now states the terminating-\ reprocess rule acceptance 45d depended on; acceptance 38 says the terminator is retained, so undo restores "\alpha " with its space; coherence cites golden-journey step 5, not step 4; and the config-registry prior art points at Q#LN22. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 435 +++---------------------------------- docs/agent-handoff.md | 71 +++++- docs/lean4-mode-framing.md | 324 +++++++++++++++++++++++---- 3 files changed, 371 insertions(+), 459 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 52d44ba..47c3677 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -1,6 +1,6 @@ # Active work — cross-machine resume ledger -**Snapshot: 2026-07-25.** This file records volatile work that has not +**Snapshot: 2026-07-26.** This file records volatile work that has not landed on `main`. Read it after `docs/agent-handoff.md`. Remove completed entries when their PR merges; do not let this become a second permanent backlog. @@ -59,421 +59,40 @@ If it does not, stop and repair the remote/fetch configuration. ## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING -- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review - round, all twelve checks green). Branch `githubsucks/lean4-stage1` - retained; it was worked in the shared checkout (no sibling worktree). -- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as - the branch's first commit (`a382965`) after three review rounds. **Seven - stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star: - match or exceed VS Code's Lean support. -- **Stage 1 implemented; no wire change (protocol stays v20), no LSP, no - frontend change.** Four commits: framing, grammar, theme captures, - editing surface + acceptance. - - `Cargo.toml` + `src/syntax.rs`: `arborium-lean` 2.18 and one - `BUILTIN_LANGUAGES` entry named **`lean4`** (Q#LN2 — the name becomes - the `didOpen` language_id), claiming `.lean` only. - - `src/highlight.rs`: four capture entries — `constructor`, `character`, - `keyword.conditional`, `warning`. - - `builtin/runtime/{comment,pair,syntax}.lua`: `--` comments, the - `⟨⟩ ⦃⦄ ⟮⟯` pair set, the `lean` → `lean4` modeline alias. - - `tests/lean4_stage1_acceptance.rs` plus unit tests in `syntax.rs` / - `highlight.rs`: 12 criteria, 17 tests. -- **Q#LN1's open obligation is discharged.** `tree-sitter-lean4` is - unusable (depends on `tree-sitter ^0.25` directly against our 0.26, - exports no `LANGUAGE` const despite its README, packages no queries); - `arborium-lean` rides `tree-sitter-language 0.1` with a pre-generated - ABI-15 parser. `cargo tree -d` shows no duplicate core. The parse smoke - pins the failure mode that matters: `→`/`∀`/`≥` must produce - `(arrow)`/`(forall)`/`(comparison)`, since a mismatched-core build - degrades silently on exactly those characters rather than failing loudly. -- **Q#LN4 is a deliberate retro-paint of seven language entries**, not - four: `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated - base-first into javascriptreact/typescript/typescriptreact. Its shape is - "every capitalized identifier" (`#match? "^[A-Z]"`) plus every Lua table - brace — not "constructors". Pinned in both directions per #146. -- Implementation findings not in the framing: - - `warning` had to move from bold red to bold **bright** red: `number` - is plain `fg(1)`, so `sorry` and an adjacent numeric literal were the - same colour. Found by writing the test. - - `Some(1)` is **not** `@constructor` — in call position a narrower - `@function` pattern wins. Only bare or pattern-position capitalized - identifiers reach it. Pinned so the blast-radius claim stays honest. - - Lean node kinds nest: `module > declaration > def|theorem`. - - `pmacs.parse.injection_aliases` is a documented **write-only** Lua - proxy (canonical map is Rust-side), so fence tests must drive - `_parse_now` and inspect layer languages, never read the table back. -- **Review round 1 addressed.** The finding: acc12's server-list assertion - could not fail for the regression it named — the shared `editor()` - helper wipes `pmacs.lsp.config` before any buffer opens, so - `#pmacs.lsp.list() == 0` holds for every language regardless of what - Stage 1 ships. It now asserts against a **pristine** `EditorState` that - `pmacs.lsp.config.lean4` is nil, with a non-vacuity check that the same - lookup finds `rust`; bite-verified by adding a `lean4` config to - `lsp.lua` and watching it fail. Also fixed a stale column in a - `highlight.rs` comment. -- Verification on this branch: `cargo fmt --check` clean; strict workspace - Clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1 - 9/9; comment toggle 14; auto-pair 45; injection 4; M4 121; required GPU - 152; **isolated-config workspace sweep 3,150 across 90 suites**; - `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` - for the reason recorded in the bottom-panel lane below. -### Stage 2 — multi-root LSP server affinity (Q#LN15) +- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), + #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full + histories were pruned from this ledger in round 6, per this file's own + instruction to remove entries when their PR merges; the durable facts + now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 7 + carries the decisions. -- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout, - based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not - for Lean: **the diff contains no Lean content**, because `ensure_server` - is the one server-affinity function every LSP language shares and a - cross-cutting change to it must not be reviewable only as a Lean - feature. -- Three files, no protocol change: `src/lua_bindings/mod.rs` (the - `lsp.list()` row builder gains `root_uri` + `cwd`), - `builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`; - `ensure_server` hoists it above the reuse loop and matches on it), - `tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21). -- **The rule that keeps this from regressing every other language: the - affinity key is the root only when a root was actually FOUND.** - `project_root_for` never returns nil for a file with a path — its last - resort is the file's own directory — so a naive `(language_id, root)` - key gives every directory of loose scratch files its own server, for - every language. `source` is `"config" | "detected" | "fallback"` and - only the first two become a key. -- **Wire-identical for the fallback case, and that is provable rather - than hoped.** Matching is on the spawned spec's `root_uri` (nil matching - nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries - the directory and `build_initialize` derives the identical `rootUri` - from `cwd` when the field is None, using a percent-encoder with the same - allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`) - is the **only** reader of `spec.root_uri` in the tree. -- Deliberate behavior change, asserted not discovered: a server - hand-spawned from `init.lua` with only `cwd` set also reads back nil, so - a root-bearing attach will not adopt it. -- `config[language].root` may now be a `function(path) -> string|nil`, - memoized per directory — needed because the hoist puts root resolution - on every attach rather than every spawn. The memo is keyed **weakly by - the resolver function itself**, so replacing `config[lang].root` cannot - serve a root the previous resolver computed. This is Q#LN8's - generalization landing early; the Lean resolver that uses it is Stage 3. -- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`, - 8/9 against the pre-change `mod.rs`, and — the one that matters most — - installing the naive always-key-on-root variant fails acceptance 20 and - 21 exactly as Q#LN15 part 2 predicts. The four that survive the first - bite (13, 15, 16, 19) are the regression pins; passing on both sides is - their job. -- Every fixture sets `pmacs.project.set_search_boundary` at its own - tempdir root. Without it the marker walk climbs to the filesystem root - and a stray `.git` above the temp directory turns the markerless cases - into detected ones — the assertions would still pass while testing - nothing. -- **Found but not fixed here (pre-existing, own lane):** `ensure_server` - never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a - `restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on - the auto-attach path. At least one existing test sets it believing it - takes effect. Out of scope for a PR whose acceptance 16 pins existing - attach behavior as unchanged. -- **Review round 1 addressed.** The blocker was process, not design: the - test file was committed *before* `cargo fmt` ran, so the fix sat - uncommitted in the working tree and the branch as pushed failed the - first gate. The reported "fmt clean" described the worktree, not the - branch — gate results are only meaningful when run against the pushed - tree. Also added the two pins review asked for (a **string** `config - .root` as an affinity key — acc17 only covered the function form; and - `root = false` reading as unset), each bite-verified against exactly - the mutation it targets and neither against the other. And documented - the canonicalization obligation: the `"detected"` arm is canonicalized - for free, a **configured** root is not, so on macOS a resolver - returning `/var/…` and a detected `/private/var/…` are different keys - for one directory. Stage 3's Lean resolver is the first real consumer, - so the obligation is written at the point of use. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; - multi-root 11/11; M4 121; statusline 7; completion popup 9; auto-pair - 45; required GPU 155; **isolated-config workspace sweep 3,164 across 91 - suites**; `git diff --check` clean. The sweep needs an isolated - `XDG_CONFIG_HOME` and `-- --skip basedpyright`. - -### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`) - -- 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 15/15 on Linux (14 on macOS — see below); multi-root - 13/13; M4 121; required GPU 155; **isolated-config workspace sweep - 3,189 across 93 suites, zero failures**; `git diff --check` clean. -- **Two flakes/portability facts from CI round 1, both worth keeping:** - 1. `composition_overhead_under_ten_percent` tripped once in a local - sweep at 18.8% against a 10% budget, then passed 3/3 in isolation - here, passed in isolation on main, and passed a full sweep rerun. - The tell is in its own output: the same run reported realistic-frame - overhead as **-4.6%**, and a negative figure is measurement noise, - not added work. Load-sensitive under a parallel `--workspace` run. - 2. **A non-UTF-8 filename fixture cannot be built on macOS.** APFS - enforces valid UTF-8, so `std::fs::write` fails with EILSEQ - ("Illegal byte sequence") before the code under test is reached. - `#[cfg(unix)]` is NOT sufficient for such a fixture — - `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. - -### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`) - -- Same worktree `../pmacs-lean-stage3`, **branched off - `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response - seam and `pmacs.fs.canonicalize`, so it is strictly sequential. - **Retarget PR #170 to `main` BEFORE merging #167, not after** — the - kill-ring lesson exactly. (Round 1 of this ledger entry stated the - reverse in its first sentence and the correct rule in the next; the - review caught it. A safety rule written twice with opposite senses is - worse than not written.) -- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in - `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`, - a `leanprogress` mode plus `waitForDiagnostics` validation on - `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (40 tests). - No protocol change. -- **Stage 1's acceptance 12 is half superseded and was rewritten, not - deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a - Stage-3 front-run; 3b is that stage. What survives is the restraint - half — constructing an editor spawns nothing though the config now - names `lake`, and opening a Lean buffer with no server configured - spawns nothing — which is what holds Q#LN7's "not at init" promise. -- **The marker test is wrong in two opposite directions if done naively** - and both are pinned: `io.open` SUCCEEDS on a directory (so truthiness - accepts a `lean-toolchain` dir), but requiring a non-nil read rejects - an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, - not content). Discriminator is `read`'s SECOND return; decline only on - a non-nil err. Probed on LuaJIT 2.1. -- **Fifteen bites recorded, each against the committed tree.** R1: bare - `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a - passes; no canonicalization → symlinked open spawns two servers; no - re-attach after the swap → three latch tests fail; hook keyed on the - attachment → the missing-`lake` case fails; `waitForDiagnostics` - without `version` → acc37 fails with InvalidParams. R2: skip retiring - a terminal server → `attempt` reaches 3; no originating-buffer gate → - the Lean buffer is left on the `lake` stub; retry-forever → the - failing-fallback test fails; version-probe any command → the - working-wrapper test fails; no disabled guard → the unconfigured test - sees "`nil` could not be started". R3: verdict keyed on `watching` → - the late-verdict test finds the buffer still on `lake`; `buf_key` - rewritten per load → the second-buffer test fails; hardcoded - `lake serve` → the wrapper-naming test fails. -- **Round-2 review: three more P1 lifecycle defects, suite 20/20 with - all of them live.** (1) The crashed primary respawned forever — - skipping the retire call avoided corrupting terminal servers but left - `next_restart_at` armed. **`forget` is the call for a TERMINAL server** - (it requires terminal state and removes the client, dropping the - restart timer); `stop` is for a live one and corrupts a terminal one. - (2) Re-attachment targeted whatever buffer was active when the async - verdict landed; an unrelated Rust attachment satisfied "a different - server id". (3) A failing fallback retried every tick forever, silent. - Plus two P2s: the Lake version parser was applied to arbitrary wrapper - output, and an UNCONFIGURED `config.lean4` was reported as failure and - latched, poisoning the session. -- **Round-3 review: two more P1s, both asynchronous correlation, suite - 25/25.** (a) `probe.watching` is cleared when the server initializes, - so a SLOW version verdict arrived with nil and retired nothing — - `_attach_buffer` returned the still-live primary and the retry called - it success, so status and config said "fell back" while the buffer - stayed put. **That is the round-1 silent no-op reached through a third - event ordering.** `probe.primary` is now separate from - `probe.watching` and survives initialization. (b) `buf_key` was - rewritten on every Lean `after-load`, so a second Lean buffer opened - before the verdict became the rebuild target while the latch still - watched the first buffer's server. Target buffer and primary server - are one fact and are now armed together, once. Plus a P2: the failure - message hardcoded `lake serve` after the latch became - command-agnostic, sending wrapper users to debug the wrong binary. -- **Round-4 review: one P1, and it is the same defect a FOURTH time.** - `pmacs.lsp.config.lean4` is a single global entry, so swapping its - command invalidates **every** Lean buffer and **every** Lean server — - Q#LN15 gives one per project root. Rounds 1–3 each fixed the repair - for one buffer and one server; round 4 is "repair the armed target, - strand the rest". The shape that finally holds: retire ALL `lean4` - servers on latch, and repair each buffer **lazily and at most once** - when it becomes active (`buffer.after-switch` + the tick), because - `_attach_buffer` is active-buffer-only and cannot reach the others. - The per-buffer once-only bound is what stops a failing fallback - retrying forever — the round-2 defect a naive global repair loop would - have reintroduced for every buffer instead of one. Plus a P2: the - argument-inclusive attribution was implemented but pinned only by - "contains the command name", so a mutation dropping every argument - still passed. -- **Round-5 review: one P1 plus a frontend scope hole, and four more.** - (1) A fallback that SPAWNS and then dies retried forever: the - once-per-buffer guard bounds `_attach_buffer`, not the server it - produced, and `ensure_server` never forwards `cfg.restart` so the - fallback inherits `OnCrash` — respawned by the manager with no - ceiling, silently, because `latched` had disabled the primary's poll. - The fallback now gets its own one-shot die-before-initialize watch. - (2) **Simultaneous frontends**: both repair triggers read the ambient - `pmacs.window.buffer()`, and the daemon restores `active_frontend` to - the last-dispatched one before `tick_processes`, so a Lean buffer - active in ANOTHER frontend gets no `after-switch` and stays stale. - Fixed at the right seam — **make CONSUMPTION safe**: both - `attached_for_active` and `attachment_for_request` now refuse a record - whose server is dead (the former rebuilds, the latter reports none, - since it must not perturb LSP state). Healing at the point of use is - frontend-agnostic, because whichever frontend runs a command is active - while it runs. (3) The retirement sweep selected on `language_id`, so - it stopped USER-spawned Lean servers too; it now keys on the - `default-lean4` label `ensure_server` stamps, which is the derivation - discriminator. (4) `probe.latched` gated repair even when NO swap - occurred, so an already-fallback config was retried and misreported. - Split out `probe.fallback_installed`. (5) The once-per-buffer - assertion counted TABLE KEYS, which cannot distinguish "once per - buffer" from "every tick for one buffer" — cardinality stays 1 either - way. Now a numeric attempt counter; the bite shows **174 vs 1**. -- **Round-6 review: four P1s and one P2, suite 40/40.** (1) General - point-of-use healing treated a crashed OnCrash server as absent and - spawned beside it while its old id still had `next_restart_at` armed; - `attach_buffer` now forgets a terminal record before replacement. - `attachment_for_request` remains non-attaching and preserves the - record, so a same-id restart can recover instead of being orphaned. - (2) The fallback watch was scalar, while Q#LN15 permits simultaneous - per-root servers and lsp.lua can create them without passing through - Lean's repair function. Watches are now per-SID and discover every - config-driven Lean server from a private origin table. (3) The shipped - `lean.wait-for-diagnostics` command bypassed both safe resolvers and - still consumed a stopped record; it now uses a command-safe resolver, - waits asynchronously for a healed replacement to initialize, and the - test requires the real request to finish. (4) When no config swap - occurred, one failed root still swept a healthy root; that arm now - retires only the SID whose verdict fired. (5) `label` is public and - unreserved, therefore not ownership. lsp.lua records successful - config-driven spawns privately, and every Lean lifecycle decision keys - on that origin fact; the user-server pin deliberately collides on - `default-lean4`. All five bites against `19f48d4` discriminate: the - old files produce 2 same-root servers, a fallback attempt of 4, a - shipped command still targeting `stopped`, retirement of the healthy - root, and retirement of the colliding user server, respectively. -- **DURABLE LESSON — "the test that passes" vs "the test that - discriminates."** Green tests across six rounds repeatedly pinned only - a nearby helper or an absence, and only biting exposed it. **Carry this - to `docs/agent-handoff.md` when the lane lands.** The concrete shapes, - all from this branch: - 1. R1 acceptance 36 asserted "every server is terminal" — pinning the - ABSENCE of the fallback it claimed to test. - 2. "No live non-fallback server" misses a respawn loop: a respawning - server sits in `crashed` most of the time. `attempt` counts - respawns; liveness does not. - 3. Returning to a buffer via `find_or_open` re-fires - `buffer.after-load`, which repairs the attachment regardless of the - code under test. Use `switch_buffer`. - 4. A MISSING executable fails synchronously inside `after-load`, where - the rebuild happens inline — no async race can occur. Only the - probe path exercises asynchronous ordering. - 5. A mutation that RAISES (indexing a nil config) is swallowed by the - hook's pcall, so the bite "passes" for the wrong reason. A bite must - reproduce the original shape, not merely break the code. - 6. A fixture whose `serve` sleeps can never let the primary initialize - first, so it cannot reach the ordering where a late verdict must - retire a LIVE server. - 7. Asserting on a field that no longer exists (`_probe.reattach_from` - after a refactor) reads as nil and passes for nothing. Assert - positive facts — a count, a command string — not absences. - 8. Counting DISTINCT KEYS cannot bound REPEATED WORK: a per-tick retry - on one buffer keeps `#repaired == 1` forever. Count the attempts, - not the things attempted against (bite: 174 vs 1). - 9. A NONEXISTENT executable only exercises synchronous ENOENT. To - reach "spawned, then died", the fixture must actually spawn. - 10. Calling the two SAFE HELPERS directly does not pin a shipped - command that bypasses both. Drive the command registry entry and - require its terminal result — replacing a dead record with a - `starting` server is still not success if the request is issued - before initialize. - Rule: **a test is not evidence until the mutation it targets has been - shown to fail it.** -- **SECOND DURABLE LESSON — a scope error repeats until the scope is - named.** The "fallback silently does not happen" defect came back four - times: no re-attach; re-attach cleared by an unrelated buffer; - re-attach satisfied by the server being replaced; re-attach of one - buffer while the others stay stale. Every fix was locally correct and - none asked *what does this config swap invalidate?* — the answer being - every Lean buffer and every Lean server, because the config entry is - global and servers are per-root. **When a change edits shared state, - enumerate everything derived from it before repairing anything.** -- **SUBSTRATE BUG FOUND, not fixed here (framing §6).** - `LspManager::stop` on an ALREADY-terminal server takes its - not-initialized branch, terminates the dead process and sets - `ShuttingDown { .. None }` on the premise that "the next exit - observation cleans up" — but the exit already happened, which is what - made it `Crashed`. No further event arrives, so the client is stuck in - `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so - `attach_buffer` never rebuilds, and `forget` refuses it for not being - terminal. **Stopping a dead server is what makes it un-replaceable.** - Lean works around it by dispatching on state: `forget` when - terminal, `stop` when live. Merely SKIPPING the call is not - enough — that leaves `next_restart_at` armed. -- Round-1 review found four P1s, all real: the latch swapped the config - but never spawned or re-attached (and acc36 *asserted every server was - terminal*, pinning the absence of the fallback); a missing `lake` - bypassed probe and latch entirely because the hook keyed on an - attachment that ENOENT prevents; `waitForDiagnostics` omitted the - `version` Lean requires; and the ledger stated the dangerous stacking - order. -- The probe's non-zero exit is deliberately NOT a fallback trigger — - §2.9's elan shim makes `lake --version` fail where `lake serve` still - works. Only a parseable version below 3.1.0 triggers it; the - server-failure latch covers the rest. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,829 default + 2,003 CRDT library tests; - lean4 server 40/40; lean4 stage 1 9/9; dispatch seams 15/15; - multi-root 13/13; M4 121; required GPU 155; **isolated-config - serial workspace sweep 3,229 across 94 suites, zero failures**; - `git diff --check` clean. (Round 1 of - this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the - fixes were pushed. The ledger's protocol is that verification - describes the pushed tree; recording it late is the #161 fmt-blocker - error in a slower form.) - -### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4 — framing rev 7, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) - Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main that had advanced 50 commits mid-review; the only conflict either time was this ledger's own lane headings, resolved by keeping both sides. - Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. - Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No + Framing-only so far: `docs/lean4-mode-framing.md` **revision 7**. No code. Awaiting user approval before implementation, per the workflow. +- **Round 6 review found five P1s, four of them internal to rev 6** — + facts about pmacs the revision asserted without checking, while its + external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint + omitted the test file its own acceptance requires; pending + abbreviation state was keyed by buffer when pmacs is **multi-frontend** + (`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already + frontend-keyed, and `buffer.after-switch` fires with NO arguments, so + a buffer-keyed clear lets any frontend discard another's pending + state); the shortest-match rule was missing its **tie-break by source + declaration order**, which 101 prefixes depend on and a `pairs`- + iterated Lua map cannot express; and the generator's "abort on keys + needing escaping" rule **rejects the real table** (`\` is a key, `"` + begins eleven). +- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared + the upstream package ships no README after fetching the package root, + with the directory listing showing `src/README.md` already in hand. + The README states the tie rule in one sentence. - **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).** 4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua` plus `pair.lua` re-expressed as one registered consumer, no behavior diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index b2d0aeb..a176505 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,7 +1,8 @@ # Agent handoff — cross-machine continuity -**Last updated: 2026-07-25, after the inline-math slice (#158) landed — -the first mathematical typesetting in pmacs — following find-file (#162), +**Last updated: 2026-07-26, after Lean 4 stages 3a and 3b (#167, #170) +landed — pmacs' first Lean language server — following the inline-math +slice (#158), the first mathematical typesetting in pmacs, and find-file (#162), the dired arc's Stage 0, and COHERENCE.md (#163), Lean 4 Stage 1 (#160), the minimap blank-slab fix (#159), bottom-panel Stage 1 (#155), the inline-math re-scout (#154), the vterm PTY-flake fix (#153), and the @@ -25,15 +26,15 @@ reads it the way you just did. For volatile branches, checkpoints, verification, and recovery commands, read `docs/active-work.md` immediately after this file. -## 1. Where the project stands (2026-07-25) +## 1. Where the project stands (2026-07-26) -- `main` @ `d152120` (the bottom-panel landed-doc refresh #156 atop the - inline-math slice #158, dired Stage 1 #165, the GPU terminal input fix - #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163, - find-file #162, Lean 4 Stage 1 #160, minimap blank-slab #159, - bottom-panel Stage 1 #155). Protocol unchanged at **v20**. The bullets - below describe the arcs in their own terms; this line is the - head-of-`main` anchor. +- `main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a #167, the + bottom-panel landed-doc refresh #156, the inline-math slice #158, + dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2 + #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean + 4 Stage 1 #160, minimap blank-slab #159, bottom-panel Stage 1 #155). + Protocol unchanged at **v20**. The bullets below describe the arcs in + their own terms; this line is the head-of-`main` anchor. - **`COHERENCE.md` is now required reading and a required framing input — #163.** It carries the product-coherence thesis, an audited scorecard, per-concern gaps, and §20's priority order, and it is the @@ -42,6 +43,56 @@ commands, read `docs/active-work.md` immediately after this file. interaction islands added, config-registry adoption, background-work attribution. Its §2 grades the golden journey **broken at step 3** (`pmacs .` exits 1). +- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED** + (`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge + `d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a + `lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language + server with a Lake-aware outermost root, a lazy toolchain probe, a + one-shot `lean --server` fallback, and `waitForDiagnostics`. **No + protocol change in any stage** (still v20). + - **Two of the four stages contained no Lean at all**, and that is the + arc's organizing rule: *no PR mixes a cross-cutting substrate change + with Lean feature content.* Stage 2 made LSP server affinity + per-project-root (`ensure_server` had been reusing one server across + roots — a correctness bug for every language, not just Lean). Stage + 3a added notification/response subscription seams to + `handle_server_requests`, the single shared LSP event drain, plus + `pmacs.fs.canonicalize`. + - **Two consecutive re-scouts found that rule broken by the stage + being scouted** — Stage 3 in round 4, Stage 4 in round 5, each time + by a risk column that contradicted its own prose. The rule is not + self-enforcing. Re-check every remaining stage's risk column at + scout time. + - **A configured LSP root must be a canonical absolute path.** It + reaches `file_uri_for` verbatim and that URI is the affinity key, so + one package opened by two spellings spawns two servers. Stage 3a's + `pmacs.fs.canonicalize` is the primitive; it returns nil rather than + a lossy path for non-UTF-8 input. + - **`LspManager::stop` on an already-terminal client strands it in + `ShuttingDown` forever** — `server_is_live` then counts it live so + nothing rebuilds against it, and `forget` refuses it for not being + terminal. *Stopping a dead server is what makes it un-replaceable.* + Stage 3b works around it by dispatching on state (`forget` when + terminal, `stop` when live); merely skipping the call leaves + `next_restart_at` armed. The real fix is unframed substrate work. + - **`elan` shims lie**: `lake --version` and `lean --version` can both + fail ("no default toolchain configured") on a machine where Lean + otherwise works, so `command -v lake` is worthless as a capability + check. Lean acceptance is fake-server; live smokes must be PATH- + **and** success-gated. + - Stage 3b took six review rounds, and **the same defect appeared four + times**: "the fallback silently doesn't happen," as no re-attach, + then re-attach cleared by an unrelated buffer, then satisfied by the + very server being replaced, then repairing one buffer while the rest + stayed stale. Each fix was locally right; none asked what a *global* + config swap invalidates. The durable lesson is to heal at + **consumption** — the point where a stale record is handed out — not + at the moment of the swap. + - Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode + input method) are framed and awaiting approval; stages 5 (goal + panel), 6 (`#eval` output channel), and 7 (module hierarchy) are + framed but not scouted against current `main`. + - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU frontend. **No protocol change (still v20); the whole slice lives in diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index e39eb36..ca50696 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. +Revision 1 — initial. Current revision: **7**. ### Round 1 (rev 1 → rev 2) @@ -288,11 +288,15 @@ landed and its citations are historical record, not navigation. Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main` @ `d400f30` produced **six findings that change the plan** and three -that confirm it. The pmacs-side facts were verified in a worktree at +that confirm it. (Round 6 found five more, four of them internal to this +revision; read that section too before trusting a rev-6 statement.) The pmacs-side facts were verified in a worktree at that commit; the upstream facts were verified by downloading and reading `leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the algorithm, not its documentation, since the `lean4-unicode-input` -package ships no README. +package ships no README. *(Round 6: it does, at `src/README.md` — see +that section. Corrections to round 5's own numbers are marked inline +below rather than rewritten, per the standing rule that revision +entries are record, not navigation.)* 1. **Stage 4 violated this document's own splitting rule — the same way Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting @@ -377,6 +381,14 @@ package ships no README. needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs does not. + *Corrected in round 6.* **119** symbols are multi-codepoint, of which + 26 carry `$CURSOR`; "93" was the non-`$CURSOR` subset stated as a + total. **Three** values contain a backslash — the `\` → `\` identity + entry was missed. And this entry's biggest omission is not a number: + the shortest-key rule needs a **tie-break by source declaration + order**, which the README round 5 said did not exist states outright. + §2.11 and Q#LN11 carry the corrected facts. + Confirmations, recorded because each was load-bearing and unverified: 7. **`take_typed_edit`'s one-shot contract is unchanged** @@ -404,6 +416,70 @@ Citation drift repaired per COHERENCE §25, on the same terms as round and the revision-history entries above, which are historical record rather than navigation. +### Round 6 (rev 6 → rev 7) + +The 4a/4b split held; five P1s against the revision's own content, all +real, all reproduced. Four share a root: **rev 6 verified its external +facts and under-verified its internal ones.** + +1. **Stage 4a's declared footprint excluded the tests its acceptance + required.** Q#LN10 listed three production files while 46a–46e demand + chain-specific tests that cannot live in + `tests/auto_pair_acceptance.rs` — criterion 46 requires that file + byte-identical. Footprint now names + `tests/typed_edit_chain_acceptance.rs` and adds it to the PR's gates. +2. **Pending state had the wrong owner.** §2.11 reasoned "no + multi-cursor, therefore one point" and Q#LN22 keyed pending + abbreviations by buffer. pmacs is multi-frontend: `EditorCore.views` + is per-`FrontendId` with its own active window, `take_typed_edit` is + *already* frontend-keyed, and `pmacs.frontend.id()` exists. Two + frontends on one Lean buffer — the TUI-plus-GPU case this project + ships — would share one slot. Worse, `buffer.after-switch` takes no + arguments, so a buffer-keyed clear-on-switch lets any frontend + discard another's pending abbreviation. Now keyed + `(frontend, buffer)` with a window check, frontend-scoped + after-switch clearing, a `frontend.detached` purge, and acceptance + 45i — which the buffer-keyed design passes every other criterion + without. +3. **The shortest-match rule was missing its tie-break, and rev 6's + research method is why.** Upstream keeps declaration order among + equal-length shortest keys. The README states it in one sentence — + and rev 6 asserted "the package ships no README" after a 404 on the + package root, without checking the directory listing it had already + fetched, which shows `README.md` under `src/`. **A 404 on a guessed + path is not evidence of absence.** The rule is load-bearing: 101 + prefixes have equal-shortest candidates resolving to *different* + symbols (`f` → `f<` not `f>`; `"` picks `"A` from eleven). A `pairs`- + iterated Lua map cannot express it, so Q#LN11 now emits an ordered + sequence and Q#LN22 sorts by `(#key, source rank)`. +4. **The generator's rejection rule rejected the current table.** "Abort + on keys needing Lua escaping" would reject `\` and the eleven `"X` + keys — and acceptance 45d requires `\` to work. Replaced with + canonical lossless escaping; the generator aborts only on duplicate + keys, invalid UTF-8, and a failed self-round-trip. Relatedly, 45g + claimed the suite compares against `abbreviations.json`, which is not + shipped; it now pins self-consistency properties and leaves + source fidelity to the generator, where the source is in hand. +5. **Durable and volatile state were not reconciled** — + `docs/agent-handoff.md` still anchored `main` at `d152120` with + neither #167 nor #170, while `docs/active-work.md` kept full merged + Stage 3a/3b histories against its own instruction to remove merged + entries, under a stale July 25 snapshot date. Round 5 updated the + ledger and skipped the handoff; per CLAUDE.md both are required + reading, and the one that outranks the other was the one left wrong. + +Corrections carried in the same revision, each verified against the +data: the README exists (finding 3); there are **119** multi-codepoint +symbols, of which 26 carry `$CURSOR` — rev 6's "93" was the +non-`$CURSOR` subset reported as a total; **three** values contain a +backslash (`\`, `n`, `setminus`), not two; Q#LN22 now states the rule +acceptance 45d depended on, that an unclaimed terminating `\` is +reprocessed as a new leader; acceptance 38 now says the terminator is +retained, so undo restores `\alpha ` with its space; the coherence +section cites golden-journey **step 5** ("Edit immediately"), not step +4; and §8's config-registry prior art points at Q#LN22, where the gate +now lives. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -828,8 +904,15 @@ them from the store needs a Rust-side policy, not a Lua filter. Q#LN18. Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`, package `lean4-unicode-input`, files `AbbreviationProvider.ts`, `TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`, -`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no -README, so the algorithm below is read off the source. Apache-2.0. +`AbbreviationConfig.ts`, `abbreviations.json`, and — round 6 — the +package README at `lean4-unicode-input/src/README.md`. Apache-2.0. + +**Rev 6 first claimed this package ships no README. It does**, at +`src/README.md` rather than the package root, and the 404 on the root +path was taken as absence without checking the directory listing that +was already in hand. That cost the tie rule below: the README states it +in one sentence, and reading only the code left it as an inference from +`Array.prototype.sort`'s stability rather than a documented contract. **Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key having `p` as a prefix, sorts them by **key length ascending**, and maps @@ -845,6 +928,32 @@ Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`), surprising enough to be worth an acceptance criterion), `alp7` → `α7` via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches). +**The tie rule, and why it is a constraint on the vendored format.** +When several shortest keys have equal length, upstream takes **the one +declared first in `abbreviations.json`**. The README says so outright; +the code achieves it because `Object.keys()` yields JSON insertion order +and `Array.prototype.sort` is stable. Ties are not rare: **101 prefixes +have equal-shortest candidates that resolve to *different* symbols**. +`f` picks `f<` → `‹` over `f>` → `›`; `"` picks `"A` → `Ä` from eleven +equal-length candidates; `(` picks `()` over `(=`, `(b`, `((`, `([`. + +A Lua table iterated with `pairs` has no order at all, so **a generated +`{ [key] = symbol }` map cannot express this contract** — it would +resolve these 101 prefixes nondeterministically, and worse, *stably +wrong* per build. Q#LN11 therefore carries source rank alongside the +symbol. + +**Two things the README explains that the code does not.** `Tab` is the +manual early-replacement trigger upstream binds, which is why +`getReplacementText`'s shortest-prefix rule is user-visible at all +rather than an internal detail. And the `[]_`/`{}_` entries in the table +are not symbols anyone types — they are **decoys**, added so that `\[` +is not uniquely-and-completely matching and therefore does not eagerly +expand before the user can type the second `[`. That is the same +collision Q#LN22 handles from the pairing side, solved upstream by +editing the data. Anyone regenerating the table must not "clean up" +those entries. + **Tracking.** The leader `\` is inserted into the buffer like any other character, and the tracked range starts after it; the replaced range spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the @@ -881,8 +990,10 @@ abbreviation the cursor has left. pmacs has no cursor-motion hook (round-5 finding 3), so this seam does not exist here and Q#LN22 makes abandonment lazy instead. -**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` → -`\n`, so an expansion can insert a backslash; upstream sets +**The re-arm guard pmacs does not need.** Three values contain a +backslash — `\` → `\`, `n` → `\n`, and `setminus` → `\` (rev 6 first +said two, dropping the `\` → `\` identity entry) — so an expansion can +insert a backslash; upstream sets `doNotTrackNewAbbr` across the replace so that backslash does not open a new abbreviation. In pmacs the expansion is a programmatic `buf:replace` that arms no typed-edit record, so the chain sees nothing and cannot @@ -891,9 +1002,25 @@ contract, not by accident — and the acceptance must pin it, because a future consumer that inferred from buffer text rather than provenance would reintroduce the bug. -**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a -`Set` and sorts changes bottom-up for that reason; -pmacs has one point, so one pending abbreviation per buffer. +**What pmacs does not have to carry.** Multi-cursor within a frontend. +Upstream tracks a `Set` and sorts changes bottom-up +for that reason; pmacs has one point per frontend view. + +**What pmacs has instead, and rev 6 got wrong.** Rev 6 read "no +multi-cursor" as "one point" and keyed pending state by buffer alone. +**pmacs is multi-frontend**: `EditorCore.views` is a +`HashMap`, each with its own active window and +cursor; `take_typed_edit` is already keyed by frontend +(`typed_edit_armed: Option<(FrontendId, TypedEditRecord)>`, matched +against `active_frontend`); the record carries `window` as well as +`buffer`; and `pmacs.frontend.id()` is exposed to Lua. Two frontends +editing the same Lean buffer — the ordinary TUI-plus-GPU case, not an +exotic one — would share a single buffer-keyed pending slot, so one +could extend, expand, or silently clear the other's half-typed +abbreviation. `buffer.after-switch` makes it worse: it fires with no +arguments, so a buffer-keyed clear-on-switch would let *any* frontend's +navigation discard a pending abbreviation belonging to another. Q#LN22 +keys the state accordingly. ## 3. Decisions @@ -1340,11 +1467,27 @@ claim a reader must be able to check without reconstructing `src/editor.rs`'s include list. **Stage 4a ships this and nothing else.** Its whole content is: -`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer, -and the `include_str!` line. Round 5's finding 1 is why this is a PR and -not a first commit — `pair.lua` is every language's auto-pairing, and a -reviewer looking at a Lean PR should not have to also review a rewrite -of it. + +| File | Change | +|---|---| +| `builtin/runtime/typed_edit.lua` | new — the chain owner | +| `builtin/runtime/pair.lua` | re-expressed as one registered consumer | +| `src/editor.rs` | one `include_str!` line, before `pair.lua`'s | +| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e | +| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** | + +Rev 6 listed only the first three and then required criteria 46a–46e, +which no existing suite can host: the auto-pairing suite must stay +untouched (that is the whole point of criterion 46), so the chain's own +behavior — take-once, priority order, claim-stops-chain, throw +containment — has nowhere to live. A declared footprint that excludes +the tests its own acceptance demands is not a footprint. The new suite +joins the required gate list for this PR alongside +`tests/auto_pair_acceptance.rs`. + +Round 5's finding 1 is why this is a PR and not a first commit — +`pair.lua` is every language's auto-pairing, and a reviewer looking at a +Lean PR should not have to also review a rewrite of it. **The no-behavior-change claim must be pinned, not asserted.** The full `tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must @@ -1377,10 +1520,24 @@ file rather than estimated: | 305 keys that are proper prefixes of another | which keys can expand eagerly | | 1,550 keys uniquely-and-completely matching | the eager-expansion set | | 26 values containing `$CURSOR` | point placement | -| 93 multi-codepoint values | the replace is not one-char-for-many | +| 119 multi-codepoint symbols (26 of them `$CURSOR`-bearing) | the replace is not one-char-for-many | +| 101 prefixes with disagreeing equal-shortest ties | why the format carries source rank | + +(Rev 6 gave the multi-codepoint figure as 93, which was the count +*excluding* the `$CURSOR` entries — a subset reported as a total.) vscode-lean4 is Apache-2.0. +**Format: an ordered array, not a map.** §2.11's tie rule makes source +order semantic, and a Lua `{ [key] = symbol }` table iterated with +`pairs` cannot carry it. The generated file emits a **sequence** — +`{ {key, symbol}, ... }` in `abbreviations.json` order — plus a derived +`key → index` lookup built at load time for the exact-match case. +Resolution sorts candidates by `(#key, index)`, so the 101 ties resolve +the way upstream resolves them and the file's own line order is the +audit trail. A map-shaped emit would be nondeterministic across builds +and, once a hash order happened to be stable, *stably wrong*. + Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header recording source repo, commit, license, entry count, and the regeneration command — the `builtin/queries/latex/highlights.scm` @@ -1405,12 +1562,29 @@ so the file is self-describing to whoever next touches it. A refresh is an ordinary PR with a visible diff — which is the point: the diff is the review. -**The generator must reject a table it cannot faithfully encode.** Keys -are ASCII today but nothing upstream promises that; a key containing a -character the emitted Lua would have to escape, or a duplicate after -normalization, aborts the regeneration rather than silently emitting a -table that disagrees with its source. Same discipline as Q#LN20's -refusal to hand back a lossy path. +**Escaping is canonical and lossless, not a rejection trigger.** Rev 6 +said the generator aborts on "a key containing a character the emitted +Lua would have to escape." **That rule rejects the current table**: `\` +is a key, `"` begins eleven keys (`"A` → `Ä` …), and acceptance 45d +requires `\` to work. The generator instead emits every key and symbol +through one canonical Lua string escaper — `\\`, `\"`, `\n`, `\r`, +`\t`, and `\ddd` for any other control byte, everything else literal +UTF-8 — chosen so the emit is byte-deterministic across runs. + +What the generator *does* abort on, because these are real corruption +rather than syntax: + +- a duplicate key after decoding (JSON permits it; the table must not), +- a key or symbol that is not well-formed UTF-8, +- a round-trip mismatch: the generator re-parses its own output and + compares the full ordered sequence against the source, entry for + entry, and fails if they differ anywhere. + +That last check is what makes the artifact trustworthy, and it belongs +in the generator rather than in the acceptance suite — the suite cannot +see `abbreviations.json`, which is not shipped. Same discipline as +Q#LN20's refusal to hand back a lossy path: refuse rather than emit +something plausible. ### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it @@ -1466,23 +1640,54 @@ that an edit was made. reconstruction of it: - `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, - start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`. + window, start_offset, text = "" }`, keyed on **`(frontend, buffer)`** — + see below. - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. - If no key extends `text .. c`, expand `text` **first**, then let `c` land normally — the chain does *not* claim `c`. -- Expansion resolves through §2.11's three-rule `getReplacementText`, - including the suffix rule (`\alp7` → `α7`). +- **A terminating `c` that is itself `\` is then reprocessed as a new + leader**, opening a fresh pending abbreviation at its position. This + is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6 + specified the acceptance without specifying the rule; upstream gets it + from `processChange`, where a `finished` abbreviation reports + `isAffected = false` and so does not suppress the new-leader branch. + Note this is *not* the `\\` case: there the pending text is empty, `\` + extends rather than terminates, and the result is one literal + backslash with no pending state left open. +- Expansion resolves through §2.11's rules — shortest key wins, ties + broken by source rank, unmatchable tail appended (`\alp7` → `α7`). - `$CURSOR` is stripped from the symbol and its index becomes the point. +**Ownership is per frontend, not per buffer** (§2.11). The key is +`(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still +match `rec.window` for the state to be usable — a frontend that moved +the same buffer into a different window is no longer typing where the +pending span is. Two consequences the buffer-only design got wrong: + +- `buffer.after-switch` fires with **no arguments**, so it cannot say + whose switch it was. The subscriber reads `pmacs.frontend.id()` at + callback time — documented as "the frontend that produced the most + recent dispatched input event" — and clears **only that frontend's** + entries. A blanket clear would let one frontend's navigation discard + another's half-typed abbreviation. +- `frontend.detached` fires with the raw frontend id and is the purge + seam, exactly as `killring.lua` uses it (Q#KR11). Without it a + detached frontend's pending state leaks for the life of the session. + +This costs one table level and buys correctness in the ordinary +TUI-plus-GPU configuration, which is not an exotic setup — it is the +one this project ships two frontends for. + **Abandonment is lazy, because there is no cursor-motion hook** (round-5 finding 3). Pending state is validated at the next typed edit and -discarded when any of these no longer holds: the record's buffer is the -pending buffer; `rec.effective_start` equals `start_offset + 1 + -#text` (the point is still at the end of the pending span); and the -buffer's `revision()` advanced by exactly the pending edit. `buffer. -after-switch` clears it eagerly since that hook *does* exist. The +discarded when any of these no longer holds: the record's buffer and +window are the pending ones; `rec.effective_start` equals `start_offset ++ 1 + #text` (the point is still at the end of the pending span); and +the buffer's `revision()` advanced by exactly the pending edit. +`buffer.after-switch` clears the acting frontend's entries eagerly, +since that hook *does* exist. The practical difference from upstream: a user who clicks away mid-`\alp` and types elsewhere gets the pending state dropped rather than expanded. Upstream expands it. **This is a deliberate divergence** — expanding @@ -2138,6 +2343,11 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage. Per the no-renumbering rule above, round 5's additions take letter suffixes on both sides of the split. +46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which +is part of Stage 4a's declared footprint (Q#LN10) and a required gate +for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which +criterion 46 requires to stay byte-identical. + 46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs` suite passes **unmodified**. A suite edited to accommodate the refactor proves nothing; the diff for 4a must show zero lines @@ -2164,8 +2374,12 @@ suffixes on both sides of the split. **Stage 4b — the Unicode input method** -38. `\alpha` + space yields `α`; the whole expansion is a single undo - step, and one undo restores `\alpha` rather than `\alph`. +38. `\alpha` + space yields `α ` — the space lands first and the + expansion runs in the following `buffer.after-edit`, so the + terminator is **retained**, not consumed. The expansion is a single + undo step: one undo restores `\alpha ` (with its space), not + `\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be + true only if the terminator were swallowed. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. 40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is @@ -2211,6 +2425,14 @@ suffixes on both sides of the split. because the expansion is a programmatic replace that arms no record. Bites against a future consumer that infers pending state from buffer text instead of provenance. +45i. **Pending state is per frontend (Q#LN22).** Two frontends attached + to the same `lean4` buffer: A types `\al`, B types `\to` + space in + the same buffer. B's expansion yields `→` and leaves A's `\al` + pending and intact; A then typing `l` + space still yields `∀`. + Plus: B switching buffers does not clear A's pending state, and a + `frontend.detached` for B purges B's entries only. Bites against the + buffer-keyed design rev 6 specified — which passes every + single-frontend criterion above. 45f. **Both producers, and the CI-darkness stated.** The dispatch path is pinned by the criteria above. The optimistic CRDT producer (round-5 finding 4) is pinned by a separate criterion driving @@ -2222,11 +2444,30 @@ suffixes on both sides of the split. verified only locally and name the command. Silence here is the failure mode — a green CI would otherwise read as covering the path most users take. -45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips: - its entry count matches the header's declared count, and a spot set - of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches - `abbreviations.json` byte-for-byte. Bites against a generator that - silently drops or mangles keys (Q#LN11). +45g. **Table integrity — what the suite can actually check.** + `abbreviations.json` is not shipped, so the suite cannot diff + against it and rev 6's "matches byte-for-byte" was unbuildable; a + count plus seven spot entries could not prove 1,855 round-trip + anyway. The full source-fidelity check belongs to the generator + (Q#LN11: re-parse own output, compare the ordered sequence entry for + entry, fail on any difference). What the suite pins instead are + self-consistency properties that a corrupt emit breaks: + - the loaded sequence's length equals the header's declared count, + and equals the declared count for the recorded upstream commit; + - every key is unique, and the derived `key → index` lookup has the + same cardinality as the sequence (a collision would silently drop + entries); + - every key and symbol is well-formed UTF-8, and no symbol contains + `$CURSOR` more than once; + - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`, + `n`, `setminus`, and the tie cases from 45h. +45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` — + `f<` and `f>` are both length 2, and `f<` is declared first. Same + for `\"` + space → `Ä`, first of eleven equal-length candidates. + **This is the criterion that bites a map-shaped vendored table**: + with `pairs` iteration it passes or fails by hash order, so it must + also be run against a deliberately reversed sequence and shown to + fail. 101 prefixes are exposed to this rule. **Stage 5 — the goal view** @@ -2294,7 +2535,7 @@ suffixes on both sides of the split. discipline on transformed source edits, and Q#AP1's optimistic-classifier limitation. Stage 4a generalizes the first; 4b is built on all three. - **#127 (config registry)** — `pmacs.config.define` and the - source-buffer-resolution correction. Q#LN10's gate follows + source-buffer-resolution correction. Q#LN22's gate follows `editing.auto-pair` exactly. - **#129 (mode system)** — mode-scoped keymaps for Stage 5. - **#155 (bottom panel)** — `pmacs.window.display` and the panel adopter @@ -2381,9 +2622,10 @@ PR. (config registry) secondarily, by adding one option in the established shape rather than a new switch mechanism. -**Golden journey (§2).** No step is touched by 4a. 4b improves step 4 -(editing) for Lean specifically and changes nothing for any other -language: the pending-abbreviation state exists only in `lean4` buffers. +**Golden journey (§2).** No step is touched by 4a. 4b improves **step 5 +("Edit immediately")** for Lean specifically and changes nothing for any +other language — rev 6 cited step 4, which is "Understand the visible +interface" and is untouched by both stages: the pending-abbreviation state exists only in `lean4` buffers. Neither stage changes launch, open, or attach. **Interaction islands (§6).** **None added, and this is the load-bearing From 174e36fce384375b94c4c84af5a7a27f41e318da Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:49:43 -0400 Subject: [PATCH 09/14] docs(lean4): reconcile peer edits with pending ownership Advance the Stage 4 framing to revision 8. Keep pending abbreviation state frontend-owned while conservatively invalidating it after any intervening shared-buffer edit, make the revision token explicit, and rewrite acceptance 45i around that contract. Correct the active-work multi-codepoint count and the stale coherence revision label. --- docs/active-work.md | 18 ++++++++--- docs/lean4-mode-framing.md | 62 ++++++++++++++++++++++++++++++-------- 2 files changed, 63 insertions(+), 17 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 47c3677..cf4ea6e 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -64,17 +64,17 @@ If it does not, stop and repair the remote/fetch configuration. histories were pruned from this ledger in round 6, per this file's own instruction to remove entries when their PR merges; the durable facts now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where - a fresh machine should read them. `docs/lean4-mode-framing.md` rev 7 + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8 carries the decisions. -### Stage 4 — framing rev 7, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) - Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main that had advanced 50 commits mid-review; the only conflict either time was this ledger's own lane headings, resolved by keeping both sides. - Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. - Framing-only so far: `docs/lean4-mode-framing.md` **revision 7**. No + Framing-only so far: `docs/lean4-mode-framing.md` **revision 8**. No code. Awaiting user approval before implementation, per the workflow. - **Round 6 review found five P1s, four of them internal to rev 6** — facts about pmacs the revision asserted without checking, while its @@ -93,6 +93,15 @@ If it does not, stop and repair the remote/fetch configuration. the upstream package ships no README after fetching the package root, with the directory listing showing `src/README.md` already in hand. The README states the tie rule in one sentence. +- **Round 7 review found one remaining P1 in acceptance 45i.** Rev 7 + required A's pending abbreviation to survive B editing the same + buffer, while Q#LN22 also required an exact buffer-revision advance. + Those cannot both hold: revisions are buffer-global and every edit + bumps them. Rev 8 keeps the conservative guard and separates + ownership from survival — B cannot consume A's record, but B editing + the shared buffer invalidates A lazily; B switching buffers or + detaching remains frontend-scoped when no shared-buffer edit + intervenes. - **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).** 4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua` plus `pair.lua` re-expressed as one registered consumer, no behavior @@ -130,7 +139,8 @@ If it does not, stop and repair the remote/fetch configuration. - Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are proper prefixes of another (so 1,550 expand eagerly), **26** values - carry `$CURSOR`, **93** are multi-codepoint. + carry `$CURSOR`, and **119** are multi-codepoint — the 26 + `$CURSOR`-bearing values plus 93 others. - Citation sweep per COHERENCE §25: five live citations moved in the 50 commits since rev 5 — `take_typed_edit` 12827→12990, `handle_server_requests` 1549→1815, `fs.stat` 93→133, diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index ca50696..650b2f3 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. Current revision: **7**. +Revision 1 — initial. Current revision: **8**. ### Round 1 (rev 1 → rev 2) @@ -480,6 +480,29 @@ section cites golden-journey **step 5** ("Edit immediately"), not step 4; and §8's config-registry prior art points at Q#LN22, where the gate now lives. +### Round 7 (rev 7 → rev 8) + +One P1 remained in the new multi-frontend acceptance, plus two +documentation cleanups. + +1. **Acceptance 45i contradicted Q#LN22's conservative abandonment + rule.** It required frontend A's pending abbreviation to survive + frontend B editing the same buffer, but `buffer:revision()` is + buffer-global and advances on every edit. B's first edit therefore + invalidates A's record under the exact-revision guard. The criterion + now separates the two contracts: another frontend cannot consume A's + record, but any intervening edit to their shared buffer invalidates + it lazily; navigation and detachment remain frontend-scoped when no + shared-buffer edit intervenes. The pending record now names its + `expected_revision` explicitly so the validation rule is buildable. + Preserving A's record through peer edits would require translating + and validating its span across arbitrary edits, a substantially + larger substrate change that Stage 4b does not take on. +2. **The volatile ledger retained rev 6's undercount.** Its table facts + now say 119 multi-codepoint symbols — 26 `$CURSOR`-bearing and 93 + others — matching §2.11 and Q#LN11. +3. **§9.1's revision label was stale.** It now names rev 8. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1640,8 +1663,9 @@ that an edit was made. reconstruction of it: - `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, - window, start_offset, text = "" }`, keyed on **`(frontend, buffer)`** — - see below. + window, start_offset, text = "", expected_revision }`, keyed on + **`(frontend, buffer)`** — see below. `expected_revision` is the + buffer's revision after that leader edit. - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. @@ -1685,7 +1709,14 @@ finding 3). Pending state is validated at the next typed edit and discarded when any of these no longer holds: the record's buffer and window are the pending ones; `rec.effective_start` equals `start_offset + 1 + #text` (the point is still at the end of the pending span); and -the buffer's `revision()` advanced by exactly the pending edit. +the buffer's `revision()` equals `expected_revision + 1`, meaning the +current typed edit is the only edit since this frontend last extended +the pending abbreviation. A claimed extension stores the current +revision as the new `expected_revision`. This is deliberately +conservative across frontends: any intervening edit to the shared +buffer invalidates the pending record even if it occurred elsewhere. +Keeping the record alive would require translating and validating its +span through arbitrary peer edits, substrate Stage 4b does not add. `buffer.after-switch` clears the acting frontend's entries eagerly, since that hook *does* exist. The practical difference from upstream: a user who clicks away mid-`\alp` @@ -2425,14 +2456,19 @@ criterion 46 requires to stay byte-identical. because the expansion is a programmatic replace that arms no record. Bites against a future consumer that infers pending state from buffer text instead of provenance. -45i. **Pending state is per frontend (Q#LN22).** Two frontends attached - to the same `lean4` buffer: A types `\al`, B types `\to` + space in - the same buffer. B's expansion yields `→` and leaves A's `\al` - pending and intact; A then typing `l` + space still yields `∀`. - Plus: B switching buffers does not clear A's pending state, and a - `frontend.detached` for B purges B's entries only. Bites against the - buffer-keyed design rev 6 specified — which passes every - single-frontend criterion above. +45i. **Pending state is per frontend, with conservative shared-buffer + invalidation (Q#LN22).** Two frontends share a `lean4` buffer at + distinct points. A types `\al`; B types `p`. B's `p` lands normally + at B's point rather than extending A's record. Because that edit + advances the shared buffer's revision, A then typing `l` + space + leaves literal `\all ` rather than expanding: A's stale record is + abandoned lazily. In a fresh setup, A types `\al`, B switches + buffers **without editing the shared buffer**, and A typing `l` + + space still yields `∀`; B's switch clears only B's entries. Finally, + `frontend.detached` for B purges B's entries only and does not clear + a still-valid A record. Bites both against the buffer-keyed design + rev 6 specified and against the impossible rev-7 promise that + pending state survives arbitrary peer edits. 45f. **Both producers, and the CI-darkness stated.** The dispatch path is pinned by the criteria above. The optimistic CRDT producer (round-5 finding 4) is pinned by a separate criterion driving @@ -2615,7 +2651,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from languages other than Lean, and §4's rule is what keeps them out of a Lean PR. -### 9.1 Coherence impact — stages 4a and 4b (rev 6) +### 9.1 Coherence impact — stages 4a and 4b (rev 8) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 From 24ca9062944d639e4aa90c3567a9e67c4497e49b Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:00:03 -0400 Subject: [PATCH 10/14] feat(typed-edit): the typed-edit consumer chain (Arc 8 Stage 4a) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `pmacs.editor.take_typed_edit()` is one-shot and per-frontend (Q#AP9): the first `buffer.after-edit` callback to call it clears the slot, and every later callback in the same fan-out sees nil. That was survivable only because auto-pairing was the sole consumer — never a property anyone chose. A second independent caller would get nil or steal the record from pairing depending on hook registration order, and registration order is not a contract. This makes it one. `builtin/runtime/typed_edit.lua` owns the single after-edit subscriber that reads the record, and offers that one read to consumers registered through `pmacs.typed_edit.add_consumer{ name, priority, fn }`: lowest priority first, ties by registration order, and the first consumer to return truthy claims the edit and stops the chain. `pair.lua` becomes that chain's only consumer, at priority 100. No Lean content. Stage 4b's abbreviation expander is what needs the ordering guarantee (64 of its 1,855 keys contain a `lean4` pair-set character, so pairing running first corrupts them), but the chain is substrate every language runs through, which is why it ships alone — framing Q#LN10, and §4's rule that no PR in this arc mixes a cross-cutting substrate change with Lean feature content. Three design points worth review attention: - Consumers are called even when the record is nil. "This fan-out carried no typed edit" is information a consumer acts on: it is how pairing's test seam observes a non-event, and how Stage 4b will abandon a pending abbreviation an unrelated edit invalidated. Three existing auto-pairing tests fail if the chain skips consumers on nil. - The chain pcalls each consumer. `buffer.after-edit` is all-must-succeed, so a throwing consumer would otherwise fail the fan-out for every other subscriber, including lsp.lua's didChange flush. Behavior-preserving for pairing, which already never throws. - Ordered insertion, not `table.sort`, which is not stable in Lua — "ties by registration order" is a stated contract, not a coincidence. `tests/auto_pair_acceptance.rs` is UNCHANGED — zero lines — and its 45 tests pass. That is criterion 46 and the whole no-behavior-change claim; a suite edited to accommodate the refactor would prove nothing. `tests/typed_edit_chain_acceptance.rs` adds 9 tests for criteria 46a-46e. Every one is bite-verified by mutation: appending instead of ordered insert (5 fail), `>=` for the tiebreak (1), re-taking per consumer (4), ignoring the claim (1), dropping the pcall (1), skipping nil fan-outs (1 here plus 3 in the untouched auto-pair suite), and loading the chain after lsp.lua (the Q#AP7 flush test fails, alongside the two existing pairing ones). Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/pair.lua | 85 +++-- builtin/runtime/typed_edit.lua | 112 ++++++ src/editor.rs | 15 + tests/typed_edit_chain_acceptance.rs | 517 +++++++++++++++++++++++++++ 4 files changed, 699 insertions(+), 30 deletions(-) create mode 100644 builtin/runtime/typed_edit.lua create mode 100644 tests/typed_edit_chain_acceptance.rs diff --git a/builtin/runtime/pair.lua b/builtin/runtime/pair.lua index 9ed9d1f..5869dce 100644 --- a/builtin/runtime/pair.lua +++ b/builtin/runtime/pair.lua @@ -4,20 +4,30 @@ -- next char is already `)` steps over it instead of doubling it. The -- carrier is a `buffer.after-edit` reaction (Q#AP1): the opener stays -- a genuine single-codepoint self-insert — the classification --- signature help depends on — and this hook inserts (or swallows) the --- closer as a second edit. Provenance is the exact one-shot typed-edit --- record (`pmacs.editor.take_typed_edit()`, Q#AP9), not buffer-text --- inference: pastes, programmatic edits, manual hook runs, and a stale --- `this_command` have no record and never pair, and a transformed, --- relocated, or context-switching source self-insert fails closed. +-- signature help depends on — and this reaction inserts (or swallows) +-- the closer as a second edit. Provenance is the exact one-shot +-- typed-edit record (`pmacs.editor.take_typed_edit()`, Q#AP9), not +-- buffer-text inference: pastes, programmatic edits, manual hook runs, +-- and a stale `this_command` have no record and never pair, and a +-- transformed, relocated, or context-switching source self-insert fails +-- closed. -- --- This chunk loads BEFORE lsp.lua (Q#AP7): registration order is hook --- execution order, and lsp.lua's after-edit callback synchronously --- flushes didChange on the signature-trigger path — the closer must --- already be in the buffer when that callback runs. Everything under --- `pmacs.lsp` is therefore looked up lazily at callback time. +-- Since Arc 8 Stage 4a (Q#LN10) pairing no longer subscribes to +-- `buffer.after-edit` itself. It registers on the typed-edit chain +-- (`builtin/runtime/typed_edit.lua`), which owns the single subscriber +-- and the single one-shot read. Everything above still holds — the +-- record is the same record — but the chain, not this file, decides +-- who sees it and in what order. -- --- Framing: docs/auto-pairing-framing.md. +-- This chunk loads AFTER typed_edit.lua (it registers into it) and +-- BEFORE lsp.lua (Q#AP7): registration order is hook execution order, +-- and lsp.lua's after-edit callback synchronously flushes didChange on +-- the signature-trigger path — the closer must already be in the +-- buffer when that callback runs. Everything under `pmacs.lsp` is +-- therefore looked up lazily at callback time. +-- +-- Framing: docs/auto-pairing-framing.md; Stage 4a in +-- docs/lean4-mode-framing.md Q#LN10. pmacs.pair = pmacs.pair or {} @@ -40,7 +50,7 @@ local ed = pmacs.editor -- Per-buffer on/off switch (Q#CR8's flagship adopter). Read against the -- SOURCE buffer of the typed edit, never the currently active one — see --- the hook body below, which resolves it the same way `set_for` resolves +-- the consumer body below, which resolves it the same way `set_for` resolves -- the buffer's pair set (round 2, finding 2): `rec.buffer`, not -- `pmacs.window.buffer()`. pmacs.config.define { @@ -214,28 +224,36 @@ end -- Acceptance tests flip `_capture_records` on; each fan-out then -- publishes the record it observed (or nil) to `_last_record`, which -- is how tests read the exact codepoint / effective triple and prove --- one-shot-ness (this callback registers first and consumes it). +-- one-shot-ness (the chain takes the record before any other +-- `buffer.after-edit` subscriber can, and hands it here). pmacs.pair._capture_records = false -pmacs.hook.add("buffer.after-edit", function() +-- The typed-edit consumer (Arc 8 Stage 4a, Q#LN10). `rec` is the one +-- record `typed_edit.lua` read for this fan-out — possibly nil, which +-- is why the capture seam below is updated before the nil guard. +-- Returns whether pairing CLAIMED the keystroke: true once it has +-- committed to reacting (a skip-over or a closer insert, landed or +-- intercept-rejected), false on every decline. Pairing is last of the +-- builtin consumers, so nothing currently observes that value; it is +-- stated correctly so it stays correct when something does. +local function on_typed_edit(rec) -- One-shot provenance (Q#AP9). Absence — paste, programmatic edit, -- manual hook run, rejected insert, a post-insert mutation by the -- command, stale `this_command` — is a silent non-event; only a -- live record for a pair-set character that then fails a gate -- reports. - local rec = ed.take_typed_edit and ed.take_typed_edit() if pmacs.pair._capture_records then pmacs.pair._last_record = rec end - if not rec then return end - if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return end + if not rec then return false end + if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return false end -- The master switch, per-buffer (Q#CR4): the SOURCE buffer of the -- typed edit, resolved buffer-local -> global -> default(true). A -- second buffer of the same language is untouched by a buffer-local -- override here (acceptance 29). - if not pmacs.config.get("editing.auto-pair", rec.buffer) then return end + if not pmacs.config.get("editing.auto-pair", rec.buffer) then return false end local buf = pmacs.window.buffer() - if not buf then return end + if not buf then return false end -- Relevance first (PR #110 round 1, finding 2): pairing has no -- interest in characters outside the set, so a transformed or @@ -247,14 +265,14 @@ pmacs.hook.add("buffer.after-edit", function() -- Rust. local ch = rec.char local openers, closers = maps_for(set_for(rec.buffer)) - if not (openers[ch] or closers[ch]) then return end + if not (openers[ch] or closers[ch]) then return false end -- Fail closed on a transformed source self-insert (Q#AP3): the -- intercept's positional result stands as produced; pairing on top -- of a relocated or expanded opener would compound it. if not rec.clean then ed.set_status("auto-pair skipped: source self-insert transformed") - return + return false end -- Fail closed when the source edit's context is no longer current: -- an intercept switched window/buffer, or something moved the @@ -268,14 +286,14 @@ pmacs.hook.add("buffer.after-edit", function() or pmacs.window.current() ~= rec.window or ed.cursor() ~= rec.post_cursor then ed.set_status("auto-pair skipped: source context changed") - return + return false end -- Region guard (Q#AP3/Q#AP6): on the dispatch route type-over has -- already consumed and cleared the region. A region surviving the -- edit means the TUI's selection-blind optimistic gate let a custom -- pair char through (named deferral) — reacting would pile a closer -- onto an unconsumed region. - if ed.region() ~= nil then return end + if ed.region() ~= nil then return false end local cursor = rec.post_cursor @@ -294,19 +312,19 @@ pmacs.hook.add("buffer.after-edit", function() if not ok then -- The duplicate stays (e.g. `())`); report, no retry. ed.set_status("auto-pair skip rejected by buffer intercept") - return + return true end if estart ~= cursor or estop ~= cursor + #ch or einserted ~= 0 then ed.set_status("auto-pair skip altered by buffer intercept") repair_cursor(win0, buf, cursor, estart, estop, einserted) end - return + return true end end local closer = openers[ch] - if not closer then return end - if not should_pair(buf, cursor, closers) then return end + if not closer then return false end + if not should_pair(buf, cursor, closers) then return false end local win0 = pmacs.window.current() local ok, estart, estop, einserted = pcall(function() @@ -315,7 +333,7 @@ pmacs.hook.add("buffer.after-edit", function() if not ok then -- Nothing landed; the opener stands alone. ed.set_status("auto-pair closer rejected by buffer intercept") - return + return true end if estart ~= cursor or estop ~= cursor or einserted ~= #closer then ed.set_status("auto-pair closer altered by buffer intercept") @@ -324,4 +342,11 @@ pmacs.hook.add("buffer.after-edit", function() -- Clean path: no cursor motion — the insert landed at the cursor -- and Lua mutators move no cursors, so it already sits between the -- pair; the daemon's per-tick CursorByte re-grounds both frontends. -end) + return true +end + +pmacs.typed_edit.add_consumer { + name = "auto-pair", + priority = 100, + fn = on_typed_edit, +} diff --git a/builtin/runtime/typed_edit.lua b/builtin/runtime/typed_edit.lua new file mode 100644 index 0000000..59f7366 --- /dev/null +++ b/builtin/runtime/typed_edit.lua @@ -0,0 +1,112 @@ +-- typed_edit.lua --- the typed-character consumer chain (Arc 8 Stage 4a). +-- +-- `pmacs.editor.take_typed_edit()` is ONE-SHOT and per-frontend (Q#AP9): +-- the first `buffer.after-edit` callback to call it clears the slot, and +-- every later callback in the same fan-out --- including a nested manual +-- `pmacs.hook.run` --- sees nil. That was survivable only because +-- auto-pairing was the sole consumer, which was never a property anyone +-- chose. A second independent caller gets nil or steals the record from +-- pairing depending on hook registration order, and registration order +-- is not a contract. +-- +-- This module makes it one. It owns the single `buffer.after-edit` +-- subscriber that reads the record, and offers that one read to +-- consumers registered through `pmacs.typed_edit.add_consumer`: +-- +-- pmacs.typed_edit.add_consumer { +-- name = "auto-pair", -- for error reporting; must be unique-ish +-- priority = 100, -- LOWEST runs FIRST +-- fn = function(rec) ... return claimed end, +-- } +-- +-- A consumer returns whether it CLAIMED the edit; the first that claims +-- stops the chain. "Claimed" means the chain stops, not that an edit was +-- made --- Stage 4b's abbreviation expander claims every keystroke that +-- extends a pending abbreviation precisely so that auto-pairing does not +-- also react to it (Q#LN22). +-- +-- Priority is an explicit number rather than load-order-implied, because +-- the ordering is load-bearing (Q#LN22: 64 Lean abbreviation keys +-- contain a character in the `lean4` pair set, and pairing running first +-- corrupts them) and a reader must be able to check it without +-- reconstructing `src/editor.rs`'s include list. +-- +-- ORDERING CONTRACT: this chunk loads BEFORE pair.lua, which registers +-- into it, and therefore before lsp.lua. That preserves Q#AP7 --- see +-- pair.lua's header and the load site in `src/editor.rs`. +-- +-- Framing: docs/lean4-mode-framing.md Q#LN10. + +pmacs.typed_edit = pmacs.typed_edit or {} + +-- Consumers in run order: lowest `priority` first, registration order +-- breaking ties. Maintained by ordered INSERTION rather than +-- `table.sort`, which is not stable in Lua --- equal priorities would +-- otherwise resolve arbitrarily, and "ties broken by registration +-- order" is part of the stated contract, not an incidental property. +local consumers = {} + +-- Register a typed-edit consumer. Argument errors throw: registration +-- happens at chunk-load or config-load time, where a throw is a visible +-- startup failure rather than a silently missing feature. Nothing in +-- the after-edit path throws --- see the fan-out below. +function pmacs.typed_edit.add_consumer(spec) + if type(spec) ~= "table" then + error("pmacs.typed_edit.add_consumer: spec must be a table", 2) + end + local name, priority, fn = spec.name, spec.priority, spec.fn + if type(name) ~= "string" or name == "" then + error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2) + end + if type(priority) ~= "number" then + error("pmacs.typed_edit.add_consumer: " .. name .. + ": priority must be a number", 2) + end + if type(fn) ~= "function" then + error("pmacs.typed_edit.add_consumer: " .. name .. + ": fn must be a function", 2) + end + + -- STRICTLY-greater comparison, so a new consumer lands AFTER every + -- already-registered consumer of equal priority. That is exactly the + -- registration-order tiebreak; `>=` here would silently reverse it. + local at = #consumers + 1 + for i, c in ipairs(consumers) do + if c.priority > priority then + at = i + break + end + end + table.insert(consumers, at, { name = name, priority = priority, fn = fn }) +end + +pmacs.hook.add("buffer.after-edit", function() + local ed = pmacs.editor + -- ONE read for the whole fan-out (Q#AP9). The record may be nil --- + -- paste, programmatic mutation, manual hook run, a replicated CRDT + -- op, a stale `this_command` --- and consumers are called ANYWAY, + -- with nil. That is deliberate: "this fan-out carried no typed edit" + -- is information a consumer acts on. Auto-pairing's test seam + -- observes the non-event through it, and Stage 4b abandons a pending + -- abbreviation that an unrelated edit invalidated. Skipping the + -- fan-out on nil would leave both reading stale state. + local rec = ed.take_typed_edit and ed.take_typed_edit() + + for _, c in ipairs(consumers) do + -- `buffer.after-edit` is all-must-succeed (builtin/hooks/default.lua): + -- a throwing consumer would fail the fan-out for every OTHER + -- subscriber, including lsp.lua's didChange flush. Contain it, + -- report it, and keep going --- a broken consumer must not be able + -- to stop the editor from telling the language server what changed. + -- This matches pair.lua's existing never-throw-from-after-edit + -- discipline; it does not weaken the hook's contract for anyone + -- else, because the chain itself still never fails. + local ok, claimed = pcall(c.fn, rec) + if not ok then + ed.set_status("typed-edit consumer '" .. c.name .. "' failed: " .. + tostring(claimed)) + elseif claimed then + return + end + end +end) diff --git a/src/editor.rs b/src/editor.rs index dcff55a..673ded6 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -415,6 +415,18 @@ impl EditorState { include_str!("../builtin/runtime/listview.lua"), ) .expect("load listview builtin chunk"); + // The typed-edit consumer chain (Arc 8 Stage 4a, Q#LN10) — + // ORDERING CONTRACT: typed_edit.lua must load BEFORE pair.lua, + // which registers a consumer into it, and therefore before + // lsp.lua. It owns the single `buffer.after-edit` subscriber + // that reads the one-shot typed-edit record, so its + // registration position is what preserves Q#AP7 below. + lua_host + .eval( + Some("@pmacs/builtin/runtime/typed_edit.lua"), + include_str!("../builtin/runtime/typed_edit.lua"), + ) + .expect("load typed_edit builtin chunk"); // Auto-pairing (Arc 2, Q#AP7) — ORDERING CONTRACT: pair.lua // must load BEFORE lsp.lua. Hook callbacks run in registration // order, and lsp.lua's `buffer.after-edit` callback flushes @@ -424,6 +436,9 @@ impl EditorState { // the closer stays unsynchronized until the next edit (hook // edits don't re-fire the hook). pair.lua's `pmacs.lsp.*` // lookups are lazy and nil-guarded for the same reason. + // Since Stage 4a the closer is inserted from the chain's + // subscriber rather than pair.lua's own, which is registered + // one chunk earlier — strictly safer for this contract. lua_host .eval( Some("@pmacs/builtin/runtime/pair.lua"), diff --git a/tests/typed_edit_chain_acceptance.rs b/tests/typed_edit_chain_acceptance.rs new file mode 100644 index 0000000..c0170f4 --- /dev/null +++ b/tests/typed_edit_chain_acceptance.rs @@ -0,0 +1,517 @@ +//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a, +//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46e). +//! +//! The chain owns the single `buffer.after-edit` subscriber that reads +//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in +//! priority order. These tests pin the chain's OWN behavior — take-once, +//! priority ordering, claim-stops-chain, throw containment, and the +//! Q#AP7 flush ordering it inherited from `pair.lua`. +//! +//! They deliberately do not re-test auto-pairing: criterion 46 requires +//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that +//! suite is the no-behavior-change pin. Pairing appears here only as +//! the chain's last consumer, which is how 46c observes that a claim +//! really stopped the chain. +//! +//! Dispatch-driven throughout: `dispatch_key` is the producer that arms +//! the record for a grid frontend. + +use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; +use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; +use pmacs::protocol::FrontendId; +use std::path::PathBuf; +use std::sync::atomic::{AtomicUsize, Ordering}; +use std::time::{Duration, Instant}; + +fn fresh_state_dir() -> PathBuf { + static SEQ: AtomicUsize = AtomicUsize::new(0); + let dir = std::env::temp_dir().join(format!( + "pmacs-typededit-{}-{}", + std::process::id(), + SEQ.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir_all(&dir).unwrap(); + dir +} + +fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent { + KeyEvent { + code, + modifiers: mods, + kind: KeyEventKind::Press, + state: KeyEventState::NONE, + } +} + +fn type_str(s: &mut EditorState, text: &str) { + for ch in text.chars() { + s.dispatch_key( + FrontendId::LOCAL, + key(KeyCode::Char(ch), KeyModifiers::NONE), + ); + } +} + +fn exec(s: &EditorState, src: &str) { + s.lua_host.lua().load(src.to_string()).exec().unwrap(); +} + +fn eval(s: &EditorState, src: &str) -> T { + s.lua_host.lua().load(src.to_string()).eval().unwrap() +} + +fn buffer_text(s: &EditorState) -> String { + let b: mlua::String = eval( + s, + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ); + String::from_utf8_lossy(&b.as_bytes()).into_owned() +} + +fn status(s: &EditorState) -> String { + s.core.borrow().status.clone() +} + +/// Fresh scratch-buffer editor, cursor at 0. Scratch pairing uses the +/// `default` set, so `(` pairs — which is what 46c reads. +fn editor_with(body: &str) -> EditorState { + let s = EditorState::new(); + if !body.is_empty() { + exec(&s, &format!("pmacs.window.buffer():insert(0, {body:?})")); + } + exec(&s, "pmacs.editor.goto_byte(0)"); + s +} + +// --------------------------------------------------------------------------- +// 46a — one read for the whole fan-out +// --------------------------------------------------------------------------- + +#[test] +fn chain_reads_the_record_once_and_hands_the_same_one_to_every_consumer() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.seen = {} + local function spy(tag) + return function(rec) + -- Each consumer independently attempts its own take. Under + -- the pre-chain design this is exactly what a second + -- consumer would have done, and exactly what would have + -- returned nil (or stolen the record from pairing). + local own = pmacs.editor.take_typed_edit() + _G.seen[#_G.seen + 1] = { + tag = tag, + char = rec and rec.char, + post_cursor = rec and rec.post_cursor, + clean = rec and rec.clean, + own_take_was_nil = (own == nil), + } + return false + end + end + pmacs.typed_edit.add_consumer { name = "spy-a", priority = 1, fn = spy("a") } + pmacs.typed_edit.add_consumer { name = "spy-b", priority = 2, fn = spy("b") } + "#, + ); + + type_str(&mut s, "x"); + + let (n, a_char, b_char, a_pc, b_pc, a_clean, b_clean, a_nil, b_nil): ( + i64, + String, + String, + i64, + i64, + bool, + bool, + bool, + bool, + ) = eval( + &s, + " + local a, b = _G.seen[1], _G.seen[2] + return #_G.seen, a.char, b.char, a.post_cursor, b.post_cursor, + a.clean, b.clean, a.own_take_was_nil, b.own_take_was_nil + ", + ); + + assert_eq!(n, 2, "both consumers ran for one typed character"); + // The same record, not two reads of a slot that only one could win. + assert_eq!(a_char, "x"); + assert_eq!(b_char, "x", "the second consumer sees the record too"); + assert_eq!((a_pc, b_pc), (1, 1), "identical post_cursor"); + assert!(a_clean && b_clean, "identical clean verdict"); + // ...and the chain, not the consumers, did the taking. + assert!( + a_nil && b_nil, + "a consumer's own take_typed_edit() observes nil — the chain \ + already consumed the one-shot slot (Q#AP9)" + ); +} + +#[test] +fn consumers_run_when_the_fan_out_carries_no_record() { + // The chain calls consumers with nil rather than skipping them. + // Three tests in the auto-pairing suite depend on this (they assert + // `_last_record == nil` after a record-less fan-out), so it is a + // load-bearing decision and not an implementation detail. + let s = editor_with(""); + exec( + &s, + r#" + _G.calls, _G.nil_calls = 0, 0 + pmacs.typed_edit.add_consumer { + name = "nil-spy", priority = 1, + fn = function(rec) + _G.calls = _G.calls + 1 + if rec == nil then _G.nil_calls = _G.nil_calls + 1 end + return false + end, + } + "#, + ); + + // A manual fan-out arms no record. + exec(&s, "pmacs.hook.run(\"buffer.after-edit\")"); + + let (calls, nil_calls): (i64, i64) = eval(&s, "return _G.calls, _G.nil_calls"); + assert_eq!(calls, 1, "the consumer ran"); + assert_eq!(nil_calls, 1, "and was handed nil, not skipped"); +} + +// --------------------------------------------------------------------------- +// 46b — priority order, not registration order +// --------------------------------------------------------------------------- + +#[test] +fn consumers_run_in_priority_order_not_registration_order() { + let mut s = editor_with(""); + // Registered HIGH priority first. If the chain honored registration + // order (or `include_str!` order, which is the same failure dressed + // differently), the observed order would be the registration order. + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + pmacs.typed_edit.add_consumer { name = "late", priority = 30, fn = mark("late") } + pmacs.typed_edit.add_consumer { name = "early", priority = 10, fn = mark("early") } + pmacs.typed_edit.add_consumer { name = "mid", priority = 20, fn = mark("mid") } + "#, + ); + + type_str(&mut s, "x"); + + let order: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + order, "early,mid,late", + "lowest priority runs first, regardless of when it registered" + ); +} + +#[test] +fn equal_priorities_break_by_registration_order() { + // The stated tiebreak. Lua's `table.sort` is not stable, so this + // bites an implementation that sorts instead of inserting in place. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + pmacs.typed_edit.add_consumer { name = "first", priority = 5, fn = mark("first") } + pmacs.typed_edit.add_consumer { name = "second", priority = 5, fn = mark("second") } + pmacs.typed_edit.add_consumer { name = "third", priority = 5, fn = mark("third") } + "#, + ); + + type_str(&mut s, "x"); + + let order: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!(order, "first,second,third"); +} + +// --------------------------------------------------------------------------- +// 46c — a claim stops the chain +// --------------------------------------------------------------------------- + +#[test] +fn a_claiming_consumer_stops_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "claimer", priority = 1, fn = function() return true end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(!later_ran, "a later consumer must not run after a claim"); + // Pairing is the chain's last consumer at priority 100, so the + // claim is observable in the buffer: no closer was inserted. This + // is the assertion that makes the criterion about behavior rather + // than about a bookkeeping flag. + assert_eq!( + buffer_text(&s), + "(", + "auto-pairing never ran, so the opener stands alone" + ); +} + +#[test] +fn a_non_claiming_consumer_does_not_stop_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "passer", priority = 1, fn = function() return false end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(later_ran, "a declining consumer passes the edit along"); + assert_eq!( + buffer_text(&s), + "()", + "and pairing, still last in the chain, reacted normally" + ); +} + +// --------------------------------------------------------------------------- +// 46d — a throwing consumer is contained +// --------------------------------------------------------------------------- + +#[test] +fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "boom", priority = 1, + fn = function() error("consumer exploded") end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + // `buffer.after-edit` is all-must-succeed: an uncontained throw + // would fail the fan-out for every other subscriber, including + // lsp.lua's didChange flush. + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(later_ran, "a throwing consumer must not stop the chain"); + assert_eq!( + buffer_text(&s), + "()", + "and pairing still ran — the fan-out survived the throw" + ); + let st = status(&s); + assert!( + st.contains("boom") && st.contains("consumer exploded"), + "the failure is reported by consumer name and message, got {st:?}" + ); +} + +#[test] +fn add_consumer_rejects_malformed_registrations() { + let s = editor_with(""); + for (src, want) in [ + ( + "pmacs.typed_edit.add_consumer(\"nope\")", + "spec must be a table", + ), + ( + "pmacs.typed_edit.add_consumer{ priority = 1, fn = function() end }", + "name must be a non-empty string", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }", + "priority must be a number", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }", + "fn must be a function", + ), + ] { + let err = s + .lua_host + .lua() + .load(src.to_string()) + .exec() + .expect_err("malformed registration must throw"); + let msg = err.to_string(); + assert!( + msg.contains(want), + "expected {want:?} in the error for {src:?}, got {msg:?}" + ); + } +} + +// --------------------------------------------------------------------------- +// 46e — the Q#AP7 flush ordering the chain inherited +// --------------------------------------------------------------------------- + +fn fake_lsp_path() -> String { + env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned() +} + +fn pump_lua_flag(state: &mut EditorState, flag: &str, secs: u64) -> bool { + let deadline = Instant::now() + Duration::from_secs(secs); + loop { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + let done: bool = state + .lua_host + .lua() + .load(format!("return ({flag}) == true")) + .eval() + .unwrap_or(false); + if done { + return true; + } + if Instant::now() >= deadline { + return false; + } + std::thread::sleep(Duration::from_millis(10)); + } +} + +/// The `text` of every `textDocument/didChange` line in the sink, in +/// arrival order. +fn did_change_texts(sink: &std::path::Path) -> Vec { + let Ok(raw) = std::fs::read_to_string(sink) else { + return Vec::new(); + }; + raw.lines() + .filter_map(|l| serde_json::from_str::(l).ok()) + .filter(|v| v.get("method").and_then(|m| m.as_str()) == Some("textDocument/didChange")) + .filter_map(|v| v.get("text").and_then(|t| t.as_str()).map(str::to_owned)) + .collect() +} + +#[test] +fn a_chain_consumers_edit_reaches_the_first_did_change() { + // Q#AP7 generalized from pairing to the chain: lsp.lua's after-edit + // callback flushes didChange SYNCHRONOUSLY on the signature-trigger + // path, so every reaction to a typed character must already be in + // the buffer when it runs. The auto-pairing suite pins this for + // pairing; this pins it for the chain itself, which is what now + // owns the registration position. + // + // Falsified by loading typed_edit.lua after lsp.lua in + // `src/editor.rs`: the consumer's text would then arrive in the + // SECOND didChange, or not at all. + let dir = fresh_state_dir(); + let sink = dir.join("changes.jsonl"); + let sink_disp = sink.display().to_string(); + let fake = fake_lsp_path(); + + let mut s = EditorState::new(); + s.lua_host.lua().remove_app_data::(); + s.lua_host.lua().set_app_data(StateDir(dir.clone())); + exec(&s, "pmacs.lsp.config = {}"); + exec( + &s, + &format!( + "pmacs.lsp.config.rust = {{ + command = '{fake}', + env = {{ + PMACS_FAKE_LSP_MODE = 'sighelp', + PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}', + }}, + }}" + ), + ); + + // A consumer that appends a marker of its own, ahead of pairing. + // It declines the claim so pairing still runs — the assertion is + // about ordering against the flush, not about claiming. + exec( + &s, + r#" + pmacs.typed_edit.add_consumer { + name = "marker", priority = 1, + fn = function(rec) + if not rec then return false end + if rec.char ~= "(" then return false end + local buf = pmacs.window.buffer() + buf:insert(buf:len(), "Z") + return false + end, + } + "#, + ); + + let f = dir.join("a.rs"); + std::fs::write(&f, "\n").unwrap(); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let initialized = "(function() \ + for _,r in ipairs(pmacs.lsp.list()) do \ + if r.state and r.state.kind=='initialized' then return true end \ + end \ + return false \ + end)()"; + assert!(pump_lua_flag(&mut s, initialized, 5), "fake server init"); + + type_str(&mut s, "("); + assert_eq!( + buffer_text(&s), + "()\nZ", + "both the chain consumer's marker and pairing's closer landed" + ); + + let deadline = Instant::now() + Duration::from_secs(5); + let changes = loop { + s.tick_processes(); + s.tick_lsp(); + s.tick_async(); + let c = did_change_texts(&sink); + if !c.is_empty() { + break c; + } + assert!( + Instant::now() < deadline, + "no didChange reached the fake server" + ); + std::thread::sleep(Duration::from_millis(10)); + }; + assert_eq!( + changes[0], "()\nZ", + "the FIRST didChange carries BOTH reactions — the chain ran \ + before lsp.lua's synchronous flush (Q#AP7)" + ); +} From c7072b49e9e7ef427fd449100aa3d3ed5b70f80a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:05:41 -0400 Subject: [PATCH 11/14] docs: record the Stage 4a lane and its bite table Verification describes the pushed tree, per the standing rule. Includes the bite that was worthless as first written: moving only typed_edit.lua past lsp.lua broke the runtime load instead of testing flush ordering. A bite that kills everything has not isolated anything. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 56 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 53 insertions(+), 3 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index cf4ea6e..bd0c0b1 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -57,7 +57,7 @@ git status --short --branch The `git log` command must expose `d152120` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING +## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4a IN REVIEW - **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full @@ -146,8 +146,58 @@ If it does not, stop and repair the remote/fetch configuration. `handle_server_requests` 1549→1815, `fs.stat` 93→133, `detect_buffer_language` 452→457, `send_request`/`send_notification` 9342/9361→9507/9527. -- Verification: none yet — the branch carries no code. `git diff --check` - clean. +### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) + +- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` + (new, 112 lines), `pair.lua` re-expressed as one consumer, + `src/editor.rs` +15 (the `include_str!` and its ordering comment), and + `tests/typed_edit_chain_acceptance.rs` (new, 9 tests). + **`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat + main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is + criterion 46 checked at the diff, which is the only way it means + anything. +- **The chain calls consumers even when the record is nil.** This is a + decision, not an implementation detail: three existing auto-pairing + tests assert `pmacs.pair._last_record == nil` after a record-less + fan-out (paste, programmatic insert, nested manual `hook.run`), so + skipping consumers on nil fails them. Stage 4b needs the same + delivery to abandon a pending abbreviation an unrelated edit + invalidated. +- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and + "ties broken by registration order" is a stated contract. +- **The chain `pcall`s each consumer** and reports through + `set_status`. `buffer.after-edit` is all-must-succeed, so an + uncontained throw fails the fan-out for every other subscriber + including lsp.lua's didChange flush. +- **Every acceptance test is bite-verified by mutation**, per the + standing rule that a test is not evidence until the mutation it + targets has been shown to fail it: + + | Mutation | Tests it fails | + |---|---| + | append instead of ordered insert | 5 chain | + | `>=` instead of `>` in the insert scan | 1 chain (tiebreak) | + | re-take the record per consumer | 4 chain | + | ignore the claim return value | 1 chain | + | drop the `pcall` | 1 chain | + | skip consumers when `rec == nil` | 1 chain + **3 auto-pair** | + | load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) | + + The first attempt at the last bite was WORTHLESS as written: moving + only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil + `add_consumer`, so the runtime failed to load and all 9 tests died — + loud, but not a test of the flush-ordering property. Moving + `typed_edit.lua` AND `pair.lua` past `lsp.lua` is the faithful + falsification: registration succeeds, the hook lands late, and exactly + the three ordering tests fail. **A bite that kills everything has not + isolated anything.** +- Verification on this branch (commit-then-gate, so this describes the + pushed tree): `cargo fmt --check` clean; strict workspace Clippy + clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45; + typed-edit chain 9/9; M4 121; required GPU 202; **isolated-config + workspace sweep 3,328 across 97 suites, zero failures** with + `grep -c basedpyright` = 0; `git diff --check` clean. +- Stage 4b (the input method) is NOT in this PR and not started. ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) From 842417200a24802b6caabccdc1bd7967af98f5fd Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:18:05 -0400 Subject: [PATCH 12/14] fix(panel): close Stage 2A review round 3 (2 P1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **P1-1 — layout invalidation could suppress the authoritative clear.** Real bug. Both render paths resolved the document identity AFTER the evaluator ran callbacks, but BOTH outcome arms carry PHASE-1 contexts. A provider that closes the primary document split changes `primary_document_window` mid-evaluation, so the filter compared phase-1 contexts against a replacement identity, matched nothing, and emitted no clear — leaving stale statusline text on the wire forever. The identity is now captured BEFORE `evaluate_statusline` runs and threaded through both paths (the terminal path via `terminal_chrome`). Pinning it took three attempts, and the two failures are the useful part: - `pmacs.window.close()` takes no argument — it closes the ACTIVE window. The first version passed a window id that was silently ignored, so it closed the panel instead of the document. - The Lua window API acts on the ACTIVE FRONTEND, so driving it against a synthetic semantic view changed nothing at all. - Closing the only document window is structurally REFUSED (Q#BP6 forbids a lone side window as a resting state), so the fixture needs TWO document windows for the close to be legal. The test now asserts its own precondition — that the callback really changed the identity — before asserting the clear, and reproduces the reported symptom (no `StatuslineSegments` at all) when the fix is reverted. **P1-2 — #21 was pinned at the helper, not the producer.** Confirmed: reverting only the call site inside `publish_buffer_snapshot_to_replicas` left both the helper test and the existing socket-pair test green. The helper assertions are removed (with a note saying why) and replaced by `snapshot_publication_follows_the_document_under_a_focused_panel`, which drives the real producer over socket pairs and asserts BOTH directions: the document buffer's snapshot is delivered while a panel holds focus, and a panel-only buffer's is not. Biting that test exposed a defect in the test itself: the delivery read had no timeout, so a regression made it HANG rather than fail. A hanging test is strictly worse than a red one — every read now has a timeout. Gates: fmt clean; workspace clippy clean; 1,832 default + 2,015 CRDT library; Stage 2A 17; Stage 1 46; statusline 8; m11_5 2; GPU initial target 14; terminal config 12; folding Stage 2 48; vterm 1/2 10 / 6; M4 121; required GPU 202; `git diff --check` clean. Co-Authored-By: Claude Opus 5 (1M context) --- docs/active-work.md | 13 ++- src/daemon.rs | 106 +++++++++++++++++++-- src/semantic_render.rs | 53 ++++++++--- tests/bottom_panel_stage2a_acceptance.rs | 112 +++++++++++++++++++++++ 4 files changed, 259 insertions(+), 25 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 36a99de..a46a908 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -494,14 +494,14 @@ implemented and in review.** #173 also changes `src/editor.rs`, so gates were rerun on the merge result, not the old combination). Five commits: the classified census routing, the painter extraction + acceptance, the lane record, then - the round-1 and round-2 review fixes. **No protocol change; no behavior + the round-1, round-2 and round-3 review fixes. **No protocol change; no behavior change for any frontend today** — with `panel_capable = false` for semantic sessions, `primary_document_window` returns `view.active` in every existing configuration, so this is seam adoption that becomes load-bearing in 2B. - Verification on the merge result: `cargo fmt --check` clean; strict - workspace Clippy clean; **1,832 default + 2,014 CRDT** library tests; - `bottom_panel_stage2a_acceptance` **16**; bottom-panel Stage 1 46; + workspace Clippy clean; **1,832 default + 2,015 CRDT** library tests; + `bottom_panel_stage2a_acceptance` **17**; bottom-panel Stage 1 46; statusline segments 8 CRDT; m11_5 semantic 2 CRDT; GPU initial target 14 CRDT; terminal config 12 CRDT; vterm Stage 1/2 10 / 6; folding Stage 2 48; M4 121; required GPU 202; `git diff --check` clean. @@ -521,7 +521,12 @@ implemented and in review.** under test; (c) a discriminating fixture must make the two routings DISAGREE — comparing two non-terminal buffers, or two windows with no selection, yields the same answer either way and proves nothing. - Round 2 found four of my own pins vacuous by exactly these shapes. + Round 2 found four of my own pins vacuous by exactly these shapes, and + round 3 found two more problems of the same family: a pin placed at a + HELPER while production called it from a producer (reverting only the + producer's call site left every test green), and a socket-pair + assertion whose blocking read made a regression HANG instead of fail. + Both now assert at the producer, with read timeouts on every read. - **Review round 1 closed: 4 P1 + 2 P2, all real.** The P1s were a stale-`Pointer` focus steal (the failed-alignment arm returned the window, so #8's activation focused it before `dispatch_pointer` diff --git a/src/daemon.rs b/src/daemon.rs index 63f6b87..84716eb 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -3483,6 +3483,96 @@ mod tests { ); } + /// Bottom-panel §1.3 #21 through the REAL producer (round 3). + /// + /// A semantic peer with a FOCUSED PANEL must still receive the + /// snapshot for the buffer on its DOCUMENT surface, and must NOT + /// receive one for a buffer visible only in its panel. Asserting the + /// helper alone was insufficient: reverting the producer's call site + /// to focused-window routing left every helper-level test green. + #[cfg(feature = "crdt")] + #[test] + fn snapshot_publication_follows_the_document_under_a_focused_panel() { + let (editor, fid, document, panel) = panel_focused_semantic_fixture(); + let (doc_buf, panel_buf) = { + let core = editor.core.borrow(); + ( + core.windows[&document].buffer_id, + core.windows[&panel].buffer_id, + ) + }; + assert_ne!(doc_buf, panel_buf, "fixture: distinct buffers"); + + let caps = crate::protocol::NegotiatedCapabilities { + multi_frontend: true, + crdt_replica: true, + semantic_render: true, + }; + let mut registry = SessionRegistry::new(); + registry.register_session( + fid, + crate::presence::SessionState::new(PROTOCOL_VERSION, caps, 0), + ); + + // The DOCUMENT buffer's snapshot must be delivered. + { + let (server, mut client) = UnixStream::pair().expect("socketpair"); + // A read timeout on the DELIVERY read too. Without it a + // regression that suppresses the snapshot makes this test + // HANG rather than fail, which is strictly worse than a red + // assertion — found by biting this very test. + client + .set_read_timeout(Some(Duration::from_millis(500))) + .expect("delivery timeout"); + let mut streams = HashMap::from([(fid, server)]); + let message = InstanceMessage::BufferSnapshot { + buffer_id: doc_buf, + crdt_snapshot: vec![1, 2, 3], + }; + publish_buffer_snapshot_to_replicas( + &editor, + doc_buf, + &message, + ®istry, + &mut streams, + &mut HashMap::new(), + ); + let delivered: InstanceMessage = + read_message(&mut client).expect("the document snapshot must arrive"); + assert_eq!( + delivered, message, + "#21: a buffer on the DOCUMENT surface must still be published while a \ + panel holds focus" + ); + } + + // The PANEL-only buffer's snapshot must NOT be delivered. + { + let (server, mut client) = UnixStream::pair().expect("socketpair"); + let mut streams = HashMap::from([(fid, server)]); + let message = InstanceMessage::BufferSnapshot { + buffer_id: panel_buf, + crdt_snapshot: vec![4, 5, 6], + }; + publish_buffer_snapshot_to_replicas( + &editor, + panel_buf, + &message, + ®istry, + &mut streams, + &mut HashMap::new(), + ); + client + .set_read_timeout(Some(Duration::from_millis(50))) + .expect("timeout"); + assert!( + read_message::(&mut client).is_err(), + "#21: a buffer visible only in a PANEL must not replace the peer's \ + document mirror" + ); + } + } + // ---- GPU terminal input: the double terminal-layout sync ------------- // // These drive `sync_terminal_layouts_for_tick` — the REAL dispatcher loop @@ -4827,15 +4917,13 @@ mod tests { "#3: CursorByte must describe the DOCUMENT surface" ); - // #21 publication recipient filter, both directions. - assert!( - peer_displays_buffer_as_document(&editor, fid, doc_buf), - "#21: a buffer visible in the document must still receive publications while a panel holds focus" - ); - assert!( - !peer_displays_buffer_as_document(&editor, fid, panel_buf), - "#21: a buffer visible only in a panel must NOT replace the document mirror" - ); + // #21 is deliberately NOT asserted here. Round 3: pinning it at + // this helper left the real producer free to regress — reverting + // the call site inside `publish_buffer_snapshot_to_replicas` + // kept both this test and the existing socket-pair test green. + // It is pinned through the producer instead, in + // `snapshot_publication_follows_the_document_under_a_focused_panel`. + let _ = panel_buf; } /// Bottom-panel §1.3 #2 — the sharpest census case: the lazy CRDT diff --git a/src/semantic_render.rs b/src/semantic_render.rs index af08741..db96fc4 100644 --- a/src/semantic_render.rs +++ b/src/semantic_render.rs @@ -625,6 +625,22 @@ impl SemanticRenderState { // post-evaluation face inventory must then precede the authoritative // segment replacement in this same frame. Unsupported peers skip the // evaluator entirely and therefore pay no Lua callback/dynamic-face cost. + // Bottom-panel A2A-2, round 3: the document identity used to + // FILTER the results must be the PRE-CALLBACK one. Both outcome + // arms carry phase-1 contexts, and a provider that closes the + // primary document split changes `primary_document_window` + // mid-evaluation — reading it after the fact would compare + // phase-1 contexts against a replacement identity, match + // nothing, and silently suppress the authoritative clear. + let statusline_document_window = self + .peer_knows_statusline_segments + .then(|| { + state + .core + .borrow() + .primary_document_window(self.frontend_id) + }) + .flatten(); let statusline_evaluation = self.peer_knows_statusline_segments.then(|| { evaluate_statusline( state.lua_host.lua(), @@ -810,11 +826,7 @@ impl SemanticRenderState { out.extend(self.font_facts_msg(state)); // Q#SL6/Q#SL8: face inventory must precede segment text. if let Some(evaluation) = statusline_evaluation { - let document_window = state - .core - .borrow() - .primary_document_window(self.frontend_id); - self.emit_statusline_segments(evaluation, document_window, &mut out); + self.emit_statusline_segments(evaluation, statusline_document_window, &mut out); } out } @@ -859,6 +871,16 @@ impl SemanticRenderState { // Evaluate callbacks before `ThemeFacts` for the same reason the // document path does: a callback may register a face, and the // face inventory must precede the segment text that names it. + // Same pre-callback capture as the document path (round 3). + let statusline_document_window = self + .peer_knows_statusline_segments + .then(|| { + state + .core + .borrow() + .primary_document_window(self.frontend_id) + }) + .flatten(); let statusline_evaluation = self.peer_knows_statusline_segments.then(|| { evaluate_statusline( state.lua_host.lua(), @@ -885,7 +907,12 @@ impl SemanticRenderState { // a verdict we hold. if self.last_terminal_frame.as_ref() == Some(&frame) { self.terminal_error_latched = false; - out.extend(self.terminal_chrome(state, buffer_id, statusline_evaluation)); + out.extend(self.terminal_chrome( + state, + buffer_id, + statusline_evaluation, + statusline_document_window, + )); return Some(out); } match frame.validate() { @@ -909,7 +936,12 @@ impl SemanticRenderState { } } - out.extend(self.terminal_chrome(state, buffer_id, statusline_evaluation)); + out.extend(self.terminal_chrome( + state, + buffer_id, + statusline_evaluation, + statusline_document_window, + )); Some(out) } @@ -924,6 +956,7 @@ impl SemanticRenderState { state: &EditorState, buffer_id: BufferId, statusline_evaluation: Option, + statusline_document_window: Option, ) -> Vec { let mut out = Vec::new(); out.extend(self.status_facts_msg(state, buffer_id)); @@ -933,11 +966,7 @@ impl SemanticRenderState { out.extend(self.font_facts_msg(state)); // Q#SL6/Q#SL8: face inventory must precede segment text. if let Some(evaluation) = statusline_evaluation { - let document_window = state - .core - .borrow() - .primary_document_window(self.frontend_id); - self.emit_statusline_segments(evaluation, document_window, &mut out); + self.emit_statusline_segments(evaluation, statusline_document_window, &mut out); } out } diff --git a/tests/bottom_panel_stage2a_acceptance.rs b/tests/bottom_panel_stage2a_acceptance.rs index 1063e9f..d39d804 100644 --- a/tests/bottom_panel_stage2a_acceptance.rs +++ b/tests/bottom_panel_stage2a_acceptance.rs @@ -784,3 +784,115 @@ fn consumer_decorations_follow_the_document_selection_not_the_panel() { "a selection living in the focused PANEL must not decorate the document viewport" ); } + +#[test] +fn a_provider_closing_the_document_split_still_clears_the_statusline() { + use pmacs::protocol::{ByteRange, InstanceMessage}; + use pmacs::semantic_render::SemanticRenderState; + + // Round 3 finding 1. `authoritative_empty` carries PHASE-1 contexts, + // so the identity used to filter them must be the PRE-CALLBACK one. + // A provider that closes the primary document split changes + // `primary_document_window` mid-evaluation; reading it afterwards + // compares phase-1 contexts against a replacement identity, matches + // nothing, and silently suppresses the authoritative clear — leaving + // stale statusline text on screen forever. + // + // Driven on LOCAL, because the Lua window API acts on the ACTIVE + // FRONTEND: a synthetic semantic view would be untouched by + // `pmacs.window.close()` and the identity would never change, which + // is exactly how the first version of this test came back vacuous. + // TWO document windows plus the panel: closing the only document + // window is structurally refused (Q#BP6 forbids a lone side window + // as a resting state), so the first attempt could not change the + // identity at all. Distinct buffers make the target selectable from + // a Lua provider, which has no focus-by-id. + let s = editor(); + exec( + &s, + "DOC_A = pmacs.buffer.create(\"*doc-a*\") + DOC_B = pmacs.buffer.create(\"*doc-b*\") + pmacs.window.display(DOC_A, {}) + pmacs.window.split_horizontal() + pmacs.window.focus_next() + pmacs.window.display(DOC_B, {})", + ); + let (_origin, panel) = focused_panel(&s); + let (document, doc_buf) = { + let core = s.core.borrow(); + let win = core + .primary_document_window(FrontendId::LOCAL) + .expect("a primary document window"); + (win, core.windows[&win].buffer_id) + }; + assert_ne!(document, panel); + + let mut sem = SemanticRenderState::for_peer(FrontendId::LOCAL, 18); + sem.set_viewport(doc_buf, ByteRange { start: 0, end: 0 }, 0); + + // Seed a baseline payload so a CLEAR is observable as a change. + exec( + &s, + r"_G.SL_SEED = pmacs.statusline.register { + name='seed', side='left', priority=10, + fn=function() return 'OLD' end, + }", + ); + let seeded = sem.render_frame(&s); + assert!( + seeded + .iter() + .any(|m| matches!(m, InstanceMessage::StatuslineSegments { .. })), + "non-vacuity: a baseline payload must exist before we test its clear" + ); + + // A provider that unregisters itself (making the evaluation + // Invalidated) AND closes the captured document window. `close()` + // closes the ACTIVE window and Lua has no focus-by-id, so step + // around the ring until the captured buffer is current. + s.lua_host + .lua() + .globals() + .set("TARGET_BUF", pmacs::lua_bindings::BufferIdLua(doc_buf)) + .expect("expose the target buffer"); + exec( + &s, + r"_G.SL_CLOSER = pmacs.statusline.register { + name='closer', side='left', priority=100, + fn=function() + pmacs.statusline.unregister(SL_CLOSER) + for _ = 1, 8 do + if pmacs.window.buffer() == TARGET_BUF then break end + pmacs.window.focus_next() + end + pmacs.window.close() + return 'STALE' + end, + }", + ); + + let msgs = sem.render_frame(&s); + + // The fixture must actually have changed the identity, or this test + // discriminates nothing. + assert_ne!( + s.core.borrow().primary_document_window(FrontendId::LOCAL), + Some(document), + "fixture: the callback must really have changed the document identity" + ); + + let cleared = msgs.iter().any(|m| match m { + InstanceMessage::StatuslineSegments { + buffer_id, + left, + right, + .. + } => *buffer_id == doc_buf && left.is_empty() && right.is_empty(), + _ => false, + }); + assert!( + cleared, + "an invalidated evaluation must still publish the authoritative EMPTY clear for \ + the phase-1 document identity, even when a callback closed that window; got {msgs:?}" + ); +} From aef4e98c26ecb2c840c564e2a4f721241e229e0a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:39:33 -0400 Subject: [PATCH 13/14] fix(typed-edit): close round-8 review on the consumer chain MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five defects in the chain itself, plus the stale handoff state. Each consumer now gets its own shallow copy of the typed-edit record. Handing everyone the same table let a DECLINING consumer rewrite provenance for the ones behind it, and pairing decides what to close from `rec.char` — so a forged `char` turned a typed `x` into `x)`. Every field is a scalar or an opaque id, so a shallow copy is complete. The fan-out iterates a snapshot of the consumer list. It was iterating the same array `add_consumer` mutates: a consumer that registered a lower-priority one shifted itself forward under `ipairs` and ran twice, and re-registering made that unbounded. Registrations and removals made during a fan-out now take effect on the next one, stated as a contract and pinned in both directions. `tostring` on the caught error moved inside the containment. A Lua error may be any value, including a table whose `__tostring` throws — rendering it outside the `pcall` reintroduced exactly the escape the containment exists to prevent. Priorities are validated as finite integers in i32 range, matching `pmacs.completion.register`. NaN is a number and every ordered comparison with it is false, so a NaN consumer landed wherever the insertion scan gave up and silently voided the lowest-first ordering that Q#LN22 depends on. `add_consumer` returns a handle and `remove_consumer` unregisters it, reporting whether it was live. Without teardown the chain inherited the `pmacs.hook.add` callback leak COHERENCE.md §13 already records, and spread it to every consumer. Also corrects the rationale the containment was documented with, in the module, the test, and the framing: an uncontained throw does NOT take the fan-out's other subscribers down. `run_all_must_succeed` (src/hook.rs:332) collects errors and continues, so lsp.lua still flushes didChange. The containment is still required — the throw skips every later consumer in the chain — but the reason is narrower than rev 7 claimed. Criteria 46f (record isolation), 46g (snapshot iteration), and 46h (lifecycle and priority validation) added; 46d's rationale corrected. Four new tests, all bite-verified by mutation, each failing only its target: shared record table (1), live-array iteration (1), unprotected tostring (1), bare number check (1), no-op removal (2). The suite also runs green under `--features lua54`. docs/agent-handoff.md said Stage 4a was awaiting approval while this branch had it implemented and in review. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/typed_edit.lua | 113 ++++++++++--- docs/active-work.md | 41 ++++- docs/agent-handoff.md | 24 ++- docs/lean4-mode-framing.md | 42 ++++- tests/typed_edit_chain_acceptance.rs | 232 ++++++++++++++++++++++++++- 5 files changed, 406 insertions(+), 46 deletions(-) diff --git a/builtin/runtime/typed_edit.lua b/builtin/runtime/typed_edit.lua index 59f7366..6baf5f8 100644 --- a/builtin/runtime/typed_edit.lua +++ b/builtin/runtime/typed_edit.lua @@ -13,11 +13,12 @@ -- subscriber that reads the record, and offers that one read to -- consumers registered through `pmacs.typed_edit.add_consumer`: -- --- pmacs.typed_edit.add_consumer { --- name = "auto-pair", -- for error reporting; must be unique-ish +-- local handle = pmacs.typed_edit.add_consumer { +-- name = "auto-pair", -- for error reporting -- priority = 100, -- LOWEST runs FIRST -- fn = function(rec) ... return claimed end, -- } +-- pmacs.typed_edit.remove_consumer(handle) -- -> true if it was live -- -- A consumer returns whether it CLAIMED the edit; the first that claims -- stops the chain. "Claimed" means the chain stops, not that an edit was @@ -46,10 +47,19 @@ pmacs.typed_edit = pmacs.typed_edit or {} -- order" is part of the stated contract, not an incidental property. local consumers = {} --- Register a typed-edit consumer. Argument errors throw: registration --- happens at chunk-load or config-load time, where a throw is a visible --- startup failure rather than a silently missing feature. Nothing in --- the after-edit path throws --- see the fan-out below. +-- Handles are opaque to callers; only identity matters. An integer +-- counter is enough because nothing ever reuses one. +local next_handle = 0 + +-- `math.huge` is the only portable spelling of infinity available in +-- both LuaJIT and 5.4, and NaN is the only value not equal to itself. +local INT32_MIN, INT32_MAX = -2147483648, 2147483647 + +-- Register a typed-edit consumer; returns an opaque handle for +-- `remove_consumer`. Argument errors throw: registration happens at +-- chunk-load or config-load time, where a throw is a visible startup +-- failure rather than a silently missing feature. Nothing in the +-- after-edit path throws --- see the fan-out below. function pmacs.typed_edit.add_consumer(spec) if type(spec) ~= "table" then error("pmacs.typed_edit.add_consumer: spec must be a table", 2) @@ -58,9 +68,18 @@ function pmacs.typed_edit.add_consumer(spec) if type(name) ~= "string" or name == "" then error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2) end - if type(priority) ~= "number" then + -- A bare `type(priority) == "number"` admits NaN and the infinities, + -- and EVERY ordered comparison against NaN is false --- so a NaN + -- consumer silently lands wherever the insertion scan happens to give + -- up, and the lowest-first contract other consumers depend on stops + -- holding. Bounded integers match `pmacs.completion.register`, whose + -- priority is an i32 on the Rust side. + if type(priority) ~= "number" or priority ~= priority + or priority == math.huge or priority == -math.huge + or priority % 1 ~= 0 + or priority < INT32_MIN or priority > INT32_MAX then error("pmacs.typed_edit.add_consumer: " .. name .. - ": priority must be a number", 2) + ": priority must be a finite integer in [-2147483648, 2147483647]", 2) end if type(fn) ~= "function" then error("pmacs.typed_edit.add_consumer: " .. name .. @@ -77,7 +96,27 @@ function pmacs.typed_edit.add_consumer(spec) break end end - table.insert(consumers, at, { name = name, priority = priority, fn = fn }) + next_handle = next_handle + 1 + local handle = next_handle + table.insert(consumers, at, + { handle = handle, name = name, priority = priority, fn = fn }) + return handle +end + +-- Unregister a consumer by the handle `add_consumer` returned. Returns +-- true if it was registered, false otherwise (so a double-remove is a +-- reportable no-op rather than a throw). Without this, re-evaluating a +-- config or reloading a package accumulates callbacks permanently --- +-- the leak COHERENCE.md §13 already records against `pmacs.hook.add`, +-- which this chain would otherwise inherit and spread. +function pmacs.typed_edit.remove_consumer(handle) + for i, c in ipairs(consumers) do + if c.handle == handle then + table.remove(consumers, i) + return true + end + end + return false end pmacs.hook.add("buffer.after-edit", function() @@ -92,19 +131,51 @@ pmacs.hook.add("buffer.after-edit", function() -- fan-out on nil would leave both reading stale state. local rec = ed.take_typed_edit and ed.take_typed_edit() - for _, c in ipairs(consumers) do - -- `buffer.after-edit` is all-must-succeed (builtin/hooks/default.lua): - -- a throwing consumer would fail the fan-out for every OTHER - -- subscriber, including lsp.lua's didChange flush. Contain it, - -- report it, and keep going --- a broken consumer must not be able - -- to stop the editor from telling the language server what changed. - -- This matches pair.lua's existing never-throw-from-after-edit - -- discipline; it does not weaken the hook's contract for anyone - -- else, because the chain itself still never fails. - local ok, claimed = pcall(c.fn, rec) + -- Iterate a SNAPSHOT. A consumer may register or remove consumers + -- while the chain is running, and `table.insert`/`table.remove` on + -- the live array shifts indices under `ipairs` --- a consumer that + -- registers a lower-priority one shifts itself forward and runs + -- twice, and repeating that is unbounded. Registrations and removals + -- made during a fan-out therefore take effect on the NEXT fan-out. + local snapshot = {} + for i, c in ipairs(consumers) do + snapshot[i] = c + end + + for _, c in ipairs(snapshot) do + -- Each consumer gets its OWN copy of the record. The table handed + -- out is plain Lua data, so a declining consumer could otherwise + -- edit `rec.char` in place and the next consumer would act on the + -- forged value --- auto-pairing reads `rec.char` to decide what to + -- close, so a rewritten `char` makes it insert a pair the user + -- never typed. Every field is a scalar or an opaque id, so a + -- shallow copy is a complete snapshot. + local mine = nil + if rec ~= nil then + mine = {} + for k, v in pairs(rec) do + mine[k] = v + end + end + + -- Contain the consumer. A throw here would skip every LATER + -- consumer in the chain and mark the whole `buffer.after-edit` run + -- failed; the other subscribers still run, because all-must-succeed + -- collects errors and continues (`src/hook.rs`'s + -- `run_all_must_succeed`), but one broken consumer must not be able + -- to silently disable the ones behind it. This matches pair.lua's + -- existing never-throw-from-after-edit discipline. + local ok, claimed = pcall(c.fn, mine) if not ok then - ed.set_status("typed-edit consumer '" .. c.name .. "' failed: " .. - tostring(claimed)) + -- Rendering is itself protected: a Lua error may be any value, + -- including a table whose `__tostring` throws, and an escaping + -- error here would defeat the containment above. + local shown, rendered = pcall(tostring, claimed) + if not shown or type(rendered) ~= "string" then + rendered = "" + end + pcall(ed.set_status, + "typed-edit consumer '" .. c.name .. "' failed: " .. rendered) elseif claimed then return end diff --git a/docs/active-work.md b/docs/active-work.md index bd0c0b1..ba1947a 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -149,9 +149,9 @@ If it does not, stop and repair the remote/fetch configuration. ### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) - Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` - (new, 112 lines), `pair.lua` re-expressed as one consumer, + (new), `pair.lua` re-expressed as one consumer, `src/editor.rs` +15 (the `include_str!` and its ordering comment), and - `tests/typed_edit_chain_acceptance.rs` (new, 9 tests). + `tests/typed_edit_chain_acceptance.rs` (new, 13 tests). **`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is criterion 46 checked at the diff, which is the only way it means @@ -166,9 +166,26 @@ If it does not, stop and repair the remote/fetch configuration. - **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and "ties broken by registration order" is a stated contract. - **The chain `pcall`s each consumer** and reports through - `set_status`. `buffer.after-edit` is all-must-succeed, so an - uncontained throw fails the fan-out for every other subscriber - including lsp.lua's didChange flush. + `set_status`. Rev 7 justified this by claiming an uncontained throw + would fail the fan-out for every other subscriber including lsp.lua's + didChange flush; **that is wrong** — `run_all_must_succeed` + (`src/hook.rs:332`) collects errors and continues, so the other + subscribers still run. The real consequence is narrower and still + worth containing: the throw skips every LATER consumer in the chain. + The rendering is protected too, because a Lua error may be a table + whose `__tostring` throws. +- **Round 8 (review) findings, all fixed on this branch:** each consumer + now gets its **own shallow copy** of the record (the same table let a + declining consumer rewrite `rec.char`, which pairing reads — typing + `x` could produce `x)`); the fan-out iterates a **snapshot** (a + consumer registering a lower-priority one shifted itself forward under + `ipairs` and ran twice, unbounded if repeated); `tostring` moved + inside the containment; **non-finite and non-integer priorities are + rejected** (NaN is a number and every ordered comparison with it is + false, so it landed wherever the insertion scan gave up and silently + voided the ordering contract); and `add_consumer` now returns a handle + with `remove_consumer` beside it, so re-evaluating a config no longer + leaks callbacks the way `pmacs.hook.add` does (COHERENCE §13). - **Every acceptance test is bite-verified by mutation**, per the standing rule that a test is not evidence until the mutation it targets has been shown to fail it: @@ -182,6 +199,11 @@ If it does not, stop and repair the remote/fetch configuration. | drop the `pcall` | 1 chain | | skip consumers when `rec == nil` | 1 chain + **3 auto-pair** | | load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) | + | hand every consumer the same record table | 1 chain (46f) | + | iterate the live array instead of a snapshot | 1 chain (46g) | + | render the error outside the `pcall` | 1 chain (46d) | + | accept any Lua number as a priority | 1 chain (46h) | + | make `remove_consumer` a no-op | 2 chain (46g, 46h) | The first attempt at the last bite was WORTHLESS as written: moving only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil @@ -194,9 +216,12 @@ If it does not, stop and repair the remote/fetch configuration. - Verification on this branch (commit-then-gate, so this describes the pushed tree): `cargo fmt --check` clean; strict workspace Clippy clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45; - typed-edit chain 9/9; M4 121; required GPU 202; **isolated-config - workspace sweep 3,328 across 97 suites, zero failures** with - `grep -c basedpyright` = 0; `git diff --check` clean. + typed-edit chain 13/13 (and 13/13 again under `--no-default-features + --features lua54`, since the fixes touch `math.huge`, `%`, and + `__tostring` behavior that differs between the backends); M4 121; + required GPU 202; **isolated-config workspace sweep 3,332 across 97 + suites, zero failures** with `grep -c basedpyright` = 0; `git diff + --check` clean. - Stage 4b (the input method) is NOT in this PR and not started. ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index a176505..66ccc25 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -88,10 +88,26 @@ commands, read `docs/active-work.md` immediately after this file. config swap invalidates. The durable lesson is to heal at **consumption** — the point where a stale record is handed out — not at the moment of the swap. - - Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode - input method) are framed and awaiting approval; stages 5 (goal - panel), 6 (`#eval` output channel), and 7 (module hierarchy) are - framed but not scouted against current `main`. + - **Stage 4a (typed-edit consumer chain) is implemented and in review + as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev + 8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the + single `buffer.after-edit` subscriber and the single one-shot read, + `pair.lua` becomes its first registered consumer, and + `tests/auto_pair_acceptance.rs` is unchanged by zero lines + (criterion 46, verified at the diff). No protocol change, no Lean + content. The three decisions that turned out load-bearing rather + than stylistic: consumers are called **even when the record is + nil** (three existing auto-pair tests assert the non-event through + it, and 4b abandons stale pending state on it); each consumer gets + its **own copy** of the record, because pairing reads `rec.char` + and a declining consumer could otherwise forge it; and the fan-out + iterates a **snapshot**, because a consumer that registers a + lower-priority one shifts itself forward under `ipairs` and runs + twice. + - Remaining: Stage 4b (the Unicode input method) is framed and + awaiting approval — not started; stages 5 (goal panel), 6 (`#eval` + output channel), and 7 (module hierarchy) are framed but not + scouted against current `main`. - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 650b2f3..789e419 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1496,7 +1496,7 @@ claim a reader must be able to check without reconstructing | `builtin/runtime/typed_edit.lua` | new — the chain owner | | `builtin/runtime/pair.lua` | re-expressed as one registered consumer | | `src/editor.rs` | one `include_str!` line, before `pair.lua`'s | -| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e | +| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46h | | `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** | Rev 6 listed only the first three and then required criteria 46a–46e, @@ -2374,7 +2374,7 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage. Per the no-renumbering rule above, round 5's additions take letter suffixes on both sides of the split. -46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which +46a–46h live in a **new `tests/typed_edit_chain_acceptance.rs`**, which is part of Stage 4a's declared footprint (Q#LN10) and a required gate for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which criterion 46 requires to stay byte-identical. @@ -2394,14 +2394,44 @@ criterion 46 requires to stay byte-identical. `include_str!` order happens to agree with intent. 46c. A claiming consumer stops the chain — a later consumer does not run — and a non-claiming one does not. -46d. A consumer that throws is contained: the fan-out still succeeds, - the other consumers still run, and the failure reports through - `set_status`. Bites against the `all-must-succeed` contract taking - the whole fan-out down with one bad consumer (Q#LN10). +46d. A consumer that throws is contained: the later consumers still + run, and the failure reports through `set_status`. Bites against a + chain where one bad consumer silently disables every consumer + behind it. (Round 8 correction: an uncontained throw would *not* + take the fan-out's other subscribers down — `run_all_must_succeed` + in `src/hook.rs` collects errors and continues, so `lsp.lua` still + flushes. Rev 7 claimed otherwise. The containment is still + required; the reason is narrower than stated.) Rendering the error + is itself protected: a Lua error may be any value, including a + table whose `__tostring` throws, and reporting outside the + containment reintroduces the escape it exists to prevent. 46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server test — pairing's closer must be in the buffer before `lsp.lua` flushes `didChange` — still holds with pairing behind the chain. Falsified by moving the chain's registration after `lsp.lua`'s. +46f. **Each consumer's record is its own.** A declining consumer that + mutates the record it was handed cannot change what a later + consumer sees. Bites against handing every consumer the same + mutable table: pairing decides what to close from `rec.char`, so a + forged `char` makes it insert a pair the user never typed. Every + field is a scalar or an opaque id, so a shallow copy is a complete + snapshot. +46g. **The fan-out iterates a snapshot.** A consumer may register or + remove consumers while the chain runs; both take effect on the next + fan-out. Bites against iterating the live array, where a consumer + that registers a lower-priority one shifts itself forward under + `ipairs` and runs twice — unbounded if it re-registers each time. +46h. **The registrar has a lifecycle.** `add_consumer` returns an + opaque handle; `remove_consumer` unregisters it and reports whether + it was live, so a double-remove is a no-op rather than a throw. + Without it, re-evaluating a config or reloading a package + accumulates callbacks permanently — the leak `COHERENCE.md` §13 + already records against `pmacs.hook.add`, which a teardown-less + chain would inherit and spread to every consumer. Priority is + validated as a **finite integer in i32 range**, matching + `pmacs.completion.register`: NaN is a number and every ordered + comparison with it is false, so a bare type check lets it land + wherever the insertion scan gives up and silently voids 46b. **Stage 4b — the Unicode input method** diff --git a/tests/typed_edit_chain_acceptance.rs b/tests/typed_edit_chain_acceptance.rs index c0170f4..8ff9c13 100644 --- a/tests/typed_edit_chain_acceptance.rs +++ b/tests/typed_edit_chain_acceptance.rs @@ -1,11 +1,13 @@ //! Typed-edit consumer chain acceptance (Arc 8 Stage 4a, -//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46e). +//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46h). //! //! The chain owns the single `buffer.after-edit` subscriber that reads //! the one-shot typed-edit record (Q#AP9) and offers it to consumers in //! priority order. These tests pin the chain's OWN behavior — take-once, -//! priority ordering, claim-stops-chain, throw containment, and the -//! Q#AP7 flush ordering it inherited from `pair.lua`. +//! priority ordering, claim-stops-chain, throw containment, per-consumer +//! record isolation, snapshot iteration under re-entrant registration, +//! the registration lifecycle, and the Q#AP7 flush ordering it inherited +//! from `pair.lua`. //! //! They deliberately do not re-test auto-pairing: criterion 46 requires //! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that @@ -324,9 +326,12 @@ fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() { "#, ); - // `buffer.after-edit` is all-must-succeed: an uncontained throw - // would fail the fan-out for every other subscriber, including - // lsp.lua's didChange flush. + // An uncontained throw would abandon every LATER consumer in the + // chain and mark the whole `buffer.after-edit` run failed. It would + // NOT stop the hook's other subscribers — all-must-succeed collects + // errors and keeps going (`src/hook.rs`'s `run_all_must_succeed`) — + // so what this pins is that one broken consumer cannot silently + // disable the ones behind it. type_str(&mut s, "("); let later_ran: bool = eval(&s, "return _G.later_ran"); @@ -357,12 +362,43 @@ fn add_consumer_rejects_malformed_registrations() { ), ( "pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }", - "priority must be a number", + "priority must be a finite integer", ), ( "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }", "fn must be a function", ), + // NaN is a number and every ordered comparison with it is + // false, so a bare type check lets it land wherever the + // insertion scan gives up — and the lowest-first contract the + // Lean expander depends on quietly stops holding. The + // infinities and non-integers go with it: priority matches + // `pmacs.completion.register`'s i32. + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 0/0, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = math.huge, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = -math.huge, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1.5, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 4e9, \ + fn = function() end }", + "priority must be a finite integer", + ), ] { let err = s .lua_host @@ -378,6 +414,188 @@ fn add_consumer_rejects_malformed_registrations() { } } +#[test] +fn an_error_whose_rendering_throws_is_still_contained() { + // A Lua error may be any value, including a table whose + // `__tostring` throws. Rendering it outside the containment is a + // second, uncontained throw — the chain would stop at exactly the + // consumer it was trying to report. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + local hostile = setmetatable({}, { + __tostring = function() error("rendering exploded") end, + }) + pmacs.typed_edit.add_consumer { + name = "boom", priority = 1, fn = function() error(hostile) end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!( + later_ran, + "an unrenderable error must not escape the containment" + ); + assert_eq!(buffer_text(&s), "()", "and pairing still ran"); + let st = status(&s); + assert!( + st.contains("boom") && st.contains(""), + "the consumer is still named, with a placeholder body, got {st:?}" + ); +} + +// --------------------------------------------------------------------------- +// The record a consumer sees is its own +// --------------------------------------------------------------------------- + +#[test] +fn a_consumers_mutation_of_the_record_cannot_reach_the_next_consumer() { + // The record is plain Lua data. Handing every consumer the same + // table lets a DECLINING consumer rewrite provenance for the ones + // behind it — and pairing decides what to close from `rec.char`, + // so a forged `char` makes it insert a pair the user never typed. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.downstream_char = "unset" + pmacs.typed_edit.add_consumer { + name = "vandal", priority = 1, + fn = function(rec) + if rec then rec.char = "("; rec.codepoint = 40 end + return false + end, + } + pmacs.typed_edit.add_consumer { + name = "witness", priority = 2, + fn = function(rec) + _G.downstream_char = rec and rec.char or "nil" + return false + end, + } + "#, + ); + + type_str(&mut s, "x"); + + let downstream: String = eval(&s, "return _G.downstream_char"); + assert_eq!( + downstream, "x", + "the next consumer sees the real typed character" + ); + assert_eq!( + buffer_text(&s), + "x", + "and pairing, reading the same field, did not close a forged opener" + ); +} + +// --------------------------------------------------------------------------- +// Re-entrant registration, and the consumer lifecycle +// --------------------------------------------------------------------------- + +#[test] +fn registering_or_removing_during_a_fan_out_takes_effect_on_the_next_one() { + // The fan-out iterates a snapshot. Iterating the live array instead + // lets a consumer that registers a LOWER-priority one shift itself + // forward under `ipairs` and run twice in a single fan-out — and + // repeating the registration makes that unbounded. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + _G.doomed = pmacs.typed_edit.add_consumer { + name = "doomed", priority = 50, fn = mark("doomed"), + } + _G.did_register = false + pmacs.typed_edit.add_consumer { + name = "a", priority = 10, + fn = function() + _G.order[#_G.order + 1] = "a" + if not _G.did_register then + _G.did_register = true + pmacs.typed_edit.add_consumer { name = "b", priority = 5, fn = mark("b") } + pmacs.typed_edit.remove_consumer(_G.doomed) + end + return false + end, + } + "#, + ); + + type_str(&mut s, "x"); + let first: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + first, "a,doomed", + "`a` runs once even though it registered ahead of itself, and \ + `doomed` still runs in the fan-out it was removed during" + ); + + exec(&s, "_G.order = {}"); + type_str(&mut s, "y"); + let second: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + second, "b,a", + "both the registration and the removal land on the next fan-out" + ); +} + +#[test] +fn remove_consumer_unregisters_and_reports_whether_it_was_live() { + // Without removal, re-evaluating a config or reloading a package + // accumulates callbacks permanently — the leak COHERENCE.md §13 + // already records against `pmacs.hook.add`. A chain with no + // teardown would inherit it and spread it to every consumer. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.runs = 0 + _G.h = pmacs.typed_edit.add_consumer { + name = "temporary", priority = 1, + fn = function() _G.runs = _G.runs + 1; return false end, + } + "#, + ); + + type_str(&mut s, "x"); + let runs: i64 = eval(&s, "return _G.runs"); + assert_eq!(runs, 1, "registered consumers run"); + + let first_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)"); + let second_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)"); + assert!(first_removal, "removing a live consumer reports true"); + assert!( + !second_removal, + "a double-remove is a reportable no-op, not a throw" + ); + + type_str(&mut s, "y"); + let runs: i64 = eval(&s, "return _G.runs"); + assert_eq!(runs, 1, "the removed consumer no longer runs"); + // Removal is surgical: the chain itself, and pairing on it, survive. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "("); + assert_eq!( + buffer_text(&s), + "xy()", + "the rest of the chain is untouched" + ); +} + // --------------------------------------------------------------------------- // 46e — the Q#AP7 flush ordering the chain inherited // --------------------------------------------------------------------------- From ea9b8c379e97fdfb84e86d37b21a3de8bbb7c1f9 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:43:30 -0400 Subject: [PATCH 14/14] docs(lean4): correct Q#LN10's throw-containment rationale MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Q#LN10 still said a throwing consumer "fails the fan-out for everyone." It does not: `run_all_must_succeed` (src/hook.rs:332) collects the error and continues to the hook's remaining subscribers, so `lsp.lua` still flushes didChange. The throw stops every LATER consumer in the chain, which is a narrower consequence and still worth containing — the failure is silent exactly where the abandoned consumers registered. The module comment, criterion 46d, the test, and the ledger were all corrected in the previous commit; Q#LN10 is the decision they descend from, so leaving it stale would have made the disproven claim the authoritative one. Also records the protected-rendering rule there. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/lean4-mode-framing.md | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 789e419..c4a32e5 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1523,11 +1523,28 @@ sees the exact record via `_capture_records`, and that the Q#AP7 ordering against `lsp.lua`'s `didChange` flush still holds. **What 4a deliberately does not do.** It does not change the `all-must- -succeed` contract, so a consumer that throws still fails the fan-out for -everyone. The chain owner therefore `pcall`s each consumer and reports -through `pmacs.editor.set_status`, matching `pair.lua`'s existing -never-throw-from-after-edit discipline — this is behavior-preserving for -pairing (which already never throws) and is the guardrail 4b needs. +succeed` contract. What that contract actually does on a throw was +stated wrongly through rev 7 and is corrected here, because this +paragraph is the authority the module comment, criterion 46d, the test, +and the ledger all descend from: `run_all_must_succeed` +(`src/hook.rs:332`) **collects** the error and continues to the hook's +remaining subscribers, marking only the run as failed. An uncontained +throw inside the chain therefore does **not** stop `lsp.lua` from +flushing `didChange`. What it does stop is every LATER consumer in the +chain — the chain is one subscriber, and a throw abandons the rest of +its loop. + +That is a narrower consequence than rev 7 claimed and still worth +containing, because the failure is silent in the direction that matters: +a consumer that throws disables the consumers behind it with no signal +at the seam where they were registered. The chain owner therefore +`pcall`s each consumer and reports through `pmacs.editor.set_status`, +matching `pair.lua`'s existing never-throw-from-after-edit discipline — +this is behavior-preserving for pairing (which already never throws) and +is the guardrail 4b needs. The **rendering** of the caught error is +protected the same way: a Lua error may be any value, including a table +whose `__tostring` throws, so `tostring` outside the `pcall` would +reintroduce the escape the containment exists to prevent. ### Q#LN11 — Stage 4b data: vendor the table, generated, attributed