Merge remote-tracking branch 'githubsucks/main' into terminal-copy-mode

# Conflicts:
#	docs/active-work.md
This commit is contained in:
Levi Neuwirth 2026-07-26 14:59:09 -04:00
commit 1b44c69a53
14 changed files with 4355 additions and 807 deletions

View File

@ -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,
}

View File

@ -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 = "<unprintable error>"
end
pcall(ed.set_status,
"typed-edit consumer '" .. c.name .. "' failed: " .. rendered)
elseif claimed then
return
end
end
end)

View File

@ -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#LN119), 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 1321).
- **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 13 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

View File

@ -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

View File

@ -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

File diff suppressed because it is too large Load Diff

View File

@ -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

View File

@ -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<crate::buffer::BufferId> {
// 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<crate::buffer::BufferId> {
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<crate::window::WindowId> {
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,
&registry,
&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,
&registry,
&mut streams,
&mut HashMap::new(),
);
client
.set_read_timeout(Some(Duration::from_millis(50)))
.expect("timeout");
assert!(
read_message::<InstanceMessage>(&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"
);
}
}

View File

@ -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<TerminalViewKey> {
// 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<std::sync::Mutex<crate::diag::DiagnosticStore>>,
) {
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);

View File

@ -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<StatuslineEvaluation>,
statusline_document_window: Option<crate::window::WindowId>,
) -> Vec<InstanceMessage> {
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<crate::window::WindowId>,
out: &mut Vec<InstanceMessage>,
) {
let to_wire = |segments: Vec<crate::statusline::EvaluatedStatuslineSegment>| {
@ -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<InstanceMessage> {
// 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"

View File

@ -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)
}
}
}

View File

@ -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

View File

@ -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<WindowId> {
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<WindowId> {
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<String> {
(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::<String>()
})
.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::<usize>(),
),
_ => 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:?}"
);
}

View File

@ -0,0 +1,735 @@
//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a,
//! docs/lean4-mode-framing.md Q#LN10, criteria 46a46h).
//!
//! 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<T: mlua::FromLuaMulti>(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("<unprintable error>"),
"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<String> {
let Ok(raw) = std::fs::read_to_string(sink) else {
return Vec::new();
};
raw.lines()
.filter_map(|l| serde_json::from_str::<serde_json::Value>(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::<StateDir>();
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)"
);
}