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..6baf5f8 --- /dev/null +++ b/builtin/runtime/typed_edit.lua @@ -0,0 +1,183 @@ +-- 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`: +-- +-- 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 +-- 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 = {} + +-- 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) + 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 + -- 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 finite integer in [-2147483648, 2147483647]", 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 + 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() + 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() + + -- 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 + -- 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 + end +end) diff --git a/docs/active-work.md b/docs/active-work.md index 3a5bb88..7df3466 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. @@ -14,11 +14,16 @@ 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` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel + Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal + configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the + CRDT undo repro #157, the inline-math landed-doc refresh #172, 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,413 +60,175 @@ 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, 4a MERGED; 4b is next -- 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 8 + 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 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) -### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`) +- 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. +- **Stage 4a merged as #179** (`main` @ `a27f646`, 2026-07-26) — the + typed-edit consumer chain. Worktree `../pmacs-lean-stage4`, branched + off `main` @ `d400f30`; retained, carrying nothing unmerged. + `docs/lean4-mode-framing.md` **revision 8** remains the approved + framing. **Stage 4b (the Lean-specific half) is framed and not + started.** +- **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 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 + 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`, 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, + `detect_buffer_language` 452→457, `send_request`/`send_notification` + 9342/9361→9507/9527. +### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) -- 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. +- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` + (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, 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 + 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`. 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: -### Stage 3b — the Lean language server (branch `lean4-stage3b-server`) + | 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) | + | 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) | -- 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.) + 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 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) @@ -611,57 +378,95 @@ If it does not, stop and repair the remote/fetch configuration. resolve *to*, and `pmacs .` should route into it rather than growing a second directory surface. -## GPU terminal input lane — IN REVIEW +## The CRDT half of the test corpus 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: +- **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: - | 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 | + | 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` | -- 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. +- **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". +- **⚠ `a37` will report green in the new job without running, unless the + job builds `pmacs-gpu` AND sets `PMACS_REQUIRE_GPU=1`.** Measured + 2026-07-26 while gating #173. `a37_real_daemon_real_pty_and_headless_gpu_ + render_one_terminal_session` derives its sibling binary path from + `CARGO_BIN_EXE_pmacs`, and on a missing binary it `eprintln!`s a skip and + **returns `ok`**. A fresh worktree running + `cargo test --features crdt --test vterm_stage3_acceptance` reports **9/9 + in 0.17 s having never run it**; a real run takes ~4 s. Only + `PMACS_REQUIRE_GPU=1` promotes that skip to a failure, and `CLAUDE.md` + applies that flag to `cargo test -p pmacs-gpu` — a **different package**, + so the required local gate does not cover a37 either. The `gpu-render` + job already sets the flag, which is what makes fix-shape part 2 sound; + state it as a **requirement** of that job rather than inheriting it by + luck, because a `crdt` leg added to the plain `test` job would run a37 + vacuously. +- **`a37` is also load-sensitive, which changes how to read the expected + first-run failures.** It passed at `d152120` and failed at that *same + commit* twenty minutes later, with a second agent saturating the machine + with `rustc` in between; it then failed identically on `d152120`, + `04c5ad1`, and the #173 merge commit, which is how #173 established the + failure was not its own. The signature is `last_frame_text` all spaces + with `rendered_nonuniform_frames` nonzero — frames arrive, content does + not. `pmacs-gpu`'s own suite flaked the same way under the same load + (201/202, then 202/202 on immediate rerun). **So a red a37 on the first + CI run is ambiguous by construction**: before treating it as a real + failure, run the same command on the merge base, and prefer serialized + execution for this suite over retry-until-green. +- **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, including the + controller-release pin whose only job is catching the plausible wrong fix. ## Terminal config + copy mode arc — Stage 1 MERGED; Stage 2 IN REVIEW @@ -670,8 +475,12 @@ If it does not, stop and repair the remote/fetch configuration. Stage 1's branch. Two stages, two branches, two PRs; **no protocol change**. - **Stage 1 MERGED as #173** (`main` @ `cf54270`, 2026-07-26, one review - round, twelve checks green). Branch `githubsucks/terminal-config` and - worktree `../pmacs-terminal-config` retained. + round, all twelve checks green). Branch `githubsucks/terminal-config` + and worktree `../pmacs-terminal-config` retained. Profiles, scrollback, + a per-terminal configurable escape key, and the `C-c t` opening + binding; no protocol change. Main was integrated **twice** during the + single review round (`ccf29e3`, then `c93f9ee` after the first merge + left the PR conflicting) — see the no-CI-while-conflicting fact below. - **Stage 2 = `githubsucks/terminal-copy-mode`**, worktree `../pmacs-terminal-copy-mode`, based on `githubsucks/main` @ `cf54270`. Copy mode: `M-x terminal.copy-mode` / `C-c C-t`. @@ -935,10 +744,84 @@ If it does not, stop and repair the remote/fetch configuration. - `pmacs-gpu` itself failed 201/202 once under the same load and passed 202/202 on immediate rerun. -## Bottom-panel lane (Arc 7) — Stage 1 MERGED; Stage 2 IN FRAMING +## Bottom-panel lane (Arc 7) — Stages 1, 2A + framing MERGED; 2B is next -Stage 1 is on `main`. **Stage 2 is in framing**, no implementation in -flight. +Stage 1, the Stage 2 framing, and Stage 2A are all on `main`. **Stage 2B +has not started.** + +- **Stage 2A MERGED as #177** (`main` @ `0a3fcd1`, 2026-07-26, all twelve + checks green at `8424172`, three review rounds). Branch + `githubsucks/bottom-panel-stage2a` and worktree `../pmacs-bp-stage2a` + are retained and carry nothing unmerged. Five commits: the classified + census routing, the painter extraction + acceptance, the lane record, + then 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. +- **Stage 2B is approved and unstarted.** It branches from `main`, **not + stacked on 2A**, per the framing §9. Scope: protocol v21, the daemon + panel projection, the GPU band, and the negotiated `panel_capable` + flip. `docs/bottom-panel-stage2-framing.md` §7.2 carries its five + acceptance criteria (A2B-1..5) plus the reassertion of parent + criterion 52, and §8 records **no open items**, so 2B needs no further + framing round. Its sharpest trap is §5.3's three-boundary split: the + GPU `text_area_bottom` is `status_band_top`, + `geometry_capacity_bottom` and `document_text_bottom` at once, and a + blanket rewrite moves the status chrome along with the document while + still satisfying an "everything moved" assertion — hence A2B-4's + contrast form. +- Verification on the merge result: `cargo fmt --check` clean; strict + 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. +- **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, 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` + rejected the buffer), the missing A2A-2 two-context fan-out, a census + suite that asserted the AUTHORITY rather than the CONSUMERS, and the + missing main integration. **Two of the new pins were themselves + vacuous on the first attempt** — the dispatcher test passed because an + unregistered session is dropped at `daemon.rs:1962` before reaching + the aligner, and the painter test was a fixed-point check that + survived deleting `text_view.render`. Both now fail under their own + bite. +- **`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 @@ -1047,6 +930,23 @@ 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. - **Inline-math slice — MERGED as #158** (`main` @ `5aa9044`, 2026-07-25). Detect → parse → layout → draw for `$…$`, entirely inside `pmacs-gpu`, no protocol change. Verified by the user's manual pass on diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index b2d0aeb..45ee353 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,8 +1,18 @@ # 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), -the dired arc's Stage 0, and COHERENCE.md (#163), Lean 4 Stage 1 (#160), the +**Last updated: 2026-07-26, after Lean 4 Stage 4a (#179) — the typed-edit +consumer chain — and bottom-panel Stage 2A (#177), the classified census +routing that makes every Projection-class consumer ask +`primary_document_window`; following the bottom-panel Stage 2 framing +(#175), terminal configuration Stage 1 (#173) — profiles, scrollback, a +per-terminal configurable escape key, and the `C-c t` opening binding — +Lean 4 stages 3a and 3b (#167, #170), pmacs' first Lean language server; +the GPU terminal input fix (#166), the double terminal-layout sync that +made a GPU terminal untypable; the CRDT undo repro (#157), the +inline-math landed-doc refresh (#172), the inline-math slice (#158), the +first mathematical typesetting in pmacs; dired Stage 1 (#165), Lean 4 +Stage 2 (#161), the dired framing pair (#163/#164), find-file (#162) — +the dired arc's Stage 0 — 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 GPU initial-target doc refresh (#152); and before that GPU @@ -25,15 +35,19 @@ 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` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel Stage 2A + #177, the bottom-panel Stage 2 framing #175, terminal configuration + Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the CRDT undo repro + #157, the inline-math landed-doc refresh #172, 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** — bottom-panel Stage 2A deliberately carries no wire change; + v21 arrives with Stage 2B. 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 +56,72 @@ 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. + - **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 frontend. **No protocol change (still v20); the whole slice lives in @@ -691,6 +771,44 @@ commands, read `docs/active-work.md` immediately after this file. 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 @@ -817,6 +935,34 @@ final variant — its own round-trip cannot detect a discriminant shift. ## 5. Hard-won ops lessons +- **A test that skips on a missing precondition reports `ok`, and a gate log + cannot tell that apart from a pass.** `vterm_stage3_acceptance::a37` — the + only acceptance driving a real daemon, a real PTY and a real wgpu render + together — derives `pmacs-gpu` from `CARGO_BIN_EXE_pmacs` and, when that + binary is absent from the target directory, prints a skip and returns. + A fresh worktree reports the suite 9/9 **in 0.17 s having never run it**; + a real run takes ~4 s. `PMACS_REQUIRE_GPU=1` is what promotes the skip to + a failure, and the standing gate list applies that flag to + `cargo test -p pmacs-gpu`, a *different package*. Two habits follow: + build the workspace before believing any suite that reaches for a sibling + binary, and **judge such a suite by its elapsed time**, not its verdict. +- **Before attributing a red test to your branch, run it on the merge base.** + `a37` failed on the #173 branch, which looked like a regression; it failed + identically on the PR's own base and on two intermediate commits, and had + *passed* on that same base twenty minutes earlier. The variable was machine + load from a second agent compiling continuously. Load-sensitive tests make + both verdicts uninformative in isolation, so the base-commit run is the + cheapest way to tell a regression from weather — and it is much cheaper + than the bisect it replaces. +- **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/lean4-mode-framing.md b/docs/lean4-mode-framing.md index ec62980..c4a32e5 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`, @@ -45,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. +Revision 1 — initial. Current revision: **8**. ### Round 1 (rev 1 → rev 2) @@ -283,10 +284,230 @@ 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. (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. *(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 + 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. + + *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** + (`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. + +### 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. + +### 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 -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 +536,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 +635,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 +716,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 +786,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 +800,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 +922,129 @@ 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`, `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 +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). + +**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 +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.** 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 +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 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 ### Q#LN1 — Bundle `arborium-lean` 2.18; reject `tree-sitter-lean4` @@ -911,7 +1276,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 +1467,295 @@ 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: - (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.) +| 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–46h | +| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** | -**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. +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`. -Expansion semantics (matching vscode-lean4 and `lean4-input`): +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. -- `\` 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()`. +**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. -### Q#LN11 — Stage 4 data: vendor the table, generated, attributed +**What 4a deliberately does not do.** It does not change the `all-must- +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 `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 | +| 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, 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. + +**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 + +`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, + 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. +- If no key extends `text .. c`, expand `text` **first**, then let `c` + land normally — the chain does *not* claim `c`. +- **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 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()` 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` +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 +1992,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 +2011,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 +2038,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 +2091,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 +2138,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 +2384,83 @@ 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. + +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. + +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 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** + +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#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 +2470,87 @@ 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. +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 + `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 — 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** @@ -1847,9 +2616,9 @@ 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 + 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 @@ -1895,8 +2664,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 +2697,60 @@ 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 8) + +**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 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 +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." diff --git a/docs/vterm-framing.md b/docs/vterm-framing.md index b1124c0..7d4ca02 100644 --- a/docs/vterm-framing.md +++ b/docs/vterm-framing.md @@ -1674,6 +1674,64 @@ 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`. + +**And `a37` is darker still than that count implies: it reports `ok` without +running whenever `pmacs-gpu` is absent from the same target directory** +(measured 2026-07-26 while gating #173). It derives the sibling binary from +`CARGO_BIN_EXE_pmacs` and, finding nothing, prints a skip notice and returns. +A fresh worktree reports the suite 9/9 in 0.17 s having executed the arc's +only real-daemon/real-PTY/real-wgpu path zero times; a genuine run takes +about four seconds. `PMACS_REQUIRE_GPU=1` is the only thing that turns that +skip into a failure, and the standing gate list applies that flag to +`cargo test -p pmacs-gpu`, a different package. So the audit's claim that +"only 3 of 9 Stage 3 tests drive a real daemon" was itself optimistic — +**on a target directory without the frontend binary the honest number is 2**, +and nothing in the gate log says so. It is also load-sensitive: it passed and +then failed at the same commit twenty minutes apart under machine +contention. Criterion 22's unpinned "without thrash" and this are the arc's +two standing verification gaps. + +**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 diff --git a/src/daemon.rs b/src/daemon.rs index 9ac8256..84716eb 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -1145,10 +1145,7 @@ fn dispatcher_loop( .session_state(*fid) .is_some_and(|s| s.negotiated_capabilities.semantic_render) { - let active_now = { - let core = editor.core.borrow(); - core.active_window_for(*fid).map(|w| w.buffer_id) - }; + 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) { @@ -1429,17 +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) { - let core = editor.core.borrow(); - if let Some(window) = core.active_window_for(*fid) { - 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; } } } @@ -2038,12 +2033,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 +2056,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 +2125,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 +2367,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 +2507,7 @@ 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); + let displays_buffer = peer_displays_buffer_as_document(editor, *peer_id, buffer_id); if !displays_buffer { continue; } @@ -2936,32 +2946,88 @@ 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( +/// 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). +/// +/// **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. + // Unknown buffer — leave the window as-is, and report + // FAILURE. Returning the window here would let a stale or + // forged `Pointer` naming a dead buffer take focus out of a + // panel via #8's activation, *before* `dispatch_pointer` + // rejects the mismatched buffer. Alignment did not happen, + // so no caller may treat this as a document gesture. + return None; }; - 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 +3035,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( @@ -3399,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 @@ -4385,7 +4559,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. @@ -4423,7 +4597,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 @@ -4582,4 +4758,381 @@ mod tests { "the panel was not overwritten with the target" ); } + + /// Bottom-panel §1.3 #8, review round 1 finding 1: a STALE document + /// `Pointer` must not steal focus out of a panel. + /// + /// Driven through `handle_dispatcher_event` — the real dispatcher + /// seam — because the defect lived in the *pair* of alignment and + /// activation, not in either alone. `align_primary_document_window` + /// once returned the window even when the named buffer was gone, so + /// #8's activation focused the document before `dispatch_pointer` + /// ever rejected the mismatched buffer. + #[cfg(feature = "crdt")] + #[test] + fn a_stale_document_pointer_does_not_steal_focus_from_a_panel() { + use crate::editor::EditorState; + use crate::protocol::FrontendId; + use crate::window::{FrontendView, Layout, LayoutNode, Orientation, Window, WindowParams}; + use pmacs_protocol::{Modifiers, PointerKind}; + + let mut editor = EditorState::new(); + let fid = FrontendId(88); + + // One document window + one focused bottom panel. + let (document, panel, dead_buffer) = { + let mut core = editor.core.borrow_mut(); + let doc_buf = core.active_window().buffer_id; + let panel_buf = core.registry.borrow_mut().create("*panel*"); + // A buffer id that names nothing: the stale-pointer payload. + let dead_buffer = crate::buffer::BufferId::from_raw(999_999); + + let document = crate::window::WindowId::next(); + let panel_id = 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::new(panel_id, panel_buf, panel_view); + let mut params = WindowParams::default(); + params.side = Some(crate::window::Side::Bottom); + params.fixed_rows = Some(4); + panel.params = params; + core.windows.insert(panel_id, panel); + core.register_frontend_view( + fid, + FrontendView { + layout: Layout { + root: LayoutNode::Split { + orientation: Orientation::Horizontal, + children: vec![LayoutNode::Leaf(document), LayoutNode::Leaf(panel_id)], + weights: vec![1, 1], + }, + }, + active: panel_id, + fold_projection: false, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + (document, panel_id, dead_buffer) + }; + + 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(); + // The dispatcher drops any event from an UNINSTALLED session + // (#148's defense-in-depth membership check), so the session must + // be registered or this test passes for the wrong reason — it did, + // on the first attempt. + 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: FrontendEvent::Pointer { + frontend_id: fid, + buffer_id: dead_buffer, + byte: 0, + kind: PointerKind::Down, + mods: Modifiers::default(), + }, + }, + &mut editor, + &mut render_states, + &mut semantic_states, + &mut streams, + &mut term_sizes, + &mut last_idle, + &mut last_active, + &mut bells, + &mut registry, + ); + + assert_eq!( + editor.core.borrow().views[&fid].active, + panel, + "a stale Pointer naming a dead buffer must NOT move focus out of the panel" + ); + assert_ne!( + editor.core.borrow().views[&fid].active, + document, + "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 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 + /// 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/editor.rs b/src/editor.rs index dcff55a..a19971e 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"), @@ -1409,9 +1424,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; } @@ -1540,6 +1562,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 @@ -3220,6 +3252,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. /// @@ -3329,6 +3525,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) @@ -3336,36 +3537,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()); } } @@ -3417,114 +3589,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/src/semantic_render.rs b/src/semantic_render.rs index 65750d3..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,7 +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 { - self.emit_statusline_segments(evaluation, &mut out); + self.emit_statusline_segments(evaluation, statusline_document_window, &mut out); } out } @@ -855,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(), @@ -881,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() { @@ -905,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) } @@ -920,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)); @@ -929,7 +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 { - self.emit_statusline_segments(evaluation, &mut out); + self.emit_statusline_segments(evaluation, statusline_document_window, &mut out); } out } @@ -941,6 +978,7 @@ impl SemanticRenderState { fn emit_statusline_segments( &mut self, evaluation: StatuslineEvaluation, + document_window: Option, out: &mut Vec, ) { let to_wire = |segments: Vec| { @@ -955,10 +993,16 @@ impl SemanticRenderState { let frontend_id = self.frontend_id; match evaluation.outcome { StatuslineEvaluationOutcome::Ready(windows) => { - if let Some(window) = windows - .into_iter() - .find(|window| window.context.frontend_id == frontend_id) - { + // Bottom-panel A2A-2: the fan-out now yields the primary + // document AND the visible side window, so the wire + // segments must be selected by WINDOW IDENTITY. Taking + // "the first context for my frontend" would silently + // depend on capture order and could ship the panel's + // mode-line text as the document status band. + if let Some(window) = windows.into_iter().find(|window| { + window.context.frontend_id == frontend_id + && Some(window.context.window_id) == document_window + }) { self.emit_statusline_payload( window.context.buffer_id, to_wire(window.left), @@ -970,10 +1014,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); } } @@ -1345,9 +1397,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 +1759,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) @@ -2916,6 +2977,7 @@ mod tests { ), new_failures: Vec::new(), }, + None, &mut stale, ); assert!(stale.is_empty(), "phase-1 stale evaluation emits nothing"); @@ -2924,11 +2986,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, }], @@ -2936,13 +3002,13 @@ mod tests { new_failures: Vec::new(), }; let mut replacement = Vec::new(); - semantic.emit_statusline_segments(invalidated(), &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(), &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 d11c885..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, @@ -639,9 +654,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); @@ -649,12 +675,46 @@ fn capture_target_contexts( if window.buffer_id != declared_buffer { return Err(StatuslineNoMessageReason::DeclaredBufferMismatch); } - Ok(vec![StatuslineContext { + let mut contexts = vec![StatuslineContext { frontend_id, window_id: window.id, buffer_id: window.buffer_id, - active: true, - }]) + active: window.id == view.active, + }]; + // Bottom-panel Q#BP8 / A2A-2 — the semantic fan-out is the + // primary document PLUS the frontend's visible side window, + // and nothing else: unprojected document splits run no + // callbacks. The document result feeds the semantic + // `StatuslineSegments`; the side result paints in the panel's + // own mode line. + // + // A derived-hidden side window is omitted (Q#BP2b): it has no + // mode line to paint this frame, so evaluating providers for + // it would invoke callbacks for a surface nobody can see. + if !view.panel_hidden { + for side_id in view.layout.iter_ids() { + if side_id == window.id { + continue; + } + let Some(side) = core.windows.get(&side_id) else { + return Err(StatuslineNoMessageReason::ContextUnavailable); + }; + if !side.is_side() { + continue; + } + if buffers.get(side.buffer_id).is_err() { + return Err(StatuslineNoMessageReason::BufferUnavailable); + } + contexts.push(StatuslineContext { + frontend_id, + window_id: side.id, + buffer_id: side.buffer_id, + // Same rule as the document context: ACTUAL focus. + active: side.id == view.active, + }); + } + } + Ok(contexts) } } } diff --git a/src/window.rs b/src/window.rs index b66499e..2ac0087 100644 --- a/src/window.rs +++ b/src/window.rs @@ -558,8 +558,19 @@ pub struct FrontendView { /// store. Reckoning in visible lines unconditionally would make that /// GPU session's cursor skip lines it is still showing, so every /// command/event-time visible-line reckoning is gated on the - /// **acting** frontend's flag. Render-time clamps need no gate: a - /// semantic session never enters `paint_frame`. + /// **acting** frontend's flag. + /// + /// **Render-time clamps used to need no gate, on the premise that a + /// semantic session never enters `paint_frame`. The bottom-panel + /// band breaks that premise** (Q#BP17): the daemon projects a + /// semantic frontend's side window through the same per-window + /// painter. So the extracted painters + /// (`prepare_window_cursor_visible`, `paint_window_content`) take the + /// visible-line map as a **parameter**, and the panel path passes + /// `None` when the *owning* frontend's `fold_projection` is false. + /// That path must not call `EditorCore::fold_map_for_window`, which + /// gates on the **active** frontend — correct for command-time + /// reckoning, wrong for painting another frontend's panel. /// /// Set at attach from the negotiated selected-render bit (grid ⇒ /// `true`, semantic ⇒ `false`), cleared with the view at detach, and diff --git a/tests/bottom_panel_stage2a_acceptance.rs b/tests/bottom_panel_stage2a_acceptance.rs new file mode 100644 index 0000000..d39d804 --- /dev/null +++ b/tests/bottom_panel_stage2a_acceptance.rs @@ -0,0 +1,898 @@ +// 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_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] + .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) => { + // A2A-2: the semantic fan-out captures the primary document + // AND the visible side window — two contexts, not one. + assert_eq!( + windows.len(), + 2, + "the semantic-layout target must capture document + visible side window" + ); + let side = windows + .iter() + .find(|w| w.context.window_id != document) + .expect("a side-window context"); + assert!( + side.context.active, + "the focused panel's own context reports active = true" + ); + 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, {})", + ); + + // The gutter only paints when line numbers are on, so turn them on + // rather than dropping the assertion. + { + let mut core = s.core.borrow_mut(); + let active = core.views[&FrontendId::LOCAL].active; + core.windows.get_mut(&active).unwrap().line_numbers = + pmacs::window::LineNumberMode::Absolute; + } + + 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"); + + // Review round 1, finding 5: a fixed-point check alone is VACUOUS — + // deleting `text_view.render` leaves it green. Assert the extracted + // painter actually produced each of its four outputs. + let rows = |cells: &[pmacs::cell::Cell]| -> Vec { + (0..ROWS as usize) + .map(|r| { + (0..COLS as usize) + .map(|c| match &cells[r * COLS as usize + c].glyph { + pmacs::cell::Glyph::Char(ch) => *ch, + _ => ' ', + }) + .collect::() + }) + .collect() + }; + let painted = rows(&cells_a); + + // TEXT: the buffer's content reached the grid. + assert!( + painted.iter().any(|row| row.contains("line")), + "the extracted painter must paint buffer TEXT; got {painted:?}" + ); + // GUTTER: line numbers were painted beside it. + assert!( + painted.iter().any(|row| row.trim_start().starts_with('1')), + "the extracted painter must paint the line-number GUTTER" + ); + // MODE LINE: the window's mode line names its buffer. + assert!( + painted.iter().any(|row| row.contains("*doc*")), + "the extracted painter must paint the window MODE LINE" + ); + // CURSOR: a real caret position came back, not None. + assert!( + cursor_a.is_some(), + "the extraction must still return a caret position" + ); +} + +#[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" + ); +} + +// --------------------------------------------------------------------------- +// A2A-1 at the CONSUMER seam — review round 1, finding 3. +// +// The tests above assert the *authority* (`primary_document_window`). +// That is not sufficient: restoring a producer to `active_window_for` +// leaves every one of them green. These drive the real producers through +// `SemanticRenderState::render_frame` with a panel focused, so a reverted +// routing fails here. +// --------------------------------------------------------------------------- + +/// A semantic frontend that CAN hold a panel. Stage 1 ships +/// `panel_capable = false` for semantic sessions and 2B flips it for a +/// v21-negotiated peer; until then the projection is only reachable with +/// a test-only capable view, which is exactly what the framing's §7.2 +/// says 2B must replace with the real capability flip. +fn semantic_frontend_with_focused_panel( + s: &EditorState, +) -> (FrontendId, WindowId, WindowId, pmacs::buffer::BufferId) { + use pmacs::window::{FrontendView, Layout, LayoutNode, Orientation, Window, WindowParams}; + + let fid = FrontendId(77); + let (doc_win, panel_win, doc_buf) = { + let mut core = s.core.borrow_mut(); + let doc_buf = core.active_window().buffer_id; + let panel_buf = core.registry.borrow_mut().create("*panel*"); + + let doc_win = WindowId::next(); + let panel_win = WindowId::next(); + let doc_view = { + let reg = core.registry.borrow(); + pmacs::text_view::TextView::new(reg.get(doc_buf).expect("document buffer")) + }; + let panel_view = { + let reg = core.registry.borrow(); + pmacs::text_view::TextView::new(reg.get(panel_buf).expect("panel buffer")) + }; + core.windows + .insert(doc_win, Window::new(doc_win, doc_buf, doc_view)); + let mut panel = Window::new(panel_win, panel_buf, panel_view); + let mut params = WindowParams::default(); + params.side = Some(Side::Bottom); + params.fixed_rows = Some(4); + panel.params = params; + core.windows.insert(panel_win, panel); + + core.register_frontend_view( + fid, + FrontendView { + layout: Layout { + root: LayoutNode::Split { + orientation: Orientation::Horizontal, + children: vec![LayoutNode::Leaf(doc_win), LayoutNode::Leaf(panel_win)], + weights: vec![1, 1], + }, + }, + // The panel owns focus; the document is the projection. + active: panel_win, + fold_projection: false, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + (doc_win, panel_win, doc_buf) + }; + s.sync_frame_geometry(fid, CellSize::new(ROWS, COLS)); + (fid, doc_win, panel_win, doc_buf) +} + +#[test] +fn consumer_line_numbers_follow_the_document_not_the_focused_panel() { + use pmacs::protocol::{ByteRange, InstanceMessage}; + use pmacs::semantic_render::SemanticRenderState; + use pmacs::window::LineNumberMode; + + let s = editor(); + let (fid, doc_win, panel_win, doc_buf) = semantic_frontend_with_focused_panel(&s); + + // Make the two windows DISAGREE, so the emitted mode identifies + // which window the producer read (§1.3 #4). + { + let mut core = s.core.borrow_mut(); + core.windows.get_mut(&doc_win).unwrap().line_numbers = LineNumberMode::Absolute; + core.windows.get_mut(&panel_win).unwrap().line_numbers = LineNumberMode::Off; + } + + let mut sem = SemanticRenderState::new(fid); + sem.set_viewport(doc_buf, ByteRange { start: 0, end: 0 }, 0); + let msgs = sem.render_frame(&s); + + let mode = msgs.iter().find_map(|m| match m { + InstanceMessage::LineNumbers { mode, .. } => Some(*mode), + _ => None, + }); + assert_eq!( + mode, + Some(pmacs::protocol::LineNumberMode::Absolute), + "LineNumbers must describe the DOCUMENT window's mode, not the focused panel's" + ); +} + +#[test] +fn consumer_statusline_segments_carry_the_document_payload_not_the_panel() { + use pmacs::protocol::{ByteRange, InstanceMessage}; + use pmacs::semantic_render::SemanticRenderState; + + // §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 panel_buf = { + let core = s.core.borrow(); + let panel = side_window_of(&core, fid).expect("panel"); + core.windows[&panel].buffer_id + }; + + // 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); + 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.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_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, term_buf), + "the DOCUMENT window's terminal must be declarable while the panel owns focus" + ); + 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" + ); +} + +#[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:?}" + ); +} diff --git a/tests/typed_edit_chain_acceptance.rs b/tests/typed_edit_chain_acceptance.rs new file mode 100644 index 0000000..8ff9c13 --- /dev/null +++ b/tests/typed_edit_chain_acceptance.rs @@ -0,0 +1,735 @@ +//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a, +//! 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, 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 +//! 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, + } + "#, + ); + + // 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"); + 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 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 + .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:?}" + ); + } +} + +#[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 +// --------------------------------------------------------------------------- + +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)" + ); +}