neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'main' into docs-dired-stage1-landed 

Three conflicts, resolved by taking the newer statement on each side
rather than either side wholesale:

- COHERENCE.md journey row 7 keeps this branch's text (dired #165 is
  merged, not a PR); row 8 takes main's, which records terminal config
  #173.
- The ledger's canonical-base line takes main's d400f30 anchor and keeps
  this branch's caveat about lanes that name an older base.
- agent-handoff's two anchors take main's d400f30 wording, with the CRDT
  undo repro #157 and the inline-math landed-doc refresh #172 added
  back — both are merged and main's summary had dropped them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RuhVYUPHXMHG8r2z4tsDPR
This commit is contained in:
Levi Neuwirth 2026-07-26 14:40:13 -04:00
parent 2b42204693 a27f6467ea
commit b123c0b9fe
26 changed files with 10340 additions and 623 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
COHERENCE.md
View File

@ -368,7 +368,7 @@ Full verdict table:
| 5 | Edit | **Works** | Full CUA + Emacs keymap in 161 lines (`builtin/keymaps/default.lua`); isearch, query-replace, kill ring, undo/redo, auto-indent/pair/comment, atomic save. Genuinely excellent zero-config |
| 6 | Language intelligence | **Partial** | Rust grammar bundled and auto-attaches; rust-analyzer preconfigured (`builtin/runtime/lsp.lua:44-52`) — but a missing binary fails silently (§1.2) and highlighting masks it. No LSP status command exists to diagnose |
| 7 | Find symbol / file | **File: fixed (open by path merged #162; browsing #165). Symbol: works but undiscoverable** | No find-file/dired/picker existed at audit. Now `C-x C-f` opens a known path and `C-x d` / `C-x C-j` browse (flat listing, `dired` mode keymap); `M-.`/`M-?`/`C-c o` still bound but advertised nowhere and server-gated; no workspace-symbol command; `pmacs.index.*` has no UI |
| 8 | Open terminal | **Works but undiscoverable** | Full PTY with scrollback + modeline segment — reachable only as `M-x terminal`, no keybinding. *Was broken outright on the GPU frontend until the double terminal-layout sync was fixed: the child took a `SIGWINCH` storm at tick cadence, so typing into it was impossible while output still flowed.* |
| 8 | Open terminal | **Works** | Full PTY with scrollback + modeline segment, bound to `C-c t` and configurable through three registered settings (`terminal.default-profile`, `terminal.scrollback-rows`, `terminal.escape-key`) plus named `pmacs.terminal.profiles` (PR #173). Named limitation: `C-c t` is unreachable from *inside* a terminal window, where `C-c` is consumed as the escape — `M-x terminal` still works there. *Was broken outright on the GPU frontend until the double terminal-layout sync was fixed: the child took a `SIGWINCH` storm at tick cadence, so typing into it was impossible while output still flowed.* |
| 9 | Build / test | **Partial** | `M-x compile.run` works, defaults cwd to detected project root, parses Rust `-->` errors — but no keybinding, an **empty first prompt** (`initial = last and last.cmdline or ""`, `builtin/runtime/compile.lua:1134-1138`), and no `cargo build`/`cargo test` suggestion despite `ProjectKind::Cargo` existing (`src/project.rs:77`) |
| 10 | Inspect error | **Partial (good once reached)** | `E:n W:n` modeline counts, underlines, `M-g n/p` + ``C-x ` `` walking a unified compile/grep/diag source, message echo, `RET` visits. Gated entirely on step 6 or 9 succeeding first |
| 11 | See background work | **Works but undiscoverable** | `*workers*` view via `M-x editor.list-workers`; `C-c C-k` cancel-at-point. No keybinding, no statusline spinner/progress indicator anywhere (§9) |
@ -379,6 +379,13 @@ A journey observation worth keeping verbatim from the audit:
C-M-s` opens all folds, while opening a file, opening a terminal, and
running a build have no bindings at all.
Two of that observation's three examples have since been answered —
opening a file by `C-x C-f` (#162) and opening a terminal by `C-c t`
(#173). **Running a build still has no binding**, and the underlying
inversion is a standing bias in how new work gets bound, not three
isolated omissions: the quote stays as written because it names the
pattern, and the pattern is not retired until step 9 is.
---
## 3. A Strong Zero-Configuration State
@ -639,7 +646,7 @@ Everything funnels through one function: `EditorInstance::dispatch_key`
| 3 | query-replace | `editor.rs:945` | `QueryReplaceKey::from_chord` (`editor.rs:2967`) | **full shadow** |
| 4 | Minibuffer | `editor.rs:951` | `MinibufferAction::from_chord` (`src/minibuffer.rs:468`) | **full shadow** |
| 5 | Completion popup | `editor.rs:958-971` | `CompletionPopupKey::from_chord` (`editor.rs:3056`) | **partial shadow** (control chords only; skipped while a multi-key prefix is pending) |
| 6 | Terminal transport + `C-c` escape | `editor.rs:973-1010` | `is_terminal_escape_chord` (`editor.rs:4355`) | **partial, transport-level** |
| 6 | Terminal transport + configurable escape | `editor.rs:973-1010` | `EditorState::terminal_escape_chord` → `TerminalManager::escape_chord` (`src/terminal/session.rs`) | **partial, transport-level** |
| 7 | Ordinary dispatch | `editor.rs:1018-1032` | `KeymapStack::resolve` | the only inspectable layer |
Facts that define the gap:
@ -647,8 +654,10 @@ Facts that define the gap:
- **Full shadows eat every key**, including unrecognized ones (each
decoder has an `Ignore`/`Dismiss` fallback arm). While a terminal
buffer is focused and unescaped, *all* keys encode to the child —
`C-c`-leading user bindings are **structurally unreachable** in a
terminal buffer.
bindings led by the escape chord are **structurally unreachable** in
a terminal buffer. Since #173 that chord is `terminal.escape-key`
rather than a hardcoded `C-c`, so a user can *move* which prefix is
eaten; they cannot make the shadow stop eating one.
- **No transient-keymap mechanism exists to migrate to.** `KeymapStack`
has exactly three fixed scopes — `Buffer(BufferId)`, `Mode(String)`,
`Global` (`src/keymap_stack.rs:37-44`); resolution order buffer →
@ -1013,20 +1022,29 @@ layering, provenance, and adoption have not followed.**
`ConfigValue`s; `describe-setting`'s "Source:" names where `define()`
ran. The inspection view sketched above is currently impossible to
render.
- **Adoption is five settings**: `editing.auto-pair` (pair.lua),
- **Adoption is eight settings**: `editing.auto-pair` (pair.lua),
`editing.trim-on-save` (editops.lua), `autosave.interval-ms`
(autosave.lua), `window.panel-height` + `window.min-height`
(window.lua). Everything else a user might set — theme, fonts, LSP
(window.lua), and `terminal.default-profile` +
`terminal.scrollback-rows` + `terminal.escape-key` (terminal.lua,
#173). Everything else a user might set — theme, fonts, LSP
server config, killring size, recentf/saveplace/desktop enables,
pair sets, comment strings, `pmacs.parse.*` — lives in raw Lua
outside the registry and is therefore invisible to `describe-setting`
and any future settings UI. The migration list is already written:
`docs/config-registry-framing.md` "named deferrals" (table-valued
settings are the hard prerequisite for LSP/pair/comment tables).
- **The table-valued gap now has a named, shipped instance.**
`pmacs.terminal.profiles` (#173) is a raw Lua table sitting beside
three registered scalars *for the same feature*, because a profile is
inherently `{ command, args, cwd, env }` and the registry stores four
scalars. It is the clearest evidence yet that table-valued settings
are the blocking prerequisite: the terminal is now half-registered,
and no settings UI can render the half that matters most.
- **No persistence**: settings changed at runtime do not survive
restart (the `custom-file` split-brain question is a named deferral).
- The three-level separation holds in principle today (registry /
hooks+keymaps / packages), but with five settings registered, level 1
hooks+keymaps / packages), but with eight settings registered, level 1
is effectively empty — users need executable Lua for nearly every
ordinary preference, which is the exact failure the section warns
about.

24
builtin/runtime/fs.lua
View File

@ -325,4 +325,28 @@ function fs.watch(path, callback, opts)
return watch
end
-- pmacs.fs.canonicalize(path) -> string | nil
--
-- Arc 8 Stage 3a (framing Q#LN20). The **only synchronous** function on
-- this module, and deliberately so: its consumer is a function-valued
-- `pmacs.lsp.config[lang].root`, invoked from `ensure_server` <-
-- `attach_buffer` <- the `buffer.after-load` hook, where there is no
-- coroutine and therefore nothing to `:await()` on. Every other
-- primitive here returns a Handle; this one cannot, or it would be
-- unusable at the one call site that needs it — the same trap
-- `pmacs.fs.stat` falls into for that caller.
--
-- Resolves symlinks and `.` / `..`, returning an absolute path, or nil
-- if the path does not exist or cannot be resolved. Nil is a normal
-- answer, not an error: callers routinely ask about paths that may have
-- been deleted.
--
-- Why it exists: a configured LSP root reaches `file_uri_for` verbatim
-- and that URI is the server-affinity key (PR #161), so one project
-- opened through a symlink and through its real path would otherwise
-- spawn two servers. `pmacs.editor.file_path()` collapses `.` and `..`
-- lexically but leaves symlinks intact, so the resolver cannot get a
-- canonical path any other way.
fs.canonicalize = pmacs._fs.canonicalize
pmacs.fs = fs

750
builtin/runtime/lean.lua Normal file
View File

@ -0,0 +1,750 @@
-- builtin/runtime/lean.lua --- Arc 8 Stage 3b: the Lean 4 language server.
--
-- Framing: `docs/lean4-mode-framing.md` Q#LN7 (lake serve + probe +
-- fallback latch), Q#LN8 (Lake-aware outermost root), Q#LN16
-- (waitForDiagnostics). Stage 1 shipped the grammar, mode, comment
-- strings and pair set; Stage 3a shipped the notification/response
-- seams and `pmacs.fs.canonicalize` this file consumes.
--
-- Loaded after `lsp.lua`, which owns `pmacs.lsp.config` and the drain.
local M = {}
-- Q#LN8 — the Lake-aware root -----------------------------------------
--
-- `pmacs.project.detect` cannot express this rule. It is innermost-wins
-- by construction, and a Lake package's `lean-toolchain` sits at the
-- OUTERMOST level: a file under `<pkg>/.lake/packages/dep/Foo.lean`
-- belongs to `<pkg>`'s server, not to `dep`'s, because `lake serve` is
-- bound to one package and analyzes its dependencies from inside it.
-- Inverting `detect` globally would change Rust/Go/Node roots for every
-- user, so the rule lives here as a function-valued `config.root` —
-- the generalization Stage 2 (#161) added for exactly this.
-- The marker test, and the two ways to get it wrong.
--
-- `pmacs.fs.stat` is UNUSABLE here: it returns an awaitable handle
-- (`fs.lua`), and this runs synchronously inside `ensure_server` <-
-- `attach_buffer` <- the `buffer.after-load` hook, where there is no
-- coroutine to await on. The Lua stdlib's `io.open` is the only
-- synchronous existence check available.
--
-- But `io.open` alone is wrong in BOTH directions:
-- * it SUCCEEDS on a directory (probed), so a truthiness test would
-- accept a `lean-toolchain` directory as a marker; and
-- * requiring a non-nil read rejects an EMPTY `lean-toolchain`, which
-- is a legitimate marker — `locate-dominating-file` semantics are
-- existence, not content.
-- The discriminator is `read`'s SECOND return (probed on LuaJIT 2.1):
-- file with content -> "l", no error -> marker
-- empty file -> nil, NO error -> marker
-- directory -> nil, "Is a directory" -> decline
-- missing -> io.open returns nil -> decline
-- so: decline only on a non-nil `err`. This needs no per-platform
-- re-probe, because both directory behaviors are declines — a platform
-- whose `fopen` refuses directories fails at `io.open` instead. There
-- is no platform where a directory both opens and yields a byte.
local function has_toolchain(dir)
local f = io.open(dir .. "/lean-toolchain", "r")
if not f then return false end
local _, err = f:read(1)
f:close()
return err == nil
end
local function parent_of(dir)
local up = dir:match("^(.*)/[^/]+$")
if up == nil or up == dir or up == "" then return nil end
return up
end
-- The walk stops at `pmacs.project.search_boundary()`. Not politeness:
-- `detect_project_within` (`src/project.rs`) exists precisely so a
-- stray marker above a temp fixture cannot leak into detection, and a
-- Lua walk that ignored the boundary would break that contract — and
-- make acceptance 23's outermost assertion non-hermetic against any
-- `lean-toolchain` sitting above the test's tempdir.
local function within_boundary(dir, boundary)
if not boundary then return true end
return dir == boundary or dir:sub(1, #boundary + 1) == boundary .. "/"
end
-- Returns the OUTERMOST ancestor holding a `lean-toolchain`, or nil to
-- decline (which falls through to `pmacs.project.detect`, then the
-- file's own directory).
--
-- **The result is canonical, and must be.** A configured root — which
-- this is — reaches `file_uri_for` verbatim and that URI is the
-- server-affinity key (#161). `pmacs.editor.file_path()` collapses `.`
-- and `..` lexically but leaves symlinks intact, so one package opened
-- through a symlink and through its real path would otherwise spawn two
-- `lake serve` processes. Canonicalizing ONCE up front is enough:
-- every ancestor of a canonical path is itself canonical, since the
-- walk only strips trailing components.
--
-- If canonicalization fails (deleted file, broken symlink) the resolver
-- declines rather than returning a path it cannot vouch for.
function M.root_for(path)
if type(path) ~= "string" then return nil end
local dir = path:match("^(.*)/[^/]*$")
if not dir then return nil end
dir = pmacs.fs.canonicalize(dir)
if not dir then return nil end
local boundary
local ok, b = pcall(pmacs.project.search_boundary)
if ok then boundary = b end
-- The boundary is canonicalized at set time (`set_search_boundary`),
-- so comparing it against a canonical `dir` is apples to apples.
local outermost = nil
local cur = dir
while cur and within_boundary(cur, boundary) do
if has_toolchain(cur) then outermost = cur end
cur = parent_of(cur)
end
return outermost
end
-- Q#LN7 — `lake serve`, with a lazy probe and a one-shot latch --------
--
-- `pmacs.lsp.config.lean4` is declarative and must stay cheap: spawning
-- a process at startup for every user, Lean-using or not, is the cost
-- rev 1 refused. So no probe runs here — it runs on the first `.lean`
-- attach, below.
pmacs.lsp.config.lean4 = pmacs.lsp.config.lean4 or {
command = "lake",
args = { "serve" },
root = M.root_for,
-- No `init_options`: `hasWidgets?` defaults to false, which is the
-- correct posture for a client reading plain goals out of standard
-- messages rather than driving the `$/lean/rpc/*` widget stack.
}
-- Session state. The latch is one-shot and never re-arms: a user whose
-- toolchain is broken sees one fallback attempt, not a loop.
local probe = {
started = false, -- the `lake --version` probe has been spawned
latched = false, -- the fallback has fired (or been ruled out)
proc = nil, -- process id of the running probe
out = "", -- accumulated probe stdout
buf_key = nil, -- tostring() of the buffer that started this
watching = nil, -- sid still being polled for die-before-initialize
primary = nil, -- sid the probe's verdict applies to; NOT cleared
-- when the server initializes, because a late
-- version verdict still has to retire it
armed = false, -- the target buffer + primary have been captured
repaired = {}, -- buffer key -> repair attempted (at most once)
repair_attempts = 0, -- COUNT of attach attempts, not distinct buffers:
-- table cardinality cannot tell "once per buffer"
-- from "every tick for one buffer"
fallback_installed = false,
fallback_watches = {}, -- sid key -> sid, each polled die-before-init
fallback_done = {}, -- sid key -> initialized or terminally handled
saw_initialized = false,
}
-- The command as configured, for status text. Hardcoding "lake serve"
-- was untruthful the moment the failure latch became command-agnostic:
-- a user whose `my-lean-wrapper` failed was told `lake serve` did.
local function configured_command()
local cfg = pmacs.lsp.config.lean4
local cmd = cfg and cfg.command
if not cmd then return "the Lean server" end
local args = cfg.args or {}
if #args > 0 then
return "`" .. tostring(cmd) .. " " .. table.concat(args, " ") .. "`"
end
return "`" .. tostring(cmd) .. "`"
end
-- The fallback command, for status text.
local function fallback_name()
local args = M._fallback.args or {}
if #args > 0 then
return "`" .. tostring(M._fallback.command) .. " "
.. table.concat(args, " ") .. "`"
end
return "`" .. tostring(M._fallback.command) .. "`"
end
local function report(msg)
-- COHERENCE §1.2: background work must leave an attributed trace.
-- `pmacs.editor.set_status` is the channel that EXISTS; `pmacs.error`
-- is referenced by fifteen call sites and defined nowhere in
-- production, so it rides along rather than standing alone.
pcall(pmacs.editor.set_status, msg)
if pmacs.error then pcall(pmacs.error, msg) end
end
-- `lake serve` below 3.1.0 starts a server that cannot answer, which is
-- worse than failing: `lean4-mode` probes for exactly this and falls
-- back to `lean --server`. Parses the leading `x.y` of a version line.
-- State kind for the server whose `tostring(id)` is `skey`, or nil if
-- the manager has forgotten it (which is itself a terminal answer).
local function server_state_kind_for_key(skey)
local ok, rows = pcall(pmacs.lsp.list)
if not ok or not rows then return nil end
for _, info in ipairs(rows) do
if tostring(info.id) == skey then
return info.state and info.state.kind
end
end
return nil
end
local function server_state_kind(sid)
return server_state_kind_for_key(tostring(sid))
end
local function version_below_3_1(text)
local major, minor = text:match("(%d+)%.(%d+)")
if not major then return false end
major, minor = tonumber(major), tonumber(minor)
if major < 3 then return true end
return major == 3 and minor < 1
end
-- What the latch falls back TO.
--
-- **Underscored: a test seam, not supported user configuration.** It is
-- a table only so the acceptance suite can point it at a stand-in server
-- and drive the real latch path end to end, instead of asserting on a
-- config mutation that proves nothing about whether a server ever
-- starts. Presenting it as public config would owe framing,
-- documentation, validation and mutation semantics that nothing here
-- provides; users configure Lean through `pmacs.lsp.config.lean4`.
M._fallback = { command = "lean", args = { "--server" } }
local function same_args(a, b)
a, b = a or {}, b or {}
if #a ~= #b then return false end
for i = 1, #a do
if a[i] ~= b[i] then return false end
end
return true
end
-- Swap `command`/`args` ONLY. A wholesale table replacement would
-- silently discard a user's `env` / `settings` / `init_options` / `root`
-- from `init.lua` at exactly the moment they are least likely to notice.
--
-- The only guard is idempotence — already-the-fallback means nothing to
-- do. It deliberately does NOT refuse when the command is user-supplied:
-- the latch fires only when the configured Lean server actually failed
-- to start, and one visible fallback attempt beats leaving the user with
-- no server at all. `probe.latched` is what keeps it to exactly one.
local function swap_to_fallback()
local cfg = pmacs.lsp.config.lean4
if not cfg then return false end
-- Idempotence compares command AND args: the same command with
-- different arguments is not "already applied", and treating it as
-- such would silently skip a swap that still needed to happen.
if cfg.command == M._fallback.command
and same_args(cfg.args, M._fallback.args) then
return false
end
cfg.command = M._fallback.command
cfg.args = M._fallback.args
return true
end
-- Retire the failed server, swap the command, then rebuild the
-- attachment on the buffer that started this.
-- Retire `sid` so it cannot come back. **Which call to use depends on
-- the state, and using the wrong one is worse than doing nothing:**
--
-- * TERMINAL (`crashed` / `stopped`) -> `forget`. It requires a
-- terminal state and removes the client outright, which also drops
-- the `next_restart_at` the crash scheduled. `stop` here would take
-- its not-initialized branch and set `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 it sits in `ShuttingDown` forever:
-- `server_is_live` reads that as LIVE so `attach_buffer` never
-- rebuilds, and `forget` then refuses it for not being terminal.
-- * NON-TERMINAL -> `stop`. `forget` rejects it, and `stop` disables
-- restart and drives the polite shutdown.
--
-- Round 1 skipped the call entirely for terminal servers. That avoided
-- the corruption but left `next_restart_at` armed, so the crashed
-- primary respawned 500ms later and kept respawning underneath the
-- live fallback — invisible to a test that stopped ticking first.
local function retire_server(sid)
local kind = server_state_kind(sid)
if kind == nil then return end
if kind == "crashed" or kind == "stopped" then
pcall(pmacs.lsp.forget, sid)
else
pcall(pmacs.lsp.stop, sid)
end
end
-- Retire EVERY Lean server, not just the one that failed.
--
-- `pmacs.lsp.config.lean4` is a single global entry, so swapping its
-- command invalidates every server spawned from the old one — and
-- Q#LN15 gives one server per project root, so there can be several.
-- Retiring only the server that happened to fail left the others live
-- and every buffer attached to them stranded on a command the config no
-- longer names.
-- Only servers the config-driven path itself produced. A server's label,
-- language, command, and root are all caller-supplied public values; none
-- is an ownership discriminator. `lsp.lua` records the successful spawn
-- in a private origin table, which is the fact this lifecycle may act on.
local function is_derived_server(sid)
local ok, owned = pcall(pmacs.lsp._is_default_server, sid, "lean4")
return ok and owned == true
end
local function retire_derived_lean_servers()
local ok, rows = pcall(pmacs.lsp.list)
if not ok or not rows then return end
local ids = {}
for _, info in ipairs(rows) do
if is_derived_server(info.id) then ids[#ids + 1] = info.id end
end
for _, id in ipairs(ids) do
-- These ids predate the fallback spawn. Mark them handled before
-- retirement so the discovery poll cannot mistake their terminal
-- state for a fallback that failed to initialize.
probe.fallback_done[tostring(id)] = true
retire_server(id)
end
end
local function watch_fallback_server(sid)
if not sid or not is_derived_server(sid) then return end
local key = tostring(sid)
if probe.fallback_done[key] then return end
probe.fallback_watches[key] = sid
end
-- Rebuild the ACTIVE buffer's attachment if it is Lean and stale.
--
-- `_attach_buffer` is an active-buffer-only seam, so a global config
-- swap cannot be applied to every open buffer at once. It is applied
-- lazily instead: whenever a Lean buffer becomes the active one, if its
-- record points at a server that is gone or terminal, it is rebuilt.
--
-- **At most one attempt per buffer.** Without that bound a fallback
-- that also fails to spawn would retry every tick forever with nothing
-- reported — the round-2 defect, which a general repair loop would
-- otherwise reintroduce for every buffer instead of just one.
--
-- A `shutting-down` server is deliberately NOT treated as stale: it is
-- still live by `server_is_live`'s reckoning, so `attach_buffer` would
-- early-return the stale record and burn this buffer's single attempt
-- on a no-op. Skipping leaves the attempt for a later tick, once the
-- retirement has actually landed.
local function repair_active_if_stale()
-- **`fallback_installed`, not `latched`.** When the swap does not
-- happen — the config already names the fallback, or it vanished
-- before an asynchronous verdict landed — `fire_latch` returns early
-- but `latched` stays true. Gating repair on `latched` then retried
-- the UNCHANGED configuration and reported the result as a fallback
-- failure, which is both a second pointless spawn and a misleading
-- message. Repair exists to apply a swap; no swap, nothing to apply.
if not probe.fallback_installed then return end
local buf = pmacs.window.buffer()
if not buf then return end
local key = tostring(buf)
if probe.repaired[key] then return end
local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf)
if not ok_lang or lang ~= "lean4" then return end
local rec = pmacs.lsp.active_attachment()
local stale
if not rec then
stale = true
else
local kind = server_state_kind(rec.server)
stale = (kind == nil or kind == "crashed" or kind == "stopped")
end
if not stale then return end
probe.repaired[key] = true
probe.repair_attempts = probe.repair_attempts + 1
local ok, fresh = pcall(pmacs.lsp._attach_buffer)
if not ok or not fresh then
report("LSP: lean4 fallback " .. fallback_name()
.. " did not start either")
return
end
-- **A successful SPAWN is not a successful START.** The once-per-
-- buffer bound stops `_attach_buffer` being called again, but it says
-- nothing about the server it produced. Arm this id immediately; the
-- poll below also discovers servers created through lsp.lua's own
-- after-load and command paths.
watch_fallback_server(fresh.server)
end
-- Every fallback server gets its own die-before-initialize poll. A scalar
-- watch cannot cover Q#LN15's simultaneous per-root servers, and a server
-- may be created by lsp.lua's after-load or command path without passing
-- through `repair_active_if_stale`. Discovery from the private ownership
-- table closes both holes.
local function poll_fallbacks()
if not probe.fallback_installed then return end
local ok, rows = pcall(pmacs.lsp.list)
if not ok or not rows then return end
local by_key = {}
for _, info in ipairs(rows) do
local key = tostring(info.id)
by_key[key] = info
if not probe.fallback_done[key] and is_derived_server(info.id) then
probe.fallback_watches[key] = info.id
end
end
for key, sid in pairs(probe.fallback_watches) do
local info = by_key[key]
local kind = info and info.state and info.state.kind
if kind == "initialized" then
probe.fallback_watches[key] = nil
probe.fallback_done[key] = true
elseif info == nil or kind == "crashed" or kind == "stopped" then
probe.fallback_watches[key] = nil
probe.fallback_done[key] = true
if info ~= nil then retire_server(sid) end
report("LSP: lean4 fallback " .. fallback_name()
.. " started but did not stay up")
end
end
end
local function fire_latch(sid, why)
if probe.latched then return end
probe.latched = true
probe.watching = nil
if not swap_to_fallback() then
report("LSP: lean4 " .. why)
-- No shared config changed, so only the server whose failure
-- triggered this verdict is invalid. Sweeping every root here stops
-- healthy instances of a root-sensitive command for no reason.
if sid and is_derived_server(sid) then retire_server(sid) end
return
end
retire_derived_lean_servers()
probe.fallback_installed = true
report("LSP: lean4 " .. why .. "; falling back to " .. fallback_name())
-- Repair what is in front of the user now; everything else is
-- repaired lazily as it becomes active (see `repair_active_if_stale`).
repair_active_if_stale()
end
local function drain_probe()
if not probe.proc then return end
local ok, evs = pcall(pmacs.process.events_take, probe.proc)
if not ok or not evs then return end
for _, ev in ipairs(evs) do
if ev.kind == "stdout" or ev.kind == "stderr" then
probe.out = probe.out .. tostring(ev.bytes)
elseif ev.kind == "exited" or ev.kind == "signaled"
or ev.kind == "crashed" then
local proc = probe.proc
probe.proc = nil
pcall(pmacs.process.forget, proc)
-- A non-zero exit is NOT a fallback trigger on its own. §2.9: elan
-- shims make `lake --version` exit non-zero with "no default
-- toolchain configured" on a machine where `lake serve` may still
-- be the right command — the server-failure latch covers that
-- case, and covers it better. The probe answers only the ONE
-- question failure detection would otherwise answer slowly: an
-- old-but-working lake that starts a useless server.
-- **`probe.primary`, NOT `probe.watching`.** `watching` is
-- failure-polling state and is cleared the moment the server
-- initializes. A slow `--version` that lands after a successful
-- initialize would then arrive with nil, and `fire_latch(nil)`
-- retires nothing: `_attach_buffer` finds the still-live primary
-- attachment, early-returns it, and the retry calls that success.
-- Status and config would say "fell back" while the buffer stayed
-- on the old server — the same silent no-op as round 1, reached
-- through a different event ordering. Initializing must stop the
-- failure poll, not erase the server the verdict has to retire.
if ev.kind == "exited" and ev.code == 0
and version_below_3_1(probe.out) then
fire_latch(probe.primary, "lake is older than 3.1.0")
end
end
end
end
-- The probe cannot gate the first attach. There is no blocking process
-- run (§2.9): `spawn` + `events_take` off a tick is the only shape
-- available, so the verdict arrives AFTER `ensure_server` has already
-- had to decide. Hence the optimistic `lake serve` spawn, with the
-- probe and the latch correcting it.
local function start_probe(root)
if probe.started then return end
probe.started = true
local cfg = pmacs.lsp.config.lean4
if not cfg or not cfg.command then return end
-- **Only probe something actually named `lake`.** `version_below_3_1`
-- parses the first `x.y` it finds anywhere in the output, which is a
-- rule about LAKE's output contract and nothing else. Run against a
-- user's wrapper it is a category error: a working `my-lean-wrapper`
-- reporting "wrapper 1.0" would be replaced despite its server having
-- initialized fine. The FAILURE latch stays command-agnostic — that
-- one keys on the server actually not starting, which is true of any
-- command — but the version rule only applies where its contract
-- holds.
local base = cfg.command:match("([^/]+)$") or cfg.command
if base ~= "lake" then return end
-- Probe the binary we would actually run, not the literal string
-- "lake": a user pointing `command` at an absolute path to lake should
-- have THAT probed, not whatever `lake` resolves to on PATH.
local spec = {
-- COHERENCE §9: `ProcessSpec.label` is the only identity a process
-- carries, and it is what `pmacs.process.list` renders. A user
-- wondering why their editor touched `lake` finds an owner here.
label = "lean:lake-version-probe",
command = cfg.command,
args = { "--version" },
stdin = "null",
}
if root then spec.cwd = root end
local ok, proc = pcall(pmacs.process.spawn, spec)
if ok then probe.proc = proc end
-- A probe that cannot even spawn says nothing the latch will not say
-- more reliably a moment later, so it is not reported here.
end
-- How the latch observes server failure.
--
-- There is no event for "died before initialize" — the drain ignores
-- state events. So this polls `pmacs.lsp.list()` on the
-- `process.after-tick` cadence and treats a terminal state reached
-- WITHOUT an intervening `initialized` as the trigger. Watching stops
-- as soon as the server initializes, so an ordinary later crash (a real
-- server dying on a real error) does not silently rewrite the command.
local function poll_latch()
local sid = probe.watching
if not sid or probe.latched then return end
local skey = tostring(sid)
local ok, rows = pcall(pmacs.lsp.list)
if not ok or not rows then return end
for _, info in ipairs(rows) do
if tostring(info.id) == skey then
local kind = info.state and info.state.kind
if kind == "initialized" then
-- Stop polling for failure; `probe.primary` deliberately
-- survives, because a later version verdict still needs it.
probe.saw_initialized = true
probe.watching = nil
return
end
if kind == "crashed" or kind == "stopped" then
fire_latch(sid, configured_command() .. " failed to start")
end
return
end
end
-- Gone from the manager entirely without ever initializing.
fire_latch(nil, configured_command() .. " failed to start")
end
-- Q#LN16 — `textDocument/waitForDiagnostics` --------------------------
--
-- A plain request: no position, so Q#LN12's `outbound_position` concern
-- does not apply. Resolves when the server has finished elaborating.
-- Awaited through Stage 3a's response seam.
--
-- **`version` is required, not optional.** Lean's
-- `WaitForDiagnosticsParams` is `{ uri, version }` (v4.9.0,
-- `src/Lean/Data/Lsp/Extra.lean`), and the request is how the client
-- says *which* revision of the document it wants elaboration for.
-- Sending only `uri` is a malformed request against a real server; it
-- happened to look fine here because the fake server echoes any
-- payload. Callers pass the attachment's current `version`.
--
-- `fn(err)` is called with nil on success. Registering the one-shot
-- requires the server to have an attached buffer — see the note on
-- `pmacs.lsp.on_response`; every caller here comes from an attachment.
function M.wait_for_diagnostics(sid, uri, version, fn)
local ok, rid = pcall(pmacs.lsp.send_request, sid,
"textDocument/waitForDiagnostics", { uri = uri, version = version })
if not ok then
if fn then pcall(fn, tostring(rid)) end
return nil
end
if fn then
pmacs.lsp.on_response(sid, rid, function(_, err)
fn(err and err.message or nil)
end)
end
return rid
end
local function when_server_ready(sid, fn)
local function state_kind()
local ok, state = pcall(pmacs.lsp.status, sid)
if not ok or not state then return nil end
return state.kind
end
local kind = state_kind()
if kind == "initialized" then
fn(nil)
return
end
if kind == nil or kind == "crashed" or kind == "stopped" then
fn("server did not initialize")
return
end
-- A command may have just healed a dead attachment, in which case the
-- replacement is still starting. Requests are not queued before
-- initialize, so issue this one after the lifecycle reaches ready
-- rather than replacing the attachment and immediately failing on it.
pmacs.async(function()
for _ = 1, 300 do
pmacs.async.yield_to_next_tick()
kind = state_kind()
if kind == "initialized" then
fn(nil)
return
end
if kind == nil or kind == "crashed" or kind == "stopped" then
fn("server did not initialize")
return
end
end
fn("server initialization timed out")
end)
end
pmacs.command.define {
name = "lean.wait-for-diagnostics",
description = "Wait for the Lean server to finish elaborating this file",
fn = function()
local rec = pmacs.lsp._attachment_for_command()
if not rec or rec.language ~= "lean4" then
pmacs.editor.set_status("lean: no Lean server for this buffer")
return
end
pmacs.editor.set_status("lean: elaborating…")
when_server_ready(rec.server, function(init_err)
if init_err then
pmacs.editor.set_status("lean: " .. tostring(init_err))
return
end
M.wait_for_diagnostics(rec.server, rec.uri, rec.version, function(err)
if err then
pmacs.editor.set_status("lean: " .. tostring(err))
else
pmacs.editor.set_status("lean: elaboration complete")
end
end)
end)
end,
}
-- `$/lean/fileProgress` — the elaboration-in-flight signal. Stage 5's
-- goal view reads it to distinguish "no goals" from "not done yet";
-- here it is recorded so that consumer has something to read and so the
-- notification seam has its first production subscriber.
M.file_progress = {}
pmacs.lsp.on_notification("$/lean/fileProgress", function(_, params)
local uri = params and params.textDocument and params.textDocument.uri
if type(uri) ~= "string" then return end
M.file_progress[uri] = params.processing or {}
end)
-- Wiring --------------------------------------------------------------
-- Runs after `lsp.lua`'s own `buffer.after-load` subscription.
--
-- **Keyed on the buffer's LANGUAGE, not on an attachment existing.**
-- Round 1 keyed on `active_attachment()` and returned early when it was
-- nil — which silently excluded the single most likely real-world
-- failure: `lake` not installed. `ensure_server` pcalls the spawn and
-- returns nil on ENOENT, so `attach_buffer` produces no record at all,
-- so the probe never started and the latch never armed. The case the
-- fallback exists for was the one case it could not see.
pmacs.hook.add("buffer.after-load", function()
local buf = pmacs.window.buffer()
if not buf then return end
local ok_lang, lang = pcall(pmacs.lsp.buffer_language, buf)
if not ok_lang or lang ~= "lean4" then return end
local rec = pmacs.lsp.active_attachment()
if rec and rec.language == "lean4" then
-- A matching-root server supplied by the user may be adopted by
-- `ensure_server`. Its lifecycle is not evidence about the
-- config-driven command, and neither the version probe nor fallback
-- latch may mutate config because that foreign server changed state.
if not is_derived_server(rec.server) then return end
if not probe.started then
local path = pmacs.editor.file_path()
start_probe(path and M.root_for(path) or nil)
end
-- **Arm ONCE, capturing buffer and server together.** Setting
-- `buf_key` on every Lean load meant a second Lean buffer opened
-- before the verdict silently became the rebuild target while the
-- latch still watched the FIRST buffer's server — so the rebuild
-- either repaired the wrong buffer or accepted the second buffer's
-- unrelated live server as success, stranding the first. The pair
-- (target buffer, primary server) is one fact and is captured as
-- one.
if not probe.armed and not probe.latched and not probe.saw_initialized then
probe.armed = true
probe.buf_key = tostring(buf)
probe.primary = rec.server
probe.watching = rec.server
end
return
end
-- **Unconfigured is DISABLED, not failed.** A user who sets
-- `pmacs.lsp.config.lean4 = nil`, or clears its `command`, has turned
-- the Lean server off; reporting that "nil could not be started" is a
-- false alarm, and latching would poison the session so a later
-- configuration could never take effect. Only a CONFIGURED command
-- that produced no attachment is a failure.
local cfg = pmacs.lsp.config.lean4
if not cfg or not cfg.command then return end
if not probe.started then
local path = pmacs.editor.file_path()
start_probe(path and M.root_for(path) or nil)
end
-- No attachment for a Lean buffer with a configured command means
-- `ensure_server` could not spawn at all — a synchronous ENOENT,
-- already swallowed upstream. That is not something to wait for; it
-- is the failure itself, and the only place it is still observable.
if not probe.latched then
-- No server was ever created, so there is no primary to retire —
-- but the rebuild still needs a target buffer.
if not probe.armed then
probe.armed = true
probe.buf_key = tostring(buf)
end
fire_latch(nil, configured_command() .. " could not be started")
end
end)
-- A buffer switch is the moment a stale Lean buffer becomes visible, so
-- repair immediately rather than waiting for the next tick. lsp.lua's
-- own `after-switch` subscription re-pushes views but does NOT rebuild a
-- stale attachment, so nothing else covers this.
pmacs.hook.add("buffer.after-switch", function()
repair_active_if_stale()
end)
pmacs.hook.add("process.after-tick", function()
drain_probe()
poll_latch()
-- Repair the active buffer if the latch invalidated it. Cheap when
-- there is nothing to do, and bounded to one attempt per buffer.
repair_active_if_stale()
poll_fallbacks()
end)
-- Test seam: acceptance drives the latch deterministically rather than
-- waiting on real process timing. Not part of the public surface.
M._probe = probe
M._fire_latch = fire_latch
M._version_below_3_1 = version_below_3_1
pmacs.lean = M

292
builtin/runtime/lsp.lua
View File

@ -607,6 +607,12 @@ local function project_root_for(language, path)
return dir_of(path), "fallback"
end
-- Servers created by the automatic config-driven path. This is the
-- ownership fact a caller-supplied `label` cannot provide: labels are
-- public, unreserved display strings, while entries here are written
-- only after this module itself successfully spawns a server.
local default_servers = {}
local function ensure_server(language, path)
local cfg = pmacs.lsp.config[language]
if not cfg or not cfg.command then return nil end
@ -660,7 +666,30 @@ local function ensure_server(language, path)
cwd = root,
root_uri = key_uri,
})
if ok then return sid end
if ok then
default_servers[tostring(sid)] = language
return sid
end
return nil
end
-- Internal ownership seam for builtins whose lifecycle follows the
-- config-driven server set (currently Lean's one-shot fallback). A
-- user-managed server may deliberately use the same language id, label,
-- command, and root; none of those make it ours.
function pmacs.lsp._is_default_server(sid, language)
local owned_language = default_servers[tostring(sid)]
return owned_language ~= nil
and (language == nil or owned_language == language)
end
local function server_state_kind(sid)
if not sid then return nil end
for _, info in ipairs(pmacs.lsp.list()) do
if tostring(info.id) == tostring(sid) then
return info.state and info.state.kind
end
end
return nil
end
@ -669,14 +698,8 @@ end
-- forgotten, or was spawned against a now-replaced `pmacs.lsp.config`
-- entry — get rebuilt on the next attach attempt.
local function server_is_live(sid)
if not sid then return false end
for _, info in ipairs(pmacs.lsp.list()) do
if tostring(info.id) == tostring(sid) then
local kind = info.state and info.state.kind
return kind ~= "crashed" and kind ~= "stopped"
end
end
return false
local kind = server_state_kind(sid)
return kind ~= nil and kind ~= "crashed" and kind ~= "stopped"
end
local function server_is_initialized(sid)
@ -811,6 +834,15 @@ local function attach_buffer(buf)
local existing = attachments[key]
if existing and server_is_live(existing.server) then return existing end
if existing then
local kind = server_state_kind(existing.server)
if kind == "crashed" or kind == "stopped" then
-- A terminal OnCrash client may still have `next_restart_at`
-- armed. Spawning beside it creates two same-root servers when
-- the old id restarts. `forget` is the terminal-state operation:
-- it removes the client and cancels that pending restart before
-- the replacement is created.
pcall(pmacs.lsp.forget, existing.server)
end
attachments[key] = nil
-- Unsent edits targeted the dead attachment; the did_open below
-- carries the full current text, superseding them.
@ -871,6 +903,21 @@ local function attached_for_active()
if not buf then return nil end
local key = tostring(buf)
local rec = attachments[key]
-- A record whose server is dead is worse than no record: every
-- command below issues requests against it and gets silence. Rebuild
-- instead, which is what `attach_buffer` does for a stale attachment
-- anyway — this just stops the dead record short-circuiting that.
--
-- Load-bearing for anything that retires a server out from under open
-- buffers (Arc 8 Stage 3b's fallback latch retires every Lean server
-- at once). Buffers in OTHER frontends get no `buffer.after-switch`
-- in this one, so an eager repair sweep keyed on the ambient active
-- buffer cannot reach them; healing at the point of USE is
-- frontend-agnostic, because whichever frontend runs the command is
-- the active one while it runs.
if rec and not server_is_live(rec.server) then
rec = nil
end
if rec then
-- Every interactive command resolves its attachment here before
-- issuing requests; flushing now means the server answers those
@ -881,6 +928,14 @@ local function attached_for_active()
return attach_buffer(buf)
end
-- Internal command-path resolver for builtin request producers outside
-- this module. Unlike `active_attachment` it may replace a dead record;
-- unlike `attachment_for_request` it is called only from an explicit
-- user command, where attach-on-use is the intended policy.
function pmacs.lsp._attachment_for_command()
return attached_for_active()
end
-- Pure, side-effect-free attachment lookup for the active buffer:
-- returns the live record (with `.uri`) when a server is already
-- attached, else nil. Unlike `attached_for_active`, it never *triggers*
@ -893,6 +948,24 @@ function pmacs.lsp.active_attachment()
return attachments[tostring(buf)]
end
-- Re-run the attach for the ACTIVE buffer, rebuilding it against the
-- current `pmacs.lsp.config`.
--
-- Exists for the Arc 8 Stage 3b fallback latch (Q#LN7): after that latch
-- stops a server that failed to start and rewrites `config.lean4`,
-- something has to actually spawn the replacement and re-point the
-- buffer at it. Nothing else does — `attach_buffer` early-returns for a
-- live attachment, and no hook re-fires on a config change, so without
-- this the buffer stays bound to the stopped server and the "fallback"
-- is a config edit with no effect.
--
-- Deliberately keyed on the active buffer, matching `attach_buffer`'s
-- own use of `active_buffer_path()`; it is not a general re-attach for
-- arbitrary buffers and must not be used as one.
function pmacs.lsp._attach_buffer()
return attach_buffer(pmacs.window.buffer())
end
-- Arc 4 stage 3: pure modeline projection. This reads the private
-- per-buffer attachment map directly so passive split windows report their
-- own buffer instead of the focused window. It never attaches, flushes
@ -924,6 +997,19 @@ function pmacs.lsp.attachment_for_request()
local key = tostring(buf)
local rec = attachments[key]
if not rec then return nil end
-- Same liveness rule as `attached_for_active`: a record naming a dead
-- server is worse than none, because the caller issues a request
-- against it and waits for a reply that cannot come. Unlike that
-- function this one is deliberately non-attaching (it must not
-- perturb LSP state), so a dead record reads as "no attachment"
-- rather than triggering a rebuild.
if not server_is_live(rec.server) then
-- Preserve the record. A crashed OnCrash server may restart under
-- the SAME id; clearing the map here would orphan that recovered
-- server, while this non-attaching lookup has no authority to
-- cancel the restart or create a replacement.
return nil
end
flush_did_change(key)
return rec
end
@ -1546,6 +1632,186 @@ end
-- itself is unaffected. Server ids are snapshotted before the loop
-- because `apply_workspace_edit` → `find_or_open` can attach a new
-- buffer mid-iteration (mutating `attachments`).
-- Server-originated notification / response seams (framing Q#LN9) -------
--
-- Before this, `handle_server_requests` handled five `request` methods
-- and `initialized`, and dropped every `notification` and `response` on
-- the floor. Dropping responses made `pmacs.lsp.send_request` a
-- write-only API from Lua: the reply was drained and discarded, so
-- nothing outside Rust's typed stores could ever consume one.
--
-- Both seams route through the *existing* drain. A second
-- `events_take` caller would steal events from this one — `take_events`
-- removes the queue — so any new consumer must extend this loop rather
-- than open its own.
--
-- method -> array of subscriber fns. Persistent; `pmacs.hook` has no
-- `remove` and neither does this, deliberately matching it.
local notification_subs = {}
-- tostring(sid) -> { [request_id] = { fn = fn, attempt = n } }. One-shot.
local pending_responses = {}
local function report_subscriber_error(what, err)
local msg = string.format("LSP: %s subscriber failed: %s", what,
tostring(err))
-- COHERENCE §1.2: a pcall around background wiring must report, not
-- discard. `pmacs.editor.set_status` is the channel that exists;
-- `pmacs.error` is referenced by fifteen call sites and defined
-- nowhere in production, so it rides along rather than standing alone.
pcall(pmacs.editor.set_status, msg)
if pmacs.error then pcall(pmacs.error, msg) end
end
-- Current spawn attempt for `sid`, or nil if the manager has forgotten
-- it. A restart reuses the sid but bumps the attempt, which is how a
-- pending one-shot tells "my server is still here" from "my server died
-- and a new generation took its id".
local function server_attempt(sid)
local skey = tostring(sid)
for _, info in ipairs(pmacs.lsp.list()) do
if tostring(info.id) == skey then
return info.attempt or 0
end
end
return nil
end
-- fn(sid, params); persistent, fires for every server.
function pmacs.lsp.on_notification(method, fn)
if type(method) ~= "string" or type(fn) ~= "function" then
error("pmacs.lsp.on_notification(method, fn): want string, function")
end
local subs = notification_subs[method]
if not subs then
subs = {}
notification_subs[method] = subs
end
subs[#subs + 1] = fn
end
-- fn(result, err); ONE-SHOT, keyed to the exact request.
-- `request_id` is what `pmacs.lsp.send_request` returned.
--
-- **Register only against a server with an attached buffer.** The drain
-- that delivers replies visits only sids present in `attachments`, so a
-- one-shot on an unattached server will not fire on its reply — the
-- reply sits in that server's queue and the handler is invoked only when
-- the purge below decides the server is gone. That is fire-on-death, not
-- fire-on-reply, and it looks exactly like a hung request while
-- debugging. The attach path is the ordinary way to get a sid; a
-- hand-spawned one from `init.lua` is the case to watch.
function pmacs.lsp.on_response(sid, request_id, fn)
if not sid or type(request_id) ~= "number" or type(fn) ~= "function" then
error("pmacs.lsp.on_response(sid, request_id, fn): want sid, number, function")
end
local skey = tostring(sid)
local pend = pending_responses[skey]
if not pend then
pend = {}
pending_responses[skey] = pend
end
-- The attempt is captured at registration so a restart under the same
-- sid purges this entry rather than leaving it waiting on a reply the
-- dead generation was going to send.
pend[request_id] = { fn = fn, attempt = server_attempt(sid) or 0 }
end
local function dispatch_notification(sid, ev)
local subs = notification_subs[ev.method]
if not subs then return end
-- Length captured up front: a subscriber that registers another one
-- must not be able to extend the list being walked.
local n = #subs
for i = 1, n do
local ok, err = pcall(subs[i], sid, ev.params)
if not ok then
report_subscriber_error("notification " .. tostring(ev.method), err)
end
end
end
local function deliver_response(sid, ev)
local skey = tostring(sid)
local pend = pending_responses[skey]
if not pend then return end
local entry = pend[ev.request_id]
if not entry then return end
-- Removed UNCONDITIONALLY, so a handler that raises is still retired
-- and cannot be invoked a second time by the purge. Removing first is
-- the defensive order and costs nothing, but it is not what defends
-- against re-invocation: `pcall` catches the raise either way, so
-- before-vs-after is unobservable without a re-entrant drain. The
-- reachable bug is gating removal on a clean return, which acceptance
-- 32 bites (2 != 1).
pend[ev.request_id] = nil
if next(pend) == nil then pending_responses[skey] = nil end
local ok, err = pcall(entry.fn, ev.result, ev.error)
if not ok then
report_subscriber_error("response " .. tostring(ev.method), err)
end
end
-- Settle every one-shot whose server can no longer answer it.
--
-- Deliberately driven off `pmacs.lsp.list()` and NOT off a death event
-- observed in the drain, because the drain cannot be relied on to reach
-- the server in question: `handle_server_requests` builds its sid list
-- from `attachments`, and a sid leaves that table whenever
-- `attach_buffer` finds it dead and rebuilds the attachment against a
-- fresh server. So the very event that should trigger the purge —
-- `crashed` / `stopped` — is the one most likely to go undrained. A
-- one-shot settled only by the drain would leak exactly when it matters.
--
-- `pmacs.lsp.list()` enumerates the manager directly and is unaffected
-- by attachment bookkeeping, which is what makes it the right authority.
local function purge_dead_pending()
if next(pending_responses) == nil then return end
local ok, rows = pcall(pmacs.lsp.list)
-- A failed enumeration is not evidence that every server died; leaving
-- the registrations alone is the safe read of "we don't know".
if not ok or not rows then return end
local alive = {}
for _, info in ipairs(rows) do
local kind = info.state and info.state.kind
if kind ~= "crashed" and kind ~= "stopped" then
alive[tostring(info.id)] = info.attempt or 0
end
end
for skey, pend in pairs(pending_responses) do
local attempt = alive[skey]
local dead = {}
for rid, entry in pairs(pend) do
-- Absent or terminal, or the same sid running a NEW generation:
-- in every case the request this entry awaits is unanswerable.
--
-- The generation half is **defensive and not covered by the
-- acceptance suite**, stated plainly rather than left to look
-- tested. Reaching it requires a crash and its restart to both
-- fall inside a gap with no `_async.tick` — the crash backoff is
-- 500ms (`src/lsp.rs:1007`), so any tick during that window sees
-- `crashed` and the absent-or-terminal test above fires first. A
-- stalled or idle editor can produce such a gap, and then this is
-- the only thing standing between a one-shot and waiting forever
-- on a reply the dead generation owed. Every attempt to stage it
-- deterministically ended up exercising the `crashed` path
-- instead, so it is kept as insurance and labelled as such.
if attempt == nil or attempt ~= entry.attempt then
dead[#dead + 1] = rid
end
end
for _, rid in ipairs(dead) do
local entry = pend[rid]
pend[rid] = nil
local ok_h, err = pcall(entry.fn, nil,
{ message = "server gone before response" })
if not ok_h then
report_subscriber_error("response purge", err)
end
end
if next(pend) == nil then pending_responses[skey] = nil end
end
end
local function handle_server_requests()
local sids, seen = {}, {}
for _, rec in pairs(attachments) do
@ -1598,6 +1864,10 @@ local function handle_server_requests()
-- LSP spells the field "unregisterations".
pcall(unregister_file_watchers, sid,
ev.params and ev.params.unregisterations)
elseif ev.kind == "notification" then
dispatch_notification(sid, ev)
elseif ev.kind == "response" then
deliver_response(sid, ev)
elseif ev.kind == "initialized" then
-- Buffers attach before the server finishes initializing, so
-- the pulls in `attach_buffer` are no-ops for the FIRST file
@ -1620,6 +1890,10 @@ if pmacs._async and pmacs._async.tick then
pmacs._async.tick = function(...)
local ret = _prior_async_tick(...)
pcall(handle_server_requests)
-- After the drain, so a response delivered this tick settles its
-- one-shot normally rather than being purged as "server gone" in the
-- same pass when the server died right after answering.
pcall(purge_dead_pending)
pcall(flush_due_did_changes)
return ret
end

85
builtin/runtime/pair.lua
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,
}

167
builtin/runtime/terminal.lua
View File

@ -3,6 +3,38 @@
local terminal = assert(pmacs.terminal, "pmacs.terminal raw bindings are required")
local raw_open = assert(terminal._open, "pmacs.terminal._open is required")
-- Q#TC2a. Every default reproduces today's behavior exactly, so a tree
-- with no settings written and no profiles registered behaves as before.
pmacs.config.define {
name = "terminal.default-profile",
type = "string",
default = "",
allow_empty = true,
mutability = "live",
description = "Profile name from pmacs.terminal.profiles to open by default. " ..
"Empty means no profile: fall back to $SHELL.",
}
pmacs.config.define {
name = "terminal.scrollback-rows",
type = "integer",
default = 10000,
min = 0,
max = 4000000,
mutability = "live",
description = "Rows of scrollback retained per terminal. " ..
"0 retains no history.",
}
pmacs.config.define {
name = "terminal.escape-key",
type = "string",
default = "C-c",
mutability = "live",
description = "Chord that escapes to the editor from a terminal. " ..
"Pressing it twice sends the chord itself to the child.",
}
local function bind_terminal_keys(buffer)
local function bind(sequence, command)
pmacs.keymap.bind {
@ -19,22 +51,145 @@ local function bind_terminal_keys(buffer)
bind("M->", "terminal.scroll-bottom")
end
-- Q#TC1: profiles are a raw Lua table, not a config setting. The
-- registry stores four scalars and has no table kind, so a profile —
-- inherently `{ command, args, cwd, env }` — lives here beside
-- `pmacs.lsp.config` and `pmacs.pair.sets` until table-valued settings
-- exist.
terminal.profiles = terminal.profiles or {}
local PROFILE_FIELDS = {
command = "string",
args = "table",
cwd = "string",
env = "table",
}
-- Every diagnostic below renders a caller- or user-supplied value, so
-- rendering must never be the thing that fails. `%q` is partial — it
-- raises on a table or function — and a profile name arrives straight
-- from `open { profile = ... }`.
local function describe_name(name)
if type(name) == "string" then return string.format("%q", name) end
return string.format("<%s %s>", type(name), tostring(name))
end
local function validate_profile(name, profile)
local shown = describe_name(name)
if type(profile) ~= "table" then
error(string.format("terminal profile %s must be a table", shown), 0)
end
for key, value in pairs(profile) do
local expected = PROFILE_FIELDS[key]
if not expected then
error(string.format("terminal profile %s: unknown field %q", shown, tostring(key)), 0)
end
if type(value) ~= expected then
error(string.format(
"terminal profile %s: field %q must be a %s, got %s",
shown, key, expected, type(value)), 0)
end
end
return profile
end
-- `terminal.profiles` is a raw user table, so its keys are whatever the
-- user wrote. Sorting them directly raises "attempt to compare number
-- with string" the moment the table holds both a string and a numeric
-- key — and it raises on the UNKNOWN-PROFILE path, replacing the very
-- error this list exists to explain with an opaque one. Sorting DISPLAY
-- strings is total over every key type, so the diagnostic survives a
-- malformed table.
local function known_profile_names()
local names = {}
for name in pairs(terminal.profiles) do names[#names + 1] = tostring(name) end
table.sort(names)
return names
end
-- Q#TC2 / Q#TC3a: resolve a profile by name, or nil when none is
-- selected. An explicitly requested profile that does not exist is an
-- error even when `terminal.default-profile` is valid — a typo must not
-- silently fall back to the default.
local function resolve_profile(requested)
local name = requested
if name == nil then
local configured = pmacs.config.get("terminal.default-profile")
if configured == nil or configured == "" then return nil end
name = configured
end
local profile = terminal.profiles[name]
if profile == nil then
local known = known_profile_names()
local listed = #known > 0 and table.concat(known, ", ") or "(none defined)"
error(string.format(
"terminal profile %s is not defined; known profiles: %s",
describe_name(name), listed), 0)
end
return validate_profile(name, profile)
end
-- Q#TC3a merge order, per field: explicit open field, then the profile's
-- field, then the scalar setting, then the built-in fallback. `env` is
-- the one field where "first wins" would be wrong, so it MERGES with
-- explicit entries overriding the profile's — any other reading silently
-- drops half a user's environment.
local function merge_env(profile_env, explicit_env)
if profile_env == nil then return explicit_env end
local merged = {}
for key, value in pairs(profile_env) do merged[key] = value end
for key, value in pairs(explicit_env or {}) do merged[key] = value end
return merged
end
function terminal.open(spec)
local buffer = raw_open(spec)
spec = spec or {}
local resolved = {}
for key, value in pairs(spec) do
if key ~= "profile" then resolved[key] = value end
end
local profile = resolve_profile(spec.profile)
if profile then
for key in pairs(PROFILE_FIELDS) do
if key ~= "env" and resolved[key] == nil then resolved[key] = profile[key] end
end
resolved.env = merge_env(profile.env, spec.env)
end
-- The two open-time settings resolve through the GLOBAL chain
-- (Q#TC2b): they are read before the identity buffer exists, so there
-- is no terminal to resolve a buffer-local against.
if resolved.scrollback_rows == nil then
resolved.scrollback_rows = pmacs.config.get("terminal.scrollback-rows")
end
if resolved.command == nil then
resolved.command = os.getenv("SHELL") or "/bin/sh"
end
local buffer = raw_open(resolved)
bind_terminal_keys(buffer)
return buffer
end
pmacs.command.define {
name = "terminal",
description = "Open a terminal running $SHELL (or /bin/sh).",
fn = function()
return terminal.open {
command = os.getenv("SHELL") or "/bin/sh",
}
description = "Open a terminal running the configured profile, or $SHELL.",
fn = function(profile)
return terminal.open { profile = profile }
end,
}
-- Q#TC10: the opening binding. `COHERENCE.md` Priority 1 names a
-- terminal keybinding as part of protecting the golden journey, and §2
-- step 8 grades the terminal "works but undiscoverable". `C-c` is
-- already a live global prefix (fold's `C-c @ ...`), so this is a new
-- leaf under it rather than a shadow.
--
-- Named limitation: unreachable from INSIDE a terminal window, where
-- `C-c` is consumed as the escape. `M-x terminal` still works there.
pmacs.keymap.bind { scope = "global", sequence = "C-c t", command = "terminal" }
pmacs.command.define {
name = "terminal.copy-selection",
description = "Copy the active terminal selection.",

183
builtin/runtime/typed_edit.lua Normal file
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)

472
docs/active-work.md
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.
@ -23,12 +23,13 @@ here too until #172 removed it — that is the update those two owe.)
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` @ `c93f9ee` (the bottom-panel Stage 2 framing #175
atop 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).
`githubsucks/main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a
#167, the bottom-panel landed-doc refresh #156, the inline-math slice
#158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4
Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file
#162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159;
protocol v20). The previous snapshot named `d152120`; the recovery
check below accepts it or anything newer.
**Lanes below that name an older base have not been re-based; derive
their integration surface from `git diff <their base>..main`.**
- On the transfer source, `origin/main` named a release mirror at
@ -71,139 +72,172 @@ declares canonical will pass on a tree the rest of this file does not
describe.
If it does not, stop and repair the remote/fetch configuration.
## Lean 4 lane (Arc 8) — Stage 1 MERGED; Stage 2 IN REVIEW (PR #161)
## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4a IN REVIEW
- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
round, all twelve checks green). Branch `githubsucks/lean4-stage1`
retained; it was worked in the shared checkout (no sibling worktree).
- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as
the branch's first commit (`a382965`) after three review rounds. **Seven
stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star:
match or exceed VS Code's Lean support.
- **Stage 1 implemented; no wire change (protocol stays v20), no LSP, no
frontend change.** Four commits: framing, grammar, theme captures,
editing surface + acceptance.
- `Cargo.toml` + `src/syntax.rs`: `arborium-lean` 2.18 and one
`BUILTIN_LANGUAGES` entry named **`lean4`** (Q#LN2 — the name becomes
the `didOpen` language_id), claiming `.lean` only.
- `src/highlight.rs`: four capture entries — `constructor`, `character`,
`keyword.conditional`, `warning`.
- `builtin/runtime/{comment,pair,syntax}.lua`: `--` comments, the
`⟨⟩ ⦃⦄ ⟮⟯` pair set, the `lean` → `lean4` modeline alias.
- `tests/lean4_stage1_acceptance.rs` plus unit tests in `syntax.rs` /
`highlight.rs`: 12 criteria, 17 tests.
- **Q#LN1's open obligation is discharged.** `tree-sitter-lean4` is
unusable (depends on `tree-sitter ^0.25` directly against our 0.26,
exports no `LANGUAGE` const despite its README, packages no queries);
`arborium-lean` rides `tree-sitter-language 0.1` with a pre-generated
ABI-15 parser. `cargo tree -d` shows no duplicate core. The parse smoke
pins the failure mode that matters: `→`/`∀`/`≥` must produce
`(arrow)`/`(forall)`/`(comparison)`, since a mismatched-core build
degrades silently on exactly those characters rather than failing loudly.
- **Q#LN4 is a deliberate retro-paint of seven language entries**, not
four: `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated
base-first into javascriptreact/typescript/typescriptreact. Its shape is
"every capitalized identifier" (`#match? "^[A-Z]"`) plus every Lua table
brace — not "constructors". Pinned in both directions per #146.
- Implementation findings not in the framing:
- `warning` had to move from bold red to bold **bright** red: `number`
is plain `fg(1)`, so `sorry` and an adjacent numeric literal were the
same colour. Found by writing the test.
- `Some(1)` is **not** `@constructor` — in call position a narrower
`@function` pattern wins. Only bare or pattern-position capitalized
identifiers reach it. Pinned so the blast-radius claim stays honest.
- Lean node kinds nest: `module > declaration > def|theorem`.
- `pmacs.parse.injection_aliases` is a documented **write-only** Lua
proxy (canonical map is Rust-side), so fence tests must drive
`_parse_now` and inspect layer languages, never read the table back.
- **Review round 1 addressed.** The finding: acc12's server-list assertion
could not fail for the regression it named — the shared `editor()`
helper wipes `pmacs.lsp.config` before any buffer opens, so
`#pmacs.lsp.list() == 0` holds for every language regardless of what
Stage 1 ships. It now asserts against a **pristine** `EditorState` that
`pmacs.lsp.config.lean4` is nil, with a non-vacuity check that the same
lookup finds `rust`; bite-verified by adding a `lean4` config to
`lsp.lua` and watching it fail. Also fixed a stale column in a
`highlight.rs` comment.
- Verification on this branch: `cargo fmt --check` clean; strict workspace
Clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1
9/9; comment toggle 14; auto-pair 45; injection 4; M4 121; required GPU
152; **isolated-config workspace sweep 3,150 across 90 suites**;
`git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME`
for the reason recorded in the bottom-panel lane below.
### Stage 2 — multi-root LSP server affinity (Q#LN15)
- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`),
#161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full
histories were pruned from this ledger in round 6, per this file's own
instruction to remove entries when their PR merges; the durable facts
now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where
a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8
carries the decisions.
- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout,
based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not
for Lean: **the diff contains no Lean content**, because `ensure_server`
is the one server-affinity function every LSP language shares and a
cross-cutting change to it must not be reviewable only as a Lean
feature.
- Three files, no protocol change: `src/lua_bindings/mod.rs` (the
`lsp.list()` row builder gains `root_uri` + `cwd`),
`builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`;
`ensure_server` hoists it above the reuse loop and matches on it),
`tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21).
- **The rule that keeps this from regressing every other language: the
affinity key is the root only when a root was actually FOUND.**
`project_root_for` never returns nil for a file with a path — its last
resort is the file's own directory — so a naive `(language_id, root)`
key gives every directory of loose scratch files its own server, for
every language. `source` is `"config" | "detected" | "fallback"` and
only the first two become a key.
- **Wire-identical for the fallback case, and that is provable rather
than hoped.** Matching is on the spawned spec's `root_uri` (nil matching
nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries
the directory and `build_initialize` derives the identical `rootUri`
from `cwd` when the field is None, using a percent-encoder with the same
allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`)
is the **only** reader of `spec.root_uri` in the tree.
- Deliberate behavior change, asserted not discovered: a server
hand-spawned from `init.lua` with only `cwd` set also reads back nil, so
a root-bearing attach will not adopt it.
- `config[language].root` may now be a `function(path) -> string|nil`,
memoized per directory — needed because the hoist puts root resolution
on every attach rather than every spawn. The memo is keyed **weakly by
the resolver function itself**, so replacing `config[lang].root` cannot
serve a root the previous resolver computed. This is Q#LN8's
generalization landing early; the Lean resolver that uses it is Stage 3.
- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`,
8/9 against the pre-change `mod.rs`, and — the one that matters most —
installing the naive always-key-on-root variant fails acceptance 20 and
21 exactly as Q#LN15 part 2 predicts. The four that survive the first
bite (13, 15, 16, 19) are the regression pins; passing on both sides is
their job.
- Every fixture sets `pmacs.project.set_search_boundary` at its own
tempdir root. Without it the marker walk climbs to the filesystem root
and a stray `.git` above the temp directory turns the markerless cases
into detected ones — the assertions would still pass while testing
nothing.
- **Found but not fixed here (pre-existing, own lane):** `ensure_server`
never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a
`restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on
the auto-attach path. At least one existing test sets it believing it
takes effect. Out of scope for a PR whose acceptance 16 pins existing
attach behavior as unchanged.
- **Review round 1 addressed.** The blocker was process, not design: the
test file was committed *before* `cargo fmt` ran, so the fix sat
uncommitted in the working tree and the branch as pushed failed the
first gate. The reported "fmt clean" described the worktree, not the
branch — gate results are only meaningful when run against the pushed
tree. Also added the two pins review asked for (a **string** `config
.root` as an affinity key — acc17 only covered the function form; and
`root = false` reading as unset), each bite-verified against exactly
the mutation it targets and neither against the other. And documented
the canonicalization obligation: the `"detected"` arm is canonicalized
for free, a **configured** root is not, so on macOS a resolver
returning `/var/…` and a detected `/private/var/…` are different keys
for one directory. Stage 3's Lean resolver is the first real consumer,
so the obligation is written at the point of use.
- Verification on this branch: `cargo fmt --check` clean; strict
workspace Clippy clean; 1,826 default + 2,003 CRDT library tests;
multi-root 11/11; M4 121; statusline 7; completion popup 9; auto-pair
45; required GPU 155; **isolated-config workspace sweep 3,164 across 91
suites**; `git diff --check` clean. The sweep needs an isolated
`XDG_CONFIG_HOME` and `-- --skip basedpyright`.
### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170**
(`main` @ `d400f30`), 2026-07-26. Both were integrated against a main
that had advanced 50 commits mid-review; the only conflict either time
was this ledger's own lane headings, resolved by keeping both sides.
- Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`.
Framing-only so far: `docs/lean4-mode-framing.md` **revision 8**. No
code. Awaiting user approval before implementation, per the workflow.
- **Round 6 review found five P1s, four of them internal to rev 6** —
facts about pmacs the revision asserted without checking, while its
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)
- 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:
| 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) |
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.
## GPU terminal input lane — IN REVIEW
@ -257,10 +291,166 @@ If it does not, stop and repair the remote/fetch configuration.
**isolated-config workspace sweep 3,177 across 92 suites, zero failures**;
`git diff --check` clean. Gates were run against the committed tree.
## Bottom-panel lane (Arc 7) — Stage 1 MERGED; Stage 2 IN FRAMING
## Terminal config + copy mode arc — Stage 1 IN REVIEW
Stage 1 is on `main`. **Stage 2 is in framing**, no implementation in
flight.
- Approved framing: `docs/terminal-config-and-copy-mode-framing.md`
**revision 4** (four review rounds), committed as the first commit of
Stage 1's branch. Two stages, two branches, two PRs; **no protocol
change**.
- **Stage 1 = `githubsucks/terminal-config`**, worktree
`../pmacs-terminal-config`, based on `githubsucks/main` @ `d152120`
and merged up to `c93f9ee` during review round 1. Profiles,
scrollback, escape key, and the `C-c t` opening binding.
- **Stage 2 = `terminal-copy-mode`, not started.** Branch it off `main`
after Stage 1 merges: no dependency, but both edit
`builtin/runtime/terminal.lua`.
- Load-bearing decisions, each forced by scouted ground truth:
- profiles are a **raw Lua table** — `ConfigValue` is four scalars with
no table kind, so they join `pmacs.lsp.config` / `pmacs.pair.sets`;
- the **two open-time settings resolve through the global chain**,
because they are read before the identity buffer exists; only
`terminal.escape-key` resolves per buffer;
- the escape cache lives on **`TerminalSession`** so its lifetime is
the terminal's. `value_epoch` alone is not a sufficient key: it does
not advance when focus moves between terminals with different
buffer-local values;
- repeating the escape sends **that chord**, not a hardcoded `0x03`.
- **Four bites, each against a different plausible wrong
implementation** — hardcoded ETX fails acc6/9; epoch-only cache key
fails acc7; single last-entry cache fails acc8's parse count; removing
the invalid-value fallback fails acc10. The first version of acc7
passed against the epoch-only bite because it asserted only that
terminal A still worked; the discriminating assertion is that **each**
terminal honors its own chord and not the other's.
- Test instruments worth reusing: `cat -v` is the echo probe, because the
screen rejects C0 controls before they reach cells so a raw echoed
`Ctrl-X` is invisible; and the probe **counts occurrences** rather than
testing presence, because a single-character probe collides with the
child's own banner text.
- **Review round 1 (2026-07-25) — five findings, all real, all fixed.**
One blocker and two majors were the same failure in three places: a
claim asserted somewhere cheaper than where it lives.
- *Blocker — `COHERENCE.md` was stale in four places, not the three
reported.* Step 8 still read "no keybinding"; §11 still read "five
settings"; and §6's dispatch table still cited
`is_terminal_escape_chord`, **a symbol this PR deletes**. §25 makes
that update ride the PR. A PR that changes audited ground truth has
to re-grep the audit for its own symbols, not only for its topic.
- *Major — acceptance 5 was vacuous.* It asserted a registry
round-trip, so it stayed green with the setting's **only** consumer
deleted. It now opens a real terminal whose child overflows the
24-row screen, scrolls the view to its oldest retained row, and
asserts `LINE001` is present at 10,000 and absent at 0. **Asserting
a value was stored is not asserting anything reads it.**
- *Major — acceptance 8a asserted the session count, not the cache.*
An editor-side map with no purge hook — the exact rejected design —
leaks *while* sessions drain, so it passed. Fixed with a
`TerminalManager::escape_caches()` seam. **A lifecycle claim needs a
lifecycle observable.**
- *Moderate — `table.sort` over user-controlled profile keys.* A
table holding both a string and a numeric key raised `attempt to
compare number with string` **on the unknown-profile path**,
replacing the diagnostic being asked for; `%q` raised likewise on a
non-string `profile` argument. Both are partial functions applied to
user input **on a diagnostic path** — the error reporter was the
thing that failed.
- *Minor — the committed framing still said "not yet approved".*
- **Three new bites, each falsified by revert**: deleting the scrollback
consumer fails acc5 (and only acc5); restoring the raw-key sort
reproduces `attempt to compare string with number` verbatim; and
implementing the rejected editor-side map fails the new acc8a at
`left: 2, right: 1` **while passing the old session-count version** —
which is the review finding demonstrated rather than argued.
- Verification after the round-1 fixes, on the tree merged with
`githubsucks/main` @ `c93f9ee`: `cargo fmt --check` clean; strict
workspace Clippy clean; 1,832 default + 2,009 CRDT library tests;
`terminal_config_acceptance` **12/12 in both configurations**; vterm
Stage 1/2 9+10 / 6+6; config registry 16+16; bottom-panel Stage 1
46+46; M4 121; required GPU 202; `git diff --check` clean.
- `compile_mode_acceptance` fails 11/67 against the **real** user
config and passes 67/67 with an isolated `XDG_CONFIG_HOME` — the
known pre-existing trap, not this branch.
- **`vterm_stage3_acceptance::a37` fails on this machine — and fails
identically on the PR's own base `d152120`**, so it is not this
branch's regression. It is load-sensitive: it passed at `d152120`
once and failed at that same commit twenty minutes later, with a
second agent saturating the machine with `rustc` in between. Two
ways it lies, both worth knowing: it **silently returns `ok` when
`pmacs-gpu` is not built** in the same target dir (only
`PMACS_REQUIRE_GPU=1` promotes that skip to a failure, and the gate
list applies that flag to `-p pmacs-gpu`, a *different* package), and
it is **crdt-gated, so CI has never run it at all**. A green a37 in
a gate log means nothing unless the binary was built and the flag
was set. Needs its own lane; see the CI `crdt`-coverage lane on #168.
- `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 + framing MERGED; Stage 2A IN REVIEW
Stage 1 and the Stage 2 framing are on `main`. **Stage 2A is
implemented and in review.**
- **Stage 2A — portable branch `githubsucks/bottom-panel-stage2a`**,
worktree `../pmacs-bp-stage2a`, **canonical `main` @ `cf54270`
integrated** (review round 1, finding 4 — the terminal-config lane
#173 also changes `src/editor.rs`, so gates were rerun on the merge
result, not the old combination). 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.
- 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

98
docs/agent-handoff.md
View File

@ -1,11 +1,13 @@
# Agent handoff — cross-machine continuity
**Last updated: 2026-07-25, after the CRDT undo repro (#157) and the
inline-math landed-doc refresh (#172) — following the bottom-panel
landed-doc refresh (#156), the inline-math slice (#158), dired Stage 1
(#165) — the directory view — the GPU terminal input fix (#166), Lean 4
Stage 2 (#161), the dired framing (#164), 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 stages 3a and 3b (#167, #170)
landed — pmacs' first Lean language server — following the CRDT undo
repro (#157), the inline-math landed-doc refresh (#172), the
bottom-panel landed-doc refresh (#156), the inline-math slice (#158),
the first mathematical typesetting in pmacs, dired Stage 1 (#165) — the
directory view — the GPU terminal input fix (#166), Lean 4 Stage 2
(#161), the dired framing (#164), and find-file (#162),
the dired arc's Stage 0, and COHERENCE.md (#163), Lean 4 Stage 1 (#160), the
minimap blank-slab fix (#159), bottom-panel Stage 1 (#155), the
inline-math re-scout (#154), the vterm PTY-flake fix (#153), and the
GPU initial-target doc refresh (#152); and before that GPU
@ -28,16 +30,16 @@ 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` @ `ccf29e3` (the CRDT undo repro #157 atop 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**. The bullets
below describe the arcs in their own terms; this line is the
head-of-`main` anchor.
- `main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a #167, the 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**. 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
@ -46,6 +48,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

1661
docs/lean4-mode-framing.md
View File

File diff suppressed because it is too large Load Diff

658
docs/terminal-config-and-copy-mode-framing.md Normal file
View File

@ -0,0 +1,658 @@
# Terminal configuration and copy mode
**Revision 4 — scouted against canonical `main` @ `b889873` (protocol v20),
2026-07-25. APPROVED after four review rounds. Stage 1 is implemented on
branch `terminal-config` (PR #173); Stage 2 (`terminal-copy-mode`) is
framed but not started, and branches off `main` after Stage 1 merges.**
Revision 4 gives the escape-key cache an owner and a lifecycle (Q#TC4c) —
revision 3 named the key but not the storage, and two implementations
satisfied its acceptance while behaving differently on A→B→A. It also corrects
the read-only deferral, which understated the substrate required: the bypass
path is `ensure_writable`-guarded too, so genuine immutability alone would
break every generated buffer that refreshes.
Revision 3 corrects two design errors and decides the chords. The
round-trip failure shape in revision 2 was **wrong in the reporter's favour**:
a Lua intercept does not set `Buffer::read_only`, and there is no Lua binding
that does, so an optimistic `CrdtOp` bypasses the intercept *and* passes
`ensure_writable()` — the daemon buffer mutates too, rather than the mirror
diverging alone (Q#TC6a). Revision 2 also had all three settings resolving
against the terminal identity buffer, which is impossible for the two read
*before* that buffer exists (Q#TC2b). Chords are now decided and
collision-scouted rather than deferred to implementation (Q#TC10, Q#TC8a).
Revision 2 answered seven review findings. Four were load-bearing: the settings
are `Live`, so the registry **accepts buffer-local overrides whether or not we
want them**, and `value_epoch()` does not move on a buffer switch — an
epoch-only cache can serve the wrong terminal's escape chord (Q#TC4); the
double-escape byte is a hardcoded `0x03`, so a configured escape would still
send Ctrl-C and make its own literal chord unreachable (Q#TC4b); the snapshot
buffer needs `set_round_trip_input`, not only a read-only intercept, or a
semantic frontend can optimistically edit it before daemon dispatch (Q#TC6);
and the two stages must be two branches and two PRs. Revision 1's
materialized-copy reframe is unchanged.
Two stages, one arc, no protocol change:
- **Stage 1 — configuration.** Terminal profiles, scrollback, and the escape
key become configurable. Today the terminal has **zero** configuration
surface: the `terminal` command hardcodes `os.getenv("SHELL") or "/bin/sh"`,
`scrollback_rows` is a per-open argument only, and the escape chord is a
literal in Rust.
- **Stage 2 — copy mode and search over scrollback.** A command that turns
the retained terminal screen and scrollback into an ordinary buffer, where
isearch, motion, selection, and the kill ring already work.
Explicitly **not** in this arc: the panel terminal (blocked on bottom-panel
Stage 2), and shell integration (cwd tracking, prompt marks, command zones) —
the keystone that unlocks the VS Code-style cluster, which needs its own
security framing because it decides what a child process may make the editor
do.
## Branch and PR plan
**Two branches, two PRs.** Configuration and copy mode are independently
releasable and have no dependency on each other; one framing covers the arc,
but the one-feature/one-branch/one-PR rule governs the implementation.
1. `terminal-config` — Stage 1. Also carries the **terminal opening
keybinding** (Q#TC10).
2. `terminal-copy-mode` — Stage 2, branched off `main` after Stage 1 merges.
Sequencing is not a dependency but avoids a conflict: both stages edit
`builtin/runtime/terminal.lua`.
## Ground truth (measured, not recalled)
Three facts constrain the design, and two of them rule out the obvious plan.
### 1. Terminal profiles cannot be a config-registry setting
`ConfigValue` is **four scalars** — `Bool`, `Int`, `Num`, `Str`
(`src/config_registry.rs:312`) — and its own doc comment says they "are never
stored --- only these four scalars (Q#CR3)". `ConfigKind` adds `Enum`, which
is physically a string validated against choices fixed at `define` time
(`src/config_registry.rs:115-145`). There is no table, list, or map kind.
A terminal profile is inherently a table: `{ command, args, cwd, env }` per
name. **Table-valued settings are an existing named deferral of the config
registry arc** — the same gap that keeps `pmacs.lsp.config`,
`pmacs.pair.sets`, `pmacs.comment.strings`, and the `pmacs.parse.*` proxies as
raw Lua. Profiles join that list rather than forcing that deferral open here.
### 2. Search cannot reuse isearch in place over a terminal
`SearchStore::set(buffer_id, query, matches: Vec<ByteRange>)`
(`src/search.rs:99`) keys matches by buffer and addresses them as **byte
ranges into that buffer's rope**; the painting path materializes the source
with `buf.snapshot_rope().slice(0, buf.len(), ..)` (`src/search.rs:435`).
A terminal identity buffer is **empty and read-only** by construction. Its
content lives in `TerminalScreen` as cells addressed by `(row, col)` across
history plus visible rows — there are no rope bytes to range over. Searching a
terminal in place therefore means a second, parallel search facility with its
own match store and its own highlight path, because terminal painting consumes
owned cells and not document style spans.
### 3. An in-place copy mode would be the seventh dispatch shadow
`dispatch_key`'s terminal-transport arm intercepts **every** key before
ordinary keymap dispatch whenever `active_terminal_key` is `Some`, which keys
purely on `is_terminal(window.buffer_id)` (`src/editor.rs:1098-1107`,
`973-1016`). A mode that keeps the terminal buffer focused while rebinding
keys to motion/selection must therefore add a new precedence rung.
`COHERENCE.md` §6 grades that ladder **weak, "and growing by one island per
modal feature"**, records that **no transient-keymap mechanism exists to
migrate to** (`KeymapStack` has exactly three fixed scopes, no layer stack, no
push/pop, no lifetime), and notes that `describe-key` already lies while a
shadow is active. It also names the counter-example: the entire picker/panel
family uses ordinary **buffer-local keymaps** and is inspectable and
rebindable.
### 4. What already exists and is reusable
- `retained_rows(projection)` (`src/terminal/view.rs:539`) iterates history
plus visible rows; `copy_selection_bytes(rows, selection)`
(`src/terminal/view.rs:849`) serializes a range with the fidelity Stage 2
criterion 21 already pins — soft wraps joined, hard rows separated, trailing
default blanks trimmed, wide glyphs and combining clusters copied once.
- `ConfigRegistry::value_epoch()` (`src/config_registry.rs:1127`) is public and
monotonic — cheap invalidation for a hot-path cache.
- The Lua surface is `define` / `get` / `set` / `set_local` / `on_change` with
a disposable handle (`src/lua_bindings/config.rs`).
- `pmacs.terminal.open` already accepts
`command, args, cwd, env, name, rows, cols, scrollback_rows, display,
window`. **`display = "panel"` already works** (bottom-panel Stage 1) — the
panel terminal is blocked on rendering, not on this surface.
- Terminal buffers already carry buffer-local bindings (`M-w`, `M-v`, `C-v`,
`M-<`, `M->`) installed by `terminal.open` in `builtin/runtime/terminal.lua`.
## Stage 1 — configuration
**Q#TC1 — Profiles are a raw Lua table, not a setting.**
`pmacs.terminal.profiles` maps a name to a spec table, exactly following the
`pmacs.lsp.config` precedent. The registry holds only scalars. Rejected
alternative: widening `ConfigValue` with a table kind — that is the config
arc's own named deferral, it is cross-cutting (persistence, `describe-setting`
rendering, the `custom-file` question all key on the scalar assumption), and
smuggling it into a terminal PR would be the wrong place to decide it.
**Q#TC2 — `terminal.default-profile` is `String`, not `Enum`.** `Enum`
choices are frozen at `define` time; profiles are user-extensible from
`init.lua` and later. Validation happens at open time, and an unknown name
must produce a pointed error that **names the known profiles**, not a bare
"unknown profile".
**Q#TC2a — the exact settings, defaults, and bounds.** All three are `Live`
(see Q#TC2b), and every default reproduces today's behavior exactly, so a tree
with no settings written behaves identically (acceptance 12).
| name | kind | default | bounds |
|---|---|---|---|
| `terminal.default-profile` | `String { allow_empty: true }` | `""` | — |
| `terminal.scrollback-rows` | `Integer` | `10_000` (`DEFAULT_TERMINAL_SCROLLBACK_ROWS`) | `0 ..= 4_000_000` (`MAX_TERMINAL_HISTORY_CELLS`) |
| `terminal.escape-key` | `String { allow_empty: false }` | `"C-c"` | parsed as a chord |
**Zero is a legal scrollback value meaning "retain no history".** The core's
own validation rejects only values *above* `MAX_TERMINAL_HISTORY_CELLS`
(`src/terminal/session.rs:114`), so `scrollback_rows = 0` is accepted through
`terminal.open` today. A `1` minimum here would invent an asymmetry between the
setting and the per-open field for no reason.
`""` is the **"no default profile" sentinel**: an empty string means "fall
through to `$SHELL`", not "a profile named empty". `allow_empty: true` exists
precisely to express it, and the open path treats empty and unset identically.
**Q#TC2b — the settings are `Live`, and the registry therefore accepts
buffer-local overrides. That is specified rather than accidental.**
`ConfigRegistry::set_local` refuses only `StartupOnly` definitions
(`src/config_registry.rs:949`); a `Live` setting can be pinned per buffer by
anyone. Declaring these global-only is **not currently expressible** — a
`scope = "global"` define flag is one of the config registry's own named
deferrals, and `autosave.interval-ms` already has the same latent problem.
Making them `StartupOnly` instead would buy enforcement at the cost of the
feature: the escape key could never be changed mid-session, which kills Q#TC4's
whole point. So they stay `Live`, and resolution is defined **per setting,
because the three are not read at the same moment**:
| setting | read when | resolution |
|---|---|---|
| `terminal.escape-key` | every keystroke in a terminal (cached) | `get(name, terminal_buffer)` — **buffer-local → global → default** |
| `terminal.default-profile` | once, **before** the terminal exists | `get(name)` — **global chain only** |
| `terminal.scrollback-rows` | once, **before** the terminal exists | `get(name)` — **global chain only** |
The split is forced, not stylistic. The two open-time settings are consumed by
`_open` **before it creates the identity buffer**, so there is no terminal
buffer to resolve against — and no caller could have pinned a local override on
a buffer that does not yet exist. `pmacs.config.get(name)` with no buffer
argument already means exactly "the global chain, never an ambient buffer", so
this is the registry's existing semantic rather than a new rule.
Consequences, stated so they are not discovered later:
- a per-terminal escape key is a supported feature, not a bug;
- `set_local` on `terminal.default-profile` or `terminal.scrollback-rows` is
**always inert**, for any buffer, because the open path never consults a
buffer chain. This is deliberate; the alternative — resolving against
whichever buffer happened to be current at open time — would make a
terminal's scrollback depend on what the user was looking at when they
pressed the key.
Rejected alternative: resolving the open-time settings against the *target
window's pre-open buffer*. It is expressible, but it makes an ambient buffer
load-bearing for a value the user set globally, which is the trap
`pmacs.config`'s two-argument/one-argument split exists to avoid.
**Q#TC3 — `terminal.scrollback-rows` is `Integer` with bounds, and an explicit
per-open `scrollback_rows` still wins.** The precedence is
**explicit argument over global setting** — there is no ambient buffer in this
chain at all (Q#TC2b resolves it through `get(name)`), so the rule is simply
that what a caller passes to `terminal.open` beats what the user configured
globally. The bounds above come from the existing validation, so the setting
cannot express a value the core will reject.
**Q#TC3a — profile resolution order, field by field.** `profile` is accepted
by **`pmacs.terminal.open` as well as the command**, so a Lua caller is not
forced through the command to use one. For each field, the first source that
supplies it wins:
1. an explicit `pmacs.terminal.open` field;
2. the named profile's field — `profile` argument, else
`terminal.default-profile` when non-empty;
3. the scalar setting, where one exists (`scrollback_rows` only);
4. the built-in fallback (`command` = `$SHELL`, else `/bin/sh`).
`env` is the one field where "first wins" is ambiguous, so it is stated:
profile `env` and explicit `env` are **merged**, with explicit entries
overriding profile entries of the same name. Any other reading silently drops
half a user's environment.
An explicitly passed `profile` that does not exist is an error even when
`terminal.default-profile` is valid — a typo must not silently fall back to
the default.
**Q#TC4 — `terminal.escape-key` is a `String` chord spelling, parsed once and
cached by `(buffer_id, value_epoch)`.** `is_terminal_escape_chord`
(`src/editor.rs:4413`) currently compares against a literal `C-c`. Reading and
parsing a setting on **every keystroke in a terminal** is not acceptable in
that path.
**The cache key must include the buffer.** `value_epoch()` advances only on
`set` / `set_local` / removal (`src/config_registry.rs:918`, `970`, `1011`,
`1029`) — **it does not move when the focused terminal changes**. An
epoch-only cache therefore serves terminal A's escape chord to terminal B for
as long as no setting is written, which is exactly the case where nothing looks
wrong. Keying on `(buffer_id, value_epoch)` is the minimum correct identity.
**Q#TC4c — the cache lives on `TerminalSession`, so its lifecycle is the
terminal's.** Revision 3 named the key `(buffer_id, value_epoch)` but not the
storage, and the two obvious storages behave differently on A→B→A:
- a **single last-entry cache** reparses on every switch between two
terminals, and re-reports an invalid value each time — a status line that
scolds you for a setting you already know about, forever;
- an **editor-side map** preserves "parsed and reported once" but **leaks an
entry per terminal** unless something purges it, and that purge is a second
thing to get wrong.
`TerminalSession` (`src/terminal/session.rs:215`) is created in
`TerminalManager::open` and dropped on kill/prune, so putting the cache there
gets the lifecycle for free with no purge hook to forget. It carries the parsed
chord, the `value_epoch` it was parsed at, and whether the current invalid
value has already been reported.
**"Reports once" means once per terminal, per effective invalid value.**
A→B→A must not re-report. Changing the setting from one invalid value to a
*different* invalid value **does** re-report, because that is new information
about a new mistake.
**The reporting channel is `EditorCore::status`** — the same channel
`send_terminal_bytes` already uses for terminal failures
(`src/editor.rs:1122`). Explicitly **not** `pmacs.error`: it is not installed
as a module anywhere in `src/lua_bindings`, so its call sites across the
runtime are dead, and a report sent there would be a report nobody sees.
**Q#TC4a — an unparseable escape key must not brick terminal input.** A bad
value falls back to `C-c` and reports once. The failure mode this avoids is
severe: with no escape chord, every key goes to the child and the user cannot
reach any editor binding to fix the setting that broke it.
**Q#TC4b — repeating the configured escape sends THAT chord to the child, not
Ctrl-C.** The double-escape arm currently writes a hardcoded
`&[0x03]` (`src/editor.rs:988`). With `terminal.escape-key = "C-x"`, `C-x C-x`
would send Ctrl-C — and literal Ctrl-X would become unreachable, since the
first `C-x` is always consumed as the escape. The repeat arm must encode the
**configured** chord through the existing `crate::terminal::input::encode_key`
path, which is also how it inherits application-cursor and modifier handling
rather than growing a second encoder.
Corollary worth pinning: after changing the escape away from `C-c`, an ordinary
`C-c` must reach the child as `0x03` like any other unescaped key.
**Q#TC5 — the `terminal` command gains an optional profile argument** and
otherwise keeps its current behavior; `$SHELL` remains the fallback when no
profile is configured. No existing invocation changes meaning.
**Q#TC10 — the terminal opening keybinding is pulled forward into Stage 1.**
`COHERENCE.md` Priority 1 names "a terminal keybinding" as part of protecting
the golden journey, §2 step 8 grades the terminal "works but undiscoverable",
and this stage already edits `terminal.lua`. Panel rendering imposes no
dependency on binding a command that already exists. Close/kill semantics stay
with the panel work, where the entry and exit points get designed together.
The chord is **decided and scouted, not deferred**: `C-c t`, global. See
Q#TC8a for the collision evidence and for why binding under the existing `C-c`
prefix is a new leaf rather than a shadow.
## Stage 2 — copy mode and search
**Q#TC6 — copy mode MATERIALIZES into an ordinary buffer. It does not add a
dispatch shadow.**
`M-x terminal.copy-mode` snapshots the retained rows into a read-only,
path-less buffer (`*terminal-copy: NAME*`) and displays it. That buffer is an
ordinary document buffer, so:
- **isearch works, with no new search substrate** — it is a rope, so
`SearchStore` and the existing match-painting path apply unchanged. Ground
truth 2 is answered by not fighting it.
- **motion, selection, `M-w`, the kill ring, even `M-x occur`-style consumers
work** — everything that operates on a buffer.
- **The "keys must not reach the child" problem dissolves structurally.**
`active_terminal_key` keys on `is_terminal(window.buffer_id)`; the snapshot
buffer is not a terminal, so the transport arm never fires. No new guard, no
new precedence rung, and ground truth 3's coherence cost is avoided rather
than paid.
- **`describe-key` stays truthful**, because the bindings are buffer-local and
inspectable — the idiom `COHERENCE.md` §6 identifies as the right side of
the line.
**Q#TC6a — the snapshot is BOTH intercept-read-only AND round-trip-marked,
and `set_round_trip_input` is the ONLY thing standing between a replica
frontend and unauthorized mutation.**
The established idiom is two calls: `listview.lua:106` and `compile.lua:272`
each pair `pmacs.buffer.add_intercept` with
`pmacs.buffer.set_round_trip_input(buf, true)`. Revision 2 described the
intercept as the guard and round-trip as defence in depth. **That was wrong,
and the correction matters:**
- A Lua intercept guards the **dispatch/edit** path only. It does **not** set
`Buffer::read_only`, which is "deliberately independent of edit intercepts"
(`src/buffer.rs:493-500`) — that flag is what makes terminal identity buffers
reject rope, undo/redo, and remote-CRDT mutation alike.
- **No Lua binding sets `read_only` at all.** The whole `src/lua_bindings`
tree only ever *reads* it (`fold.rs:313`). A Lua-created "read-only" buffer
is therefore read-only against dispatch and nothing else.
- So an optimistic `CrdtOp` from a semantic frontend bypasses the intercept
**and passes `ensure_writable()`**. It is applied. The daemon buffer mutates
in lockstep with the mirror — the user silently edits a buffer the editor
told them is read-only. There is no divergence to notice, which is worse
than divergence.
`set_round_trip_input` prevents this at the only point it can be prevented: it
makes `dispatch_idle_for` report false while the buffer is focused, so the
frontend never applies optimistically and never emits the op. It is not
hardening — it is the guard.
Two things follow, and both are recorded rather than fixed here:
- **The same exposure exists today** for every Lua-created read-only buffer —
listview panels and `*compilation*` included. They are correct only because
they call `set_round_trip_input`. This arc must not be the place that
unilaterally changes that substrate.
- **Exposing `Buffer::set_read_only` to Lua** would make these buffers
genuinely immutable at the rope/CRDT boundary the way terminal identity
buffers are, turning round-trip back into real defence in depth. That is a
substrate change affecting listview and compile as much as this snapshot, so
it is named in Deferred with its own lane.
**Q#TC7 — the materializer reuses the existing serializer.** A whole-range
variant of `copy_selection_bytes` over `retained_rows` inherits the criterion
21 fidelity rather than re-deriving soft-wrap, wide-glyph, and trailing-blank
behavior. Writing a second serializer would guarantee the two drift.
**Q#TC8 — one snapshot buffer per terminal, reused on re-invoke.** Re-running
the command against the same terminal replaces the contents in place rather
than accumulating buffers. It is killed with its terminal; killing the
snapshot alone leaves the terminal untouched.
**Q#TC8a — the chords, decided and collision-scouted.**
Worth stating first because it is easy to get backwards: in a terminal window
every **unescaped** key goes to the child, so terminal-local bindings are
reached as `<escape> <key>`. The existing `M-w` copy is physically `C-c M-w`.
The escape consumes itself and the next key starts a fresh ordinary sequence,
which is also why `C-c`-leading bindings are structurally unreachable *inside*
a terminal.
| action | scope | binding | physically typed |
|---|---|---|---|
| open a terminal (Q#TC10) | global | `C-c t` | `C-c t` |
| enter copy mode | terminal buffer | `C-t` | `C-c C-t` |
| refresh snapshot | snapshot buffer | `g` | `g` |
| return to terminal | snapshot buffer | `q` | `q` |
Scouted against the real keymaps:
- **`C-c t` is free.** No bare global `C-c` binding exists; `C-c` is already a
live global prefix from `fold.lua:48-52` (`C-c @ …`), and `C-c C-k` is
buffer-scoped in compile/async. `C-c t` is a new leaf under an existing
prefix, not a shadow.
- **`C-t` is globally `edit.transpose-chars`** (`editops.lua:909`), and binding
it **buffer-locally is legitimate**: `keymap.bind`'s strictness rejects
binding a *prefix* of an existing sequence within a scope
(`keymap_bind_conflict_surfaces_at_bind_time` — "would shadow"), not
cross-scope shadowing, which is what scopes are for. Listview already binds
`n`/`p`/`g`/`q`/`RET`/`SPC` buffer-locally. Transpose-chars is meaningless in
a read-only terminal buffer.
- `C-c C-t` matches emacs-libvterm's own `vterm-copy-mode` chord, so the muscle
memory transfers.
- `g` / `q` in the snapshot follow listview's precedent exactly.
**Named limitation:** `C-c t` cannot open a terminal *from inside* a terminal,
because `C-c` is consumed as the escape there. `M-x terminal` still works. This
is the documented consequence of Stage 2 criterion 19, not a new defect.
These are what make acceptance 21's `describe-key` claim testable: named
bindings, in named buffers, that introspection must report truthfully.
**Q#TC9 — the live-terminal keys stay.** `M-w`, `M-v`, `C-v`, `M-<`, `M->` on
the terminal buffer are the live affordances and do not change. Copy mode is
additive, on its own binding, and does not replace scroll-and-select.
## Bets
- **B1.** Materializing gives search for free: no second match store, no
second highlight path, no terminal-specific search UI. *Scored by Stage 2
landing with zero changes under `src/search.rs`.*
- **B2.** Point-in-time is sufficient for read-back/search/copy. *Scored by
use; if false, the live frozen mode in Deferred becomes the real feature and
this becomes its snapshot fallback.*
- **B3.** No protocol change. The snapshot is an ordinary buffer, so both
frontends render it with existing machinery. *Scored by the diff.*
- **B4.** The escape-key cache keyed by `(buffer_id, value_epoch)` never
becomes stale in a way a user can observe. *Scored by two acceptances, not
one: changing the setting mid-session (8) and two terminals with different
buffer-local values and no write between them (7). Revision 1's epoch-only
cache would pass the first and fail the second, which is why the bet now
names both.*
- **B5.** Buffer-local escape keys are a feature rather than a hazard.
*Unscored and honestly so: the registry cannot express global-only, so this
is what we get either way. If per-terminal escapes turn out to confuse more
than they help, the fix is the config registry's `scope = "global"` deferral,
not a terminal change.*
## Deferred (named)
- **Live frozen copy mode** (true `vterm-copy-mode` semantics: freeze the
terminal in place, navigate it, resume). Strictly larger; needs either the
transient-keymap primitive `COHERENCE.md` §6 specifies or a deliberate
seventh shadow.
- **Shell integration** — cwd tracking, prompt marks, command zones, and the
VS Code cluster downstream of it (command decorations, exit-code markers,
rerun, sticky scroll, terminal IntelliSense). Its own arc, with a security
framing.
- **Table-valued settings** — the config registry's own deferral. This arc
adds a **second** blocked adopter (after `pmacs.lsp.config` /
`pmacs.pair.sets`); worth recording as evidence when that deferral is
ranked.
- **A `scope = "global"` define flag** — also the config registry's own
deferral, and this arc is its second live case after `autosave.interval-ms`.
Until it exists, `set_local` on any `Live` setting is accepted whether or not
the owner wants it, so Q#TC2b specifies the behavior instead of pretending
it is prevented.
- **Panel terminal** — blocked on bottom-panel Stage 2 (semantic frontends are
not `panel_capable`). `display = "panel"` already exists and works on the
grid frontend.
- OSC 8 hyperlinks, images (sixel/kitty), `faint`/`blink`/`conceal`/
`strikethrough` (needs a shared `Style` widening, so a protocol bump),
cursor shape/blink, kitty keyboard protocol.
- Terminal session persistence/reconnect across editor restart.
- **A terminal close/kill command** — the remaining half of `COHERENCE.md`
§2 step 8's discoverability gap. It belongs with the panel-terminal work,
where entry and exit points get designed together. The *opening* keybinding
is **no longer deferred**: Stage 1 carries it as Q#TC10.
- **Genuine immutability for generated buffers — and it is bigger than a Lua
setter.** Today no Lua binding sets `read_only` (`src/lua_bindings` only
reads it, `fold.rs:313`), so every Lua-created "read-only" buffer — listview
panels, `*compilation*`, and this snapshot — is read-only against dispatch
alone and relies entirely on `set_round_trip_input` (Q#TC6a).
Merely **exposing `set_read_only` would break all three.** The
intercept-bypass path is `ensure_writable`-guarded too:
`apply_edit_skip_intercepts` calls it first (`src/buffer.rs:994`), and that
is exactly the primitive an owner uses to rewrite its own generated buffer.
Flipping the flag would stop listview refreshing, `*compilation*` streaming,
and this snapshot refreshing — the very operations those buffers exist for.
So the lane needs **two** things, not one: genuine immutability at the
rope/CRDT boundary, *and* an owner-authorized update path that is not simply
"skip the intercepts". Naming only the setter would have made it look like a
one-line follow-up.
## Acceptance
### Stage 1 — `terminal-config`
1. `pmacs.terminal.profiles` accepts a strict spec table per name and rejects
unknown fields before anything is spawned, matching `terminal.open`'s
existing transactional contract.
2. `terminal.default-profile` naming an unknown profile fails at open with an
error that **lists the known profile names**, and creates no buffer,
session, or process. An explicitly passed unknown `profile` fails the same
way **even when `terminal.default-profile` is valid** (Q#TC3a).
2a. That diagnostic is **total over a malformed profiles table** (review round
1). `pmacs.terminal.profiles` is a raw user table, so listing its names must
not assume its keys are comparable and rendering a requested name must not
assume it is a string: a table holding both a string and a numeric key made
`table.sort` raise `attempt to compare number with string` *on the
unknown-profile path*, replacing the exact error being asked for, and `%q`
raises on a non-string `profile` argument. Both are partial functions
applied to user input on a diagnostic path — the failure class is
"the error reporter is the thing that fails".
3. Field-by-field resolution follows Q#TC3a: explicit open field beats profile
field beats scalar setting beats `$SHELL`. `env` **merges**, with explicit
entries overriding profile entries of the same name.
4. `""` in `terminal.default-profile` means "no profile" and is
indistinguishable from unset (Q#TC2a).
5. `terminal.scrollback-rows` takes effect for a terminal opened without an
explicit `scrollback_rows`; an explicit per-open value overrides it; values
outside `0 ..= 4_000_000` are rejected by the registry rather than by the
core, and `0` is accepted as "retain no history".
6. `terminal.escape-key` changes which chord escapes to the editor, observed
through the **real dispatch path**, not by calling the predicate directly.
7. **Two terminals with different buffer-local escape keys each honor their
own**, with no setting written in between (Q#TC4/Q#TC2b). Driven as
**A→B→A**, asserting both directions. This is the pin an epoch-only cache
fails.
8. Across that same **A→B→A** switch with no setting written, the parse count
does **not** increase after each terminal's first keystroke (Q#TC4c) —
pinned by counting parses, not by timing. This is the pin a single
last-entry cache fails while still satisfying 7.
8a. A terminal's cache does not outlive it: killing a terminal and opening a
new one does not serve the dead terminal's chord, and no per-terminal cache
entry survives its session (Q#TC4c). This is the pin an unpurged
editor-side map fails.
9. With `terminal.escape-key = "C-x"`: `C-x C-x` sends **Ctrl-X** to the child,
and an ordinary `C-c` reaches the child as `0x03` like any other unescaped
key (Q#TC4b). Bite: against the hardcoded `&[0x03]`, the first assertion
fails.
10. An unparseable `terminal.escape-key` falls back to `C-c`, reports through
`EditorCore::status`, and leaves the terminal usable (Q#TC4a). Bite: with
the fallback removed, the terminal becomes unescapable.
10a. "Reports once" is once per terminal per effective invalid value
(Q#TC4c): an **A→B→A** switch with the same invalid value reports **once**,
while changing it to a *different* invalid value reports again. The report
count is asserted, not the message text.
11. The terminal opening keybinding invokes the existing command, and is
verified to have shadowed nothing (Q#TC10).
12. Existing `terminal` invocations and every existing terminal test behave
identically with no settings defined and no profiles registered.
### Stage 2 — `terminal-copy-mode`
13. `terminal.copy-mode` produces a read-only buffer whose text is
byte-identical to serializing the full retained range through the existing
copy path (Q#TC7) — pinned against the serializer, so the two cannot drift.
14. Soft wraps, hard rows, wide glyphs, combining clusters, and trailing
default blanks appear in the snapshot exactly as Stage 2 criterion 21 pins
them for selection copy.
15. isearch over the snapshot finds content that is **only in scrollback**
(scrolled off the visible screen), with no change to `src/search.rs` (B1).
16. **Ungated, runs in CI:** focusing the snapshot buffer makes
`dispatch_idle_for` report **false**. This is the whole mechanism Q#TC6a
depends on, it needs no CRDT, and it fails the moment
`set_round_trip_input` is dropped — so the load-bearing regression is
caught by the default configuration rather than only by a `crdt`-gated
test that CI never compiles.
17. **Through a semantic frontend** (this one does need CRDT): keys typed in
the snapshot buffer reach ordinary dispatch and never the child, and
**neither the daemon buffer nor the frontend's mirror is mutated**
(Q#TC6a). Bite: with `set_round_trip_input` removed, the optimistic op is
emitted, bypasses the Lua intercept, passes `ensure_writable()`, and
mutates **both sides** — a buffer the editor calls read-only silently
accepts an edit.
18. Re-invoking against the same terminal refreshes in place; the buffer count
does not grow (Q#TC8). Killing the snapshot leaves the terminal running;
killing the terminal removes the snapshot.
19. `C-t` in a terminal buffer (physically `C-c C-t`) enters copy mode; `g`
refreshes the snapshot from the live terminal and `q` returns to the source
terminal (Q#TC8a).
20. The live terminal's own keys are unchanged while a snapshot exists
(Q#TC9), and the terminal keeps following its tail.
21. The dispatch-shadow count is **unchanged at six** — pinned by asserting
`describe-key` reports the truth for the snapshot buffer's `g` and `q`,
which is the observable difference between the buffer-local idiom and a
shadow.
## Coherence impact (`COHERENCE.md` §20)
- **§6 Interaction islands — this arc deliberately adds none.** It is the
first modal-feeling terminal feature that resolves to the buffer-local
keymap idiom §6 identifies as correct, rather than a seventh rung on the
precedence ladder. The shadow count stays at six and `describe-key` stays
truthful (acceptance 21). Worth recording in §6 as a worked example that the
idiom scales to a case that looks modal.
- **§11 Configuration as typed, layered data** — the terminal gains its first
settings, and produces a second blocked adopter for **two** distinct registry
deferrals: the missing table-valued kind (profiles) and the missing
`scope = "global"` flag (the **two open-time settings** —
`terminal.escape-key` deliberately supports buffer-locals, so only
`default-profile` and `scrollback-rows` want an enforcement the registry
cannot express). §11's ground truth should
record both, because the argument for prioritizing them is now cumulative
rather than hypothetical.
- **§2 golden journey, step 8 — partially closed here.** Stage 1 carries the
**terminal opening keybinding** that Priority 1 explicitly names (Q#TC10),
which is the larger half of "works but undiscoverable". Close/kill stays with
the panel work so the entry and exit points are designed together, and is
named in Deferred rather than silently skipped.
- **§5 Unify discovery** — the new commands must carry real descriptions so
M-x rows are useful; no new introspection surface is added.
- No background-work attribution change; no new activity view; no protocol
change.
## Verification plan
Full gate suite per `CLAUDE.md` for each PR separately, plus:
- **The touched terminal suites in BOTH configurations** — default and
`--features crdt` — not only the CRDT one. `vterm_stage1_acceptance`,
`vterm_stage2_acceptance`, and `vterm_stage3_acceptance` all carry tests in
each, and acceptance 12 is a claim about the default configuration too.
- `cargo test --test config_registry_acceptance` for the new settings.
- New suites: `tests/terminal_config_acceptance.rs` (Stage 1) and
`tests/terminal_copy_mode_acceptance.rs` (Stage 2).
- Every behavioral claim bite-verified. The bites that matter most:
**7/8/8a** — three pins that fail against three *different* wrong cache
implementations (epoch-only key, single last-entry, unpurged map), which is
why one pin was not enough; **9** (a hardcoded `0x03` makes the configured
chord unreachable); **10** (its failure mode is a terminal nobody can
escape); and **16/17** (a read-only buffer that silently accepts an edit on
both sides).
- **The observation seams the cache pins need are `escape_parses` (how often)
and `escape_caches` (how many are still held).** Neither is inferable from
behavior: for a *valid* setting a correct per-session cache and a leaking
editor-side map produce identical keystroke results, and both leave the
session count draining normally. Review round 1 caught 8a asserting the
session count instead — which the unpurged-map bite passes, since a map with
no purge hook leaks *while* sessions drain. A lifecycle claim needs a
lifecycle observable; the count of live sessions is not one.
- **Criterion 5 must open a real terminal and read back retained history.**
Round 1 caught it asserting a registry round-trip instead, which is a test of
the registry: it stays green with the setting's only consumer deleted. The
same shape to watch for anywhere — *asserting that a value was stored is not
asserting that anything reads it*.
- **Do not gate the new suites on `#[cfg(feature = "crdt")]` unless a test
genuinely needs CRDT.** CI never enables that feature, so a suite gated that
way is written and then never run — 264 tests are currently dark for exactly
this reason. That measurement and its lane live on **PR #168**, which is open
and unmerged; it is not yet in `docs/active-work.md` on `main`.
Acceptance 17 does need a semantic frontend, so that one test is gated — but
acceptance 16 pins the same mechanism ungated, so the regression is caught in
CI regardless. That pairing is the pattern to reuse whenever a claim's
end-to-end proof needs CRDT.

54
src/bin/pmacs_fake_lsp.rs
View File

@ -483,6 +483,27 @@ fn main() {
}
});
write_frame(&mut stdout, &echo);
// Arc 8 Stage 3b: `leanprogress` mode emits one
// `$/lean/fileProgress` covering line 0, so the Lean
// subscriber can be pinned end-to-end through the real
// drain rather than by calling its handler directly.
if mode == "leanprogress" && uri.is_string() {
let progress = serde_json::json!({
"jsonrpc": "2.0",
"method": "$/lean/fileProgress",
"params": {
"textDocument": { "uri": uri, "version": 1 },
"processing": [{
"range": {
"start": { "line": 0, "character": 0 },
"end": { "line": 1, "character": 0 }
},
"kind": 1
}]
}
});
write_frame(&mut stdout, &progress);
}
// Also push a synthetic `publishDiagnostics`
// notification with two entries (one Error, one
// Warning) so M4.6 tests can exercise the store.
@ -1062,6 +1083,39 @@ fn main() {
});
write_frame(&mut stdout, &resp);
}
("textDocument/waitForDiagnostics", Some(idv)) => {
// Arc 8 Stage 3b: Lean's `WaitForDiagnosticsParams` is
// `{ uri, version }` (v4.9.0
// `src/Lean/Data/Lsp/Extra.lean`). Validated here rather
// than echoed, because the generic echo arm below
// accepts anything — which is exactly how a client
// sending only `uri` shipped looking correct. A client
// that omits `version`, or sends a non-integer, gets an
// InvalidParams error the way a real server would.
let uri_ok = params
.get("uri")
.and_then(serde_json::Value::as_str)
.is_some();
let version_ok = params
.get("version")
.and_then(serde_json::Value::as_i64)
.is_some();
let resp = if uri_ok && version_ok {
serde_json::json!({
"jsonrpc": "2.0", "id": idv, "result": serde_json::Value::Null
})
} else {
serde_json::json!({
"jsonrpc": "2.0",
"id": idv,
"error": {
"code": -32602,
"message": "waitForDiagnostics requires { uri, version }"
}
})
};
write_frame(&mut stdout, &resp);
}
(_, Some(idv)) => {
// Generic echo response.
let resp = serde_json::json!({

629
src/daemon.rs
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"
);
}
}

421
src/editor.rs
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"),
@ -436,6 +451,17 @@ impl EditorState {
include_str!("../builtin/runtime/lsp.lua"),
)
.expect("load lsp builtin chunk");
// Arc 8 Stage 3b: the Lean 4 language server. Loaded after
// lsp.lua because it registers `pmacs.lsp.config.lean4`,
// subscribes on the Stage 3a notification seam, and adds a
// `buffer.after-load` hook that must run AFTER lsp.lua's own
// (it reads the attachment lsp.lua creates).
lua_host
.eval(
Some("@pmacs/builtin/runtime/lean.lua"),
include_str!("../builtin/runtime/lean.lua"),
)
.expect("load lean builtin chunk");
// Arc 1a: the in-buffer completion popup driver. Loaded after
// lsp.lua because it drives `pmacs.lsp.request_completion` /
// `pmacs.lsp.attachment_for_request` and after the framework
@ -989,19 +1015,28 @@ impl EditorState {
.get(&frontend_id)
.is_some_and(|state| state.terminal_escape);
if let Some(view_key) = terminal_key {
// Q#TC4: the escape chord is per terminal, resolved through
// `terminal.escape-key` and cached on the session so this
// hot path parses at most once per (terminal, config epoch).
let escape_chord = self.terminal_escape_chord(view_key.buffer_id);
if escaped {
self.dispatchers
.entry(frontend_id)
.or_default()
.terminal_escape = false;
if chord.is_some_and(is_terminal_escape_chord) {
if chord == Some(escape_chord) {
// Q#TC4b: repeating the escape sends THAT chord to the
// child, not a hardcoded ETX. With a configured escape
// of `C-x`, sending Ctrl-C here would both surprise the
// user and make literal Ctrl-X unreachable, since the
// first press is always consumed as the escape.
self.claim_terminal_controller(view_key);
self.send_terminal_bytes(view_key.buffer_id, &[0x03]);
self.send_terminal_escape_literal(view_key, escape_chord);
return;
}
// The post-escape key starts a fresh ordinary sequence below.
} else if !dispatcher_pending {
if chord.is_some_and(is_terminal_escape_chord) {
if chord == Some(escape_chord) {
let state = self.dispatchers.entry(frontend_id).or_default();
state.terminal_escape = true;
state.dispatcher = KeyDispatcher::new();
@ -1117,6 +1152,54 @@ impl EditorState {
.then_some(key)
}
/// This terminal's effective escape chord (Q#TC4).
///
/// Resolution is `get("terminal.escape-key", terminal_buffer)` —
/// buffer-local, then global, then default — because unlike the two
/// open-time settings this one is read while the terminal exists, so
/// a per-terminal escape is expressible and supported (Q#TC2b).
///
/// The parse and the once-per-terminal invalid-value report both live
/// in [`crate::terminal::TerminalManager::escape_chord`]; this method
/// only supplies the resolved spelling and the epoch that keys the
/// cache, and surfaces any report through the status line — the same
/// channel `send_terminal_bytes` uses for terminal failures.
fn terminal_escape_chord(&self, buffer_id: crate::buffer::BufferId) -> Chord {
let lua = self.lua_host.lua();
let (spelling, epoch) = crate::lua_bindings::config_string_and_epoch(
lua,
"terminal.escape-key",
Some(buffer_id),
crate::terminal::DEFAULT_TERMINAL_ESCAPE_KEY,
);
let (chord, report) = self
.terminal_manager
.borrow_mut()
.escape_chord(buffer_id, epoch, &spelling);
if let Some(message) = report {
self.core.borrow_mut().status = message;
}
chord
}
/// Send the configured escape chord to the child as literal input
/// (Q#TC4b), through the same encoder ordinary keys use so it
/// inherits application-cursor and modifier handling.
fn send_terminal_escape_literal(&self, key: TerminalViewKey, chord: Chord) {
let event = KeyEvent::new(chord.code, chord.modifiers);
let Some((terminal_key, modifiers)) = terminal_key_from_crossterm(event) else {
return;
};
let modes = self
.terminal_manager
.borrow()
.modes_for_view(key)
.unwrap_or_default();
if let Some(bytes) = crate::terminal::input::encode_key(terminal_key, modifiers, modes) {
self.send_terminal_bytes(key.buffer_id, &bytes);
}
}
fn claim_terminal_controller(&self, key: TerminalViewKey) {
let mut manager = self.terminal_manager.borrow_mut();
let _ = manager.register_view(key);
@ -1341,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;
}
@ -1472,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
@ -3152,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.
///
@ -3261,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)
@ -3268,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());
}
}
@ -3349,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);
@ -4421,10 +4564,6 @@ fn sanitize_single_line(s: &str) -> String {
.collect()
}
fn is_terminal_escape_chord(chord: Chord) -> bool {
chord.code == KeyCode::Char('c') && chord.modifiers == KeyModifiers::CONTROL
}
fn terminal_key_from_crossterm(key: KeyEvent) -> Option<(TerminalKey, TerminalModifiers)> {
let modifiers = crate::protocol::crossterm_translate::mods_from_crossterm(key.modifiers);
let key = crate::protocol::crossterm_translate::keycode_from_crossterm(key.code);

75
src/lua_bindings/mod.rs
View File

@ -668,6 +668,33 @@ pub fn config_u32(lua: &Lua, name: &str, buffer_id: Option<BufferId>, fallback:
}
}
/// Read a `String` setting plus the registry epoch that keys any cache
/// built from it (Q#TC4c).
///
/// The epoch is returned WITH the value deliberately: a caller caching a
/// parsed form needs both, and reading them in two calls would let a
/// `set` land between them and produce a cache stamped with the wrong
/// epoch. `fallback` covers a bare core whose runtime never defined the
/// setting, matching [`config_u32`].
#[must_use]
pub fn config_string_and_epoch(
lua: &Lua,
name: &str,
buffer_id: Option<BufferId>,
fallback: &str,
) -> (String, u64) {
let Some(registry) = lua.app_data_ref::<config::SharedConfigRegistry>() else {
return (fallback.to_owned(), 0);
};
let borrowed = registry.borrow();
let epoch = borrowed.value_epoch();
let value = match borrowed.get(name, buffer_id) {
Ok(crate::config_registry::ConfigValue::Str(v)) => v.clone(),
_ => fallback.to_owned(),
};
(value, epoch)
}
/// Short-circuit a binding when the init phase has completed.
///
/// Lifecycle-affecting Lua APIs (currently just `pmacs.attach`; M5.6d+)
@ -6594,6 +6621,54 @@ pub fn install_async(
) -> mlua::Result<()> {
lua.set_app_data(runtime.clone());
let pmacs: Table = lua.globals().get("pmacs")?;
// Arc 8 Stage 3a (framing Q#LN20): the one *synchronous* filesystem
// primitive Lua has. `pmacs.fs` is otherwise an async, handle-
// returning surface built in `builtin/runtime/fs.lua`, so this
// arrives through a private table that file re-exports rather than
// joining the `_dispatch_fs_*` family it would not belong to.
//
// Installed here, alongside those dispatchers, purely for load
// order: `make_async_runtime` runs before `fs.lua` is evaluated,
// whereas `install_project` — the other plausible home — runs after
// it, so a canonicalizer placed there is nil when `fs.lua` reads it.
//
// Synchronous on purpose, and that is the whole point. The consumer
// is a function-valued `pmacs.lsp.config[lang].root`, which
// `project_root_for` calls from `ensure_server` <- `attach_buffer`
// <- the `buffer.after-load` hook — no coroutine, nothing to await
// on. An awaitable canonicalizer would be unusable there for exactly
// the reason `pmacs.fs.stat` already is, leaving #161's
// canonical-root obligation undischarged. The cost is one syscall on
// a path the editor is already opening; `pmacs.project.detect`
// canonicalizes synchronously on the same hook today.
{
let fs_priv = lua.create_table()?;
fs_priv.set(
"canonicalize",
lua.create_function(|_, path: String| {
// nil rather than an error for a path that cannot be
// resolved: asking about a deleted file or a broken
// symlink is ordinary, and raising would surface through
// `resolve_root_fn`'s pcall as a config bug, which it is
// not.
//
// `to_str`, NOT `display()`. A resolution that lands on
// non-UTF-8 bytes has no faithful string form, and
// `display()` would substitute U+FFFD and hand back a
// path that does not exist on disk — strictly worse than
// nil here, because this value becomes a server-affinity
// key via `file_uri_for` and would silently fail to
// round-trip. Unrepresentable is a decline, matching how
// the fs layer already treats non-UTF-8 symlink targets.
Ok(std::fs::canonicalize(&path)
.ok()
.and_then(|p| p.to_str().map(str::to_owned)))
})?,
)?;
pmacs.set("_fs", fs_priv)?;
}
let async_mod = lua.create_table()?;
{

100
src/semantic_render.rs
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"

74
src/statusline.rs
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)
}
}
}

4
src/terminal/mod.rs
View File

@ -34,6 +34,10 @@ pub use pmacs_protocol::terminal::{
/// Configuration-time, not a wire bound: history never crosses the
/// protocol, so this stays core-owned.
pub const DEFAULT_TERMINAL_SCROLLBACK_ROWS: usize = 10_000;
/// Default `terminal.escape-key`, and the fallback an unparseable value
/// falls back to (Q#TC4a).
pub const DEFAULT_TERMINAL_ESCAPE_KEY: &str = "C-c";
/// Maximum retained main-screen history cells. Core-owned for the same
/// reason as [`DEFAULT_TERMINAL_SCROLLBACK_ROWS`].
pub const MAX_TERMINAL_HISTORY_CELLS: usize = 4_000_000;

122
src/terminal/session.rs
View File

@ -12,6 +12,7 @@ use crate::ansi::AnsiParserProfile;
use crate::buffer::{Buffer, BufferId};
use crate::cell::{Cell, CellCoord, CellSize};
use crate::editor_core::EditorCore;
use crate::key::{Chord, parse_chord};
use crate::process::{
ProcessEventKind, ProcessId, ProcessMode, ProcessSpec, ProcessState, ProcessSupervisor,
RestartPolicy, StdinMode, TerminalMode,
@ -218,12 +219,40 @@ pub(super) struct TerminalSession {
pub(super) screen: TerminalScreen,
pub(super) process: TerminalProcessState,
pub(super) annotated: bool,
/// Resolved `terminal.escape-key` for this terminal (Q#TC4c).
///
/// The cache lives HERE, not in an editor-side map, because a
/// session is created in [`TerminalManager::open`] and dropped on
/// kill/prune — so its lifetime is exactly the cache's, with no
/// purge hook to forget. An editor-side map would leak an entry per
/// terminal; a single last-entry cache would reparse (and re-report
/// an invalid value) every time focus alternates between two
/// terminals.
pub(super) escape: Option<EscapeCache>,
}
/// One terminal's parsed escape chord, valid for one config epoch.
pub(super) struct EscapeCache {
/// The `ConfigRegistry::value_epoch` this was parsed at. The key is
/// `(this session, epoch)`: the epoch alone is not enough, because
/// it does not advance when focus moves between terminals with
/// different buffer-local values.
pub(super) epoch: u64,
/// The effective chord — the parsed spelling, or the `C-c` fallback.
pub(super) chord: Chord,
/// The invalid spelling already reported for this terminal, if any.
/// Reporting is once per terminal per effective invalid value: an
/// unchanged bad value stays quiet, a *different* bad value reports
/// again because it is a new mistake.
pub(super) reported_invalid: Option<String>,
}
/// Owns the one-buffer/one-process/one-screen terminal registry.
#[derive(Default)]
pub struct TerminalManager {
pub(super) sessions: HashMap<BufferId, TerminalSession>,
/// Total escape-key parses performed (Q#TC4c observability).
escape_parses: u64,
process_to_buffer: HashMap<ProcessId, BufferId>,
/// Removed buffers whose children are still being reaped. Their events
/// remain manager-owned so Lua/LSP/MCP consumers cannot steal a batch.
@ -331,6 +360,7 @@ impl TerminalManager {
screen,
process: TerminalProcessState::Running,
annotated: false,
escape: None,
},
);
debug_assert!(previous.is_none(), "fresh BufferId collided");
@ -538,6 +568,89 @@ impl TerminalManager {
.map_err(TerminalError::Process)
}
/// Resolve this terminal's effective escape chord, parsing at most
/// once per `(terminal, config epoch)` (Q#TC4c).
///
/// `spelling` is the caller-resolved `terminal.escape-key` value and
/// `epoch` the registry's `value_epoch()` it was read at. Returns the
/// effective chord plus, at most once per terminal per effective
/// invalid value, a message the caller should surface.
///
/// An unparseable spelling falls back to `C-c` rather than leaving the
/// terminal with no escape at all (Q#TC4a): without one, every key goes
/// to the child and the user cannot reach the binding that would fix
/// the setting that broke it.
pub fn escape_chord(
&mut self,
buffer_id: BufferId,
epoch: u64,
spelling: &str,
) -> (Chord, Option<String>) {
let fallback = default_escape_chord();
if let Some(session) = self.sessions.get(&buffer_id)
&& let Some(cache) = session.escape.as_ref()
&& cache.epoch == epoch
{
return (cache.chord, None);
}
self.escape_parses = self.escape_parses.saturating_add(1);
let Some(session) = self.sessions.get_mut(&buffer_id) else {
return (fallback, None);
};
let previously_reported = session
.escape
.as_ref()
.and_then(|cache| cache.reported_invalid.clone());
let (chord, reported_invalid, report) = match parse_chord(spelling) {
Ok(chord) => (chord, None, None),
Err(error) => {
let already = previously_reported.as_deref() == Some(spelling);
let message = (!already).then(|| {
format!(
"terminal.escape-key {spelling:?} is not a valid chord ({error}); using C-c"
)
});
(fallback, Some(spelling.to_owned()), message)
}
};
session.escape = Some(EscapeCache {
epoch,
chord,
reported_invalid,
});
(chord, report)
}
/// How many escape-key spellings this manager has parsed.
///
/// An observability seam for Q#TC4c's cache contract, which is
/// otherwise unpinnable for a VALID setting: a correct per-session
/// cache and a single last-entry cache produce identical behavior
/// there and differ only in how often they parse. Counting reports
/// covers the invalid case; this covers the valid one.
#[must_use]
pub fn escape_parses(&self) -> u64 {
self.escape_parses
}
/// How many terminals currently hold a cached escape chord.
///
/// The LIFETIME half of Q#TC4c's cache contract, which `escape_parses`
/// cannot cover: parse counting says a valid setting is read once, but
/// says nothing about whether the cache is ever released. Because the
/// cache lives on [`TerminalSession`], this count falls with the
/// session set by construction — which is exactly the property worth
/// pinning, since the rejected alternative (an editor-side
/// `HashMap<BufferId, EscapeCache>`) has no purge hook and would hold
/// this at its high-water mark while sessions drained.
#[must_use]
pub fn escape_caches(&self) -> usize {
self.sessions
.values()
.filter(|session| session.escape.is_some())
.count()
}
/// Resize a terminal screen and its PTY after validating shared limits.
pub fn resize(
&mut self,
@ -730,3 +843,12 @@ fn sanitize_metadata(value: &str) -> String {
}
clean
}
/// The built-in terminal escape chord, and the fallback for an
/// unparseable `terminal.escape-key` (Q#TC4a).
pub(super) fn default_escape_chord() -> Chord {
Chord::new(
crossterm::event::KeyCode::Char('c'),
crossterm::event::KeyModifiers::CONTROL,
)
}

15
src/window.rs
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

898
tests/bottom_panel_stage2a_acceptance.rs Normal file
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:?}"
);
}

1882
tests/lean4_server_acceptance.rs Normal file
View File

File diff suppressed because it is too large Load Diff

62
tests/lean4_stage1_acceptance.rs
View File

@ -305,36 +305,50 @@ fn acc11b_an_unknown_fence_name_still_injects_nothing() {
// ---------------------------------------------------------------------------
#[test]
fn acc12_stage1_ships_no_lsp_config_and_spawns_no_process() {
// Stage 1 is grammar + Lua tables only. Opening a Lean file must not
// reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and
// even then it is fallible by design (Q#LN7).
fn acc12_opening_lean_spawns_no_process_without_a_server_config() {
// **Superseded in half by Stage 3b.** This criterion originally also
// asserted `pmacs.lsp.config.lean4 == nil`, guarding against a Stage-3
// front-run. Stage 3b *is* Stage 3: `builtin/runtime/lean.lua` now ships
// that config deliberately, and its shape is pinned by
// `tests/lean4_server_acceptance.rs`. Asserting the absence here would
// now pin the opposite of the intended behavior, so it is gone rather
// than weakened.
//
// What survives is the half that was always about *restraint*, and it
// matters more now than it did in Stage 1 — it is what holds Q#LN7's
// "not at init" promise. `pmacs.lsp.config` is a declarative table, and
// spawning a process at startup for every user, Lean-using or not, is
// the cost rev 1 refused. Both the `lake serve` spawn and the
// `lake --version` probe are gated on a real Lean attachment.
// The load-bearing assertion, and it must run against a PRISTINE editor.
// The shared `editor()` helper wipes `pmacs.lsp.config` before any
// buffer opens, so an assertion about the server list under that harness
// holds for every language regardless of what Stage 1 ships — it could
// not fail for the regression it names. This checks the real claim
// directly: no builtin runtime file defines a Lean server config. A
// Stage-3 front-run adding `pmacs.lsp.config.lean4` fails here.
// Constructing an editor touches no process, even though the Lean
// config now exists and names `lake`.
let pristine = EditorState::new();
let no_lean_config: bool = eval(&pristine, "return pmacs.lsp.config.lean4 == nil");
assert!(
no_lean_config,
"Stage 1 defines no `pmacs.lsp.config.lean4`; the LSP is Stage 3"
let at_init: i64 = eval(&pristine, "return #pmacs.process.list()");
assert_eq!(
at_init, 0,
"constructing an editor must not probe or spawn for Lean"
);
// Non-vacuity for the assertion above: the config really is present and
// really does name a command, so "nothing spawned" is restraint rather
// than an empty table having nothing to act on.
let names_lake: bool = eval(
&pristine,
"return pmacs.lsp.config.lean4 ~= nil and pmacs.lsp.config.lean4.command == \"lake\"",
);
// Non-vacuity: the same lookup finds the configs that DO ship, so this
// is not passing because `pmacs.lsp.config` is empty or absent.
let rust_config_exists: bool = eval(&pristine, "return pmacs.lsp.config.rust ~= nil");
assert!(
rust_config_exists,
"the config table is populated, so the lean4 absence above is meaningful"
names_lake,
"Stage 3b ships a lean4 config naming `lake`, so the no-spawn \
assertion above is meaningful"
);
// And nothing is spawned by opening the file. This half retains its
// value under the wiped config: a direct probe spawn from `lean.lua`
// would show up here whatever `pmacs.lsp.config` contains.
// And opening a Lean buffer with no server configured spawns nothing —
// the `editor()` helper wipes `pmacs.lsp.config`, so this catches a
// probe that fires off the mode rather than off an attachment.
let s = editor_visiting("Basic.lean", "def x : Nat := 1\n");
let procs: i64 = eval(&s, "return #pmacs.process.list()");
assert_eq!(procs, 0, "opening a Lean buffer spawns no child process");
assert_eq!(
procs, 0,
"with no server configured, opening a Lean buffer spawns nothing"
);
}

724
tests/lsp_dispatch_seams_acceptance.rs Normal file
View File

@ -0,0 +1,724 @@
//! Arc 8 Stage 3a acceptance — LSP notification/response dispatch seams
//! and `pmacs.fs.canonicalize`.
//!
//! `docs/lean4-mode-framing.md` Q#LN9 and Q#LN20, acceptance 29–34 plus
//! 34a/34b.
//!
//! This suite deliberately contains **no Lean content**.
//! `handle_server_requests` (`builtin/runtime/lsp.lua`) is the single
//! LSP event drain for every language in pmacs, so the change is
//! exercised through an already-shipped language driven against
//! `pmacs_fake_lsp`. A suite that reached the drain only through Lean
//! would understate the blast radius — the same reasoning that shaped
//! Stage 2's suite.
//!
//! Every fixture calls `pmacs.project.set_search_boundary` at its own
//! tempdir root, so a stray marker above the temp directory cannot make
//! a "markerless" case silently detected.
use std::path::{Path, PathBuf};
use std::time::Duration;
use pmacs::editor::EditorState;
fn exec(state: &EditorState, source: &str) {
state.lua_host.lua().load(source.to_owned()).exec().unwrap();
}
fn eval<T: mlua::FromLuaMulti>(state: &EditorState, source: &str) -> T {
state.lua_host.lua().load(source.to_owned()).eval().unwrap()
}
fn fake_lsp_path() -> String {
env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned()
}
/// A fresh editor with the shipped language configs cleared, so the only
/// server any test can spawn is the fake one it configures itself.
fn editor() -> EditorState {
let state = EditorState::new();
exec(&state, "pmacs.lsp.config = {}");
state
}
fn lua_str(path: &Path) -> String {
path.display()
.to_string()
.replace('\\', "\\\\")
.replace('"', "\\\"")
}
struct Fixture {
_dir: tempfile::TempDir,
root: PathBuf,
}
impl Fixture {
fn new() -> Self {
let dir = tempfile::tempdir().unwrap();
let root = std::fs::canonicalize(dir.path()).unwrap();
Self { _dir: dir, root }
}
fn write(&self, rel: &str, contents: &str) -> PathBuf {
let path = self.root.join(rel);
std::fs::create_dir_all(path.parent().unwrap()).unwrap();
std::fs::write(&path, contents).unwrap();
path
}
fn dir(&self, rel: &str) -> PathBuf {
self.root.join(rel)
}
fn bind(&self, state: &EditorState) {
exec(
state,
&format!(
"pmacs.project.set_search_boundary(\"{}\")",
lua_str(&self.root)
),
);
}
}
fn configure(state: &EditorState, language: &str) {
exec(
state,
&format!(
"pmacs.lsp.config.{language} = {{ command = \"{}\" }}",
fake_lsp_path()
),
);
}
fn open(state: &EditorState, path: &Path) {
exec(
state,
&format!("pmacs.buffer.find_or_open(\"{}\")", lua_str(path)),
);
}
/// `tick_async` is what drives the drain: `handle_server_requests` is
/// wrapped onto `pmacs._async.tick`, so a settle loop without it moves
/// the LSP state machine while never delivering a single event to Lua.
fn settle(state: &mut EditorState) {
for _ in 0..8 {
state.tick_processes();
state.tick_lsp();
state.tick_async();
std::thread::sleep(Duration::from_millis(2));
}
}
/// A rust project with one file, an attached fake server, and the
/// probes below installed. Returns the opened file's path.
fn attached_rust(state: &mut EditorState, fx: &Fixture) -> PathBuf {
fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n");
let file = fx.write("proj/src/main.rs", "fn main() {}\nlet x = 1;\n");
fx.bind(state);
configure(state, "rust");
open(state, &file);
settle(state);
file
}
/// The sid of the single live server, as a Lua expression fragment.
const THE_SID: &str = "pmacs.lsp.list()[1].id";
// ---------------------------------------------------------------------------
// Acceptance 29 — a notification reaches a registered subscriber.
// ---------------------------------------------------------------------------
#[test]
fn acc29_notification_reaches_a_registered_subscriber() {
let fx = Fixture::new();
let mut state = editor();
// Registered BEFORE the open, so the didOpen-triggered `pmacs/echo`
// is in the first drain.
exec(
&state,
r#"
_G.seen = {}
pmacs.lsp.on_notification("pmacs/echo", function(sid, params)
_G.seen[#_G.seen + 1] = tostring(params and params.uri)
end)
"#,
);
attached_rust(&mut state, &fx);
let n: i64 = eval(&state, "return #_G.seen");
assert!(
n >= 1,
"expected at least one pmacs/echo notification, got {n}"
);
let first: String = eval(&state, "return _G.seen[1]");
assert!(
first.starts_with("file://") && first.ends_with("main.rs"),
"subscriber got the document uri; saw {first:?}"
);
}
#[test]
fn acc29_subscriber_for_an_unsent_method_does_not_fire() {
let fx = Fixture::new();
let mut state = editor();
exec(
&state,
r#"
_G.hits = 0
pmacs.lsp.on_notification("pmacs/never", function() _G.hits = _G.hits + 1 end)
"#,
);
attached_rust(&mut state, &fx);
// Non-vacuity for acc29: the seam is method-keyed, not a firehose.
// Without this, a subscriber invoked for every notification would
// pass the test above while being wrong.
let hits: i64 = eval(&state, "return _G.hits");
assert_eq!(hits, 0, "a subscriber must only fire for its own method");
}
// ---------------------------------------------------------------------------
// Acceptance 30 + 33 — dispatch integrity: with subscribers registered,
// a `workspace/applyEdit` request in the same drain is still handled.
//
// The fake server writes the applyEdit request and the executeCommand
// response back to back, so both land in one `events_take` batch. That
// co-occurrence is the point: a seam that consumed the batch, or that
// returned early, would starve the `request` arms that share it.
// ---------------------------------------------------------------------------
fn drive_apply_edit(state: &mut EditorState, file: &Path) {
exec(
state,
&format!(
r#"
local sid = {THE_SID}
local uri = "file://{}"
_G.rid = pmacs.lsp.send_request(sid, "workspace/executeCommand", {{
command = "pmacs.fake.applyEdit",
arguments = {{ uri }},
}})
_G.response_hits = 0
pmacs.lsp.on_response(sid, _G.rid, function(result, err)
_G.response_hits = _G.response_hits + 1
end)
"#,
lua_str(file)
),
);
settle(state);
}
fn buffer_text(state: &EditorState) -> String {
eval(
state,
"local b = pmacs.window.buffer() return b:slice(0, b:len())",
)
}
#[test]
fn acc30_apply_edit_still_handled_with_a_notification_subscriber() {
let fx = Fixture::new();
let mut state = editor();
exec(
&state,
r#"
_G.notes = 0
pmacs.lsp.on_notification("pmacs/echo", function() _G.notes = _G.notes + 1 end)
"#,
);
let file = attached_rust(&mut state, &fx);
assert!(
eval::<i64>(&state, "return _G.notes") >= 1,
"precondition: the notification subscriber is actually firing"
);
drive_apply_edit(&mut state, &file);
assert!(
buffer_text(&state).contains("ED2"),
"workspace/applyEdit must still be applied with a subscriber \
registered; buffer was {:?}",
buffer_text(&state)
);
}
#[test]
fn acc33_apply_edit_still_handled_with_a_response_subscriber() {
let fx = Fixture::new();
let mut state = editor();
let file = attached_rust(&mut state, &fx);
drive_apply_edit(&mut state, &file);
// Both halves in one drain: the response was delivered to its
// one-shot AND the server-originated request was serviced.
assert_eq!(
eval::<i64>(&state, "return _G.response_hits"),
1,
"the executeCommand response reaches its one-shot"
);
assert!(
buffer_text(&state).contains("ED2"),
"workspace/applyEdit must still be applied with a response \
subscriber registered; buffer was {:?}",
buffer_text(&state)
);
}
// ---------------------------------------------------------------------------
// Acceptance 31 — a raising subscriber does not stop later events in the
// same drain (and does not stop the `request` arms either).
// ---------------------------------------------------------------------------
#[test]
fn acc31_raising_notification_subscriber_does_not_stop_the_drain() {
let fx = Fixture::new();
let mut state = editor();
exec(
&state,
r#"
_G.second_hits = 0
pmacs.lsp.on_notification("pmacs/echo", function()
error("subscriber blew up")
end)
pmacs.lsp.on_notification("pmacs/echo", function()
_G.second_hits = _G.second_hits + 1
end)
"#,
);
let file = attached_rust(&mut state, &fx);
assert!(
eval::<i64>(&state, "return _G.second_hits") >= 1,
"a raising subscriber must not starve the ones after it"
);
// And the shared `request` arms still run in a later drain.
drive_apply_edit(&mut state, &file);
assert!(
buffer_text(&state).contains("ED2"),
"a raising subscriber must not stop workspace/applyEdit"
);
}
#[test]
fn acc33_raising_response_handler_does_not_stop_the_drain() {
let fx = Fixture::new();
let mut state = editor();
let file = attached_rust(&mut state, &fx);
exec(
&state,
&format!(
r#"
local sid = {THE_SID}
_G.notes_after = 0
pmacs.lsp.on_notification("pmacs/echo", function()
_G.notes_after = _G.notes_after + 1
end)
local rid = pmacs.lsp.send_request(sid, "workspace/executeCommand", {{
command = "pmacs.fake.applyEdit",
arguments = {{ "file://{}" }},
}})
pmacs.lsp.on_response(sid, rid, function() error("handler blew up") end)
"#,
lua_str(&file)
),
);
settle(&mut state);
assert!(
buffer_text(&state).contains("ED2"),
"a raising response handler must not stop workspace/applyEdit in \
the same drain"
);
}
// ---------------------------------------------------------------------------
// Acceptance 32 — the one-shot is removed exactly once, whether or not
// the handler raises.
//
// Named for what it pins rather than for the framing's wording. Q#LN9
// specifies removal *before* invocation, and the implementation does
// that — but bite-testing showed the before/after ordering is not
// observable on its own: `pcall` catches the raise either way, so
// removal after the call is behaviorally identical unless a handler
// re-enters the drain, which nothing does. What IS observable, and what
// this pins, is that removal is **unconditional**: the bite that moves
// it inside `if ok then` fails here 2 != 1, because the surviving
// registration gets invoked a second time by the purge.
// ---------------------------------------------------------------------------
#[test]
fn acc32_response_one_shot_is_removed_even_when_the_handler_raises() {
let fx = Fixture::new();
let mut state = editor();
attached_rust(&mut state, &fx);
exec(
&state,
&format!(
r#"
local sid = {THE_SID}
_G.calls = 0
local rid = pmacs.lsp.send_request(sid, "test/ping", {{ v = 1 }})
pmacs.lsp.on_response(sid, rid, function(result, err)
_G.calls = _G.calls + 1
error("handler raises after being removed")
end)
"#
),
);
settle(&mut state);
assert_eq!(
eval::<i64>(&state, "return _G.calls"),
1,
"the one-shot fires exactly once for its reply"
);
exec(&state, &format!("pmacs.lsp.stop({THE_SID})"));
settle(&mut state);
assert_eq!(
eval::<i64>(&state, "return _G.calls"),
1,
"a delivered one-shot must not be re-invoked by the purge — \
removal is unconditional, not gated on a clean return"
);
}
#[test]
fn acc32_response_carries_the_servers_result() {
let fx = Fixture::new();
let mut state = editor();
attached_rust(&mut state, &fx);
exec(
&state,
&format!(
r#"
local sid = {THE_SID}
_G.echoed = nil
_G.saw_err = "unset"
local rid = pmacs.lsp.send_request(sid, "test/ping", {{ v = 42 }})
pmacs.lsp.on_response(sid, rid, function(result, err)
_G.echoed = result and result.echo and result.echo.v
_G.saw_err = tostring(err)
end)
"#
),
);
settle(&mut state);
// Non-vacuity: without this the seam could "fire" with nil payloads
// and every count-based assertion above would still pass.
assert_eq!(
eval::<i64>(&state, "return _G.echoed or -1"),
42,
"the handler receives the server's result payload"
);
assert_eq!(
eval::<String>(&state, "return _G.saw_err"),
"nil",
"a successful reply passes nil for err"
);
}
// ---------------------------------------------------------------------------
// Acceptance 34 — the pending purge, driven off `pmacs.lsp.list()` and
// NOT off a death event seen in the drain.
//
// The second test is the load-bearing one. `handle_server_requests`
// builds its sid list from `attachments`, so a server that is in no
// attachment is never drained — and its `stopped` event is therefore
// never seen. A purge wired to that event leaks exactly there.
// ---------------------------------------------------------------------------
#[test]
fn acc34_purge_settles_a_pending_one_shot_when_the_server_dies() {
let fx = Fixture::new();
let mut state = editor();
attached_rust(&mut state, &fx);
exec(
&state,
&format!(
r#"
local sid = {THE_SID}
_G.err_msg = "never called"
-- A method the fake server answers only after a delay would
-- be ideal; instead the server is stopped in the same breath,
-- so the reply can never arrive.
local rid = pmacs.lsp.send_request(sid, "test/slow", {{}})
pmacs.lsp.on_response(sid, rid, function(result, err)
_G.err_msg = tostring(err and err.message)
end)
pmacs.lsp.stop(sid)
"#
),
);
settle(&mut state);
let msg: String = eval(&state, "return _G.err_msg");
assert!(
msg.contains("server gone") || msg == "nil",
"a pending one-shot must be settled, not left waiting; saw {msg:?}"
);
assert_ne!(
msg, "never called",
"the one-shot was never settled — it leaked"
);
}
#[test]
fn acc34_purge_reaches_a_server_that_is_in_no_attachment() {
let fx = Fixture::new();
let mut state = editor();
fx.bind(&state);
// Spawned directly, never attached to a buffer. `attachments` is
// empty, so `handle_server_requests` never visits this sid and its
// `stopped` event is never drained.
exec(
&state,
&format!(
r#"
_G.settled = "never called"
local sid = pmacs.lsp.spawn({{
label = "orphan",
language_id = "rust",
command = "{}",
args = {{}},
}})
_G.orphan = sid
"#,
fake_lsp_path()
),
);
settle(&mut state);
exec(
&state,
r#"
local rid = pmacs.lsp.send_request(_G.orphan, "test/slow", {})
pmacs.lsp.on_response(_G.orphan, rid, function(result, err)
_G.settled = tostring(err and err.message)
end)
pmacs.lsp.stop(_G.orphan)
"#,
);
settle(&mut state);
let settled: String = eval(&state, "return _G.settled");
assert_ne!(
settled, "never called",
"the purge must not depend on the drain reaching this server — \
it is in no attachment, so the drain never does"
);
assert!(
settled.contains("server gone"),
"settled with the purge's error; saw {settled:?}"
);
}
// ---------------------------------------------------------------------------
// Acceptance 34a — `pmacs.fs.canonicalize` (Q#LN20).
// ---------------------------------------------------------------------------
#[test]
#[cfg(unix)]
fn acc34a_canonicalize_resolves_symlinks_and_dot_segments() {
let fx = Fixture::new();
fx.write("pkg/sub/a.txt", "x\n");
// Built here rather than assumed: the whole point is the symlink.
std::os::unix::fs::symlink(fx.dir("pkg"), fx.dir("linkpkg")).unwrap();
let state = editor();
let noncanon = format!("{}/sub/./../sub/a.txt", fx.dir("linkpkg").display());
let got: String = eval(
&state,
&format!("return tostring(pmacs.fs.canonicalize(\"{noncanon}\"))"),
);
let want = fx.root.join("pkg/sub/a.txt").display().to_string();
assert_eq!(got, want, "symlink and dot segments both resolved");
// Falsification for 34b: the uncanonicalized spelling really is
// different, so the affinity test below is not vacuous.
assert_ne!(noncanon, want);
}
#[test]
fn acc34a_canonicalize_returns_nil_for_a_missing_path() {
let fx = Fixture::new();
let state = editor();
let missing = fx.dir("nope/not-here").display().to_string();
let got: String = eval(
&state,
&format!("return tostring(pmacs.fs.canonicalize(\"{missing}\"))"),
);
assert_eq!(
got, "nil",
"a nonexistent path declines rather than raising"
);
}
// ---------------------------------------------------------------------------
// Acceptance 34b — affinity survives a symlinked open.
//
// Asserted at the affinity layer, not just at the binding: the
// regression Q#LN20 exists to prevent is *two servers for one project*,
// and only this shape observes it.
// ---------------------------------------------------------------------------
fn server_count(state: &EditorState) -> i64 {
eval(state, "return #pmacs.lsp.list()")
}
#[test]
#[cfg(unix)]
fn acc34b_canonicalizing_resolver_reuses_one_server_across_a_symlink() {
let fx = Fixture::new();
fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n");
let real = fx.write("proj/src/main.rs", "fn main() {}\n");
std::os::unix::fs::symlink(fx.dir("proj"), fx.dir("linkproj")).unwrap();
let linked = fx.dir("linkproj").join("src/main.rs");
let mut state = editor();
fx.bind(&state);
exec(
&state,
&format!(
r#"
pmacs.lsp.config.rust = {{
command = "{}",
root = function(path)
local dir = path:match("^(.*)/[^/]*$")
if not dir then return nil end
-- Walk up to the directory holding Cargo.toml, then
-- canonicalize — the Q#LN8 shape Stage 3b will use.
while dir and #dir > 0 do
local f = io.open(dir .. "/Cargo.toml", "r")
if f then
f:close()
return pmacs.fs.canonicalize(dir)
end
dir = dir:match("^(.*)/[^/]*$")
end
return nil
end,
}}
"#,
fake_lsp_path()
),
);
open(&state, &real);
settle(&mut state);
assert_eq!(server_count(&state), 1, "the real path spawns one server");
open(&state, &linked);
settle(&mut state);
assert_eq!(
server_count(&state),
1,
"the symlinked path must reuse the same server — two here is the \
exact regression Q#LN20 exists to prevent"
);
}
#[test]
#[cfg(unix)]
fn acc34b_falsified_by_a_resolver_that_skips_canonicalization() {
let fx = Fixture::new();
fx.write("proj/Cargo.toml", "[package]\nname = \"p\"\n");
let real = fx.write("proj/src/main.rs", "fn main() {}\n");
std::os::unix::fs::symlink(fx.dir("proj"), fx.dir("linkproj")).unwrap();
let linked = fx.dir("linkproj").join("src/main.rs");
let mut state = editor();
fx.bind(&state);
// Same resolver, minus the canonicalize call. This is the bite: if
// it also produced one server, the test above would be vacuous and
// `pmacs.fs.canonicalize` would be doing nothing.
exec(
&state,
&format!(
r#"
pmacs.lsp.config.rust = {{
command = "{}",
root = function(path)
local dir = path:match("^(.*)/[^/]*$")
while dir and #dir > 0 do
local f = io.open(dir .. "/Cargo.toml", "r")
if f then f:close() return dir end
dir = dir:match("^(.*)/[^/]*$")
end
return nil
end,
}}
"#,
fake_lsp_path()
),
);
open(&state, &real);
settle(&mut state);
open(&state, &linked);
settle(&mut state);
assert_eq!(
server_count(&state),
2,
"without canonicalization the two spellings key differently and \
spawn two servers — this is what 34b's positive case rules out"
);
}
// ---------------------------------------------------------------------------
// Acceptance 34a, non-UTF-8 arm — an unrepresentable resolution declines
// rather than returning a lossy string.
//
// Review finding on PR #167: `display().to_string()` substitutes U+FFFD,
// which would hand back a path that does not exist on disk. That is
// strictly worse than nil here, because the value becomes a
// server-affinity key via `file_uri_for` and would silently fail to
// round-trip. Bites against the `display()` form, which returns a
// non-nil string for this fixture.
//
// **Linux-gated, and `cfg(unix)` was not enough** — CI caught that.
// APFS enforces valid UTF-8 in filenames, so on macOS the `write` below
// fails with EILSEQ ("Illegal byte sequence") before the code under test
// is ever reached: the fixture cannot be built there. That is a
// filesystem refusing to represent the case, not a behavioral
// difference — the subject itself, `to_str()` returning None, is
// platform-independent Rust. Gated explicitly rather than skipped at
// runtime, so a future failure here is a real failure and not a silent
// no-op.
// ---------------------------------------------------------------------------
#[test]
#[cfg(target_os = "linux")]
fn acc34a_canonicalize_declines_a_non_utf8_resolution() {
use std::ffi::OsStr;
use std::os::unix::ffi::OsStrExt as _;
let fx = Fixture::new();
// 0xFF is not valid UTF-8 in any position.
let raw = OsStr::from_bytes(b"bad-\xffname");
let target = fx.root.join(raw);
std::fs::write(&target, "x\n").unwrap();
// Reached through an ASCII symlink, so the *input* is representable
// and only the resolved output is not — which is the case
// `to_str()` has to catch and a UTF-8-only input check would miss.
let link = fx.dir("ascii-link");
std::os::unix::fs::symlink(&target, &link).unwrap();
let state = editor();
let got: String = eval(
&state,
&format!(
"return tostring(pmacs.fs.canonicalize(\"{}\"))",
lua_str(&link)
),
);
assert_eq!(
got, "nil",
"a resolution that lands on non-UTF-8 bytes must decline, not \
return a U+FFFD-substituted path that exists nowhere"
);
}

746
tests/terminal_config_acceptance.rs Normal file
View File

@ -0,0 +1,746 @@
//! Terminal configuration acceptance (Stage 1 of
//! `docs/terminal-config-and-copy-mode-framing.md`, criteria 1-12).
//!
//! Deliberately NOT `#[cfg(feature = "crdt")]`: CI never enables that
//! feature, so a gated suite is written and then never run.
use std::thread;
use std::time::{Duration, Instant};
use crossterm::event::{KeyCode, KeyEvent, KeyModifiers};
use mlua::Value;
use pmacs::cell::{CellSize, Glyph};
use pmacs::editor::EditorState;
use pmacs::protocol::FrontendId;
use pmacs::terminal::TerminalViewKey;
use pmacs::window::WindowId;
fn exec(state: &EditorState, src: &str) {
state
.lua_host
.lua()
.load(src)
.exec()
.unwrap_or_else(|e| panic!("lua failed: {src}\n{e}"));
}
fn eval_err(state: &EditorState, src: &str) -> String {
let result: mlua::Result<Value> = state.lua_host.lua().load(src).eval();
match result {
Ok(_) => panic!("expected an error from: {src}"),
Err(e) => e.to_string(),
}
}
/// The viewport every test projects through. Deliberately SHORTER than
/// the 24-row screen a terminal opens with, so "scroll to the oldest
/// retained row" has somewhere to go even when nothing is retained —
/// which is what makes the two scrollback arms differ by content rather
/// than by whether scrolling was possible at all.
fn viewport() -> CellSize {
CellSize::new(10, 40)
}
fn cells_to_text(cells: &[pmacs::cell::Cell]) -> String {
let mut text = String::new();
for cell in cells {
match &cell.glyph {
Glyph::Char(c) => text.push(*c),
Glyph::Cluster(b) => text.push_str(&String::from_utf8_lossy(b)),
Glyph::Continuation => {}
}
}
text
}
fn screen_text(state: &EditorState, buffer: pmacs::buffer::BufferId) -> String {
let manager = state.terminal_manager.borrow();
let Some(snapshot) = manager.snapshot(buffer) else {
return String::new();
};
cells_to_text(&snapshot.cells)
}
/// Text a view actually shows, which is where retained history is
/// visible at all — the live `screen_text` above always reads the tail.
fn view_text(state: &EditorState, key: TerminalViewKey) -> String {
let mut manager = state.terminal_manager.borrow_mut();
manager
.snapshot_for_view(key, viewport())
.map(|snapshot| cells_to_text(&snapshot.cells))
.unwrap_or_default()
}
/// Scroll a view to its OLDEST retained row and read it back.
fn oldest_view_text(state: &EditorState, key: TerminalViewKey) -> String {
state
.terminal_manager
.borrow_mut()
.scroll_view(key, viewport(), i32::MAX);
view_text(state, key)
}
fn tick_until(state: &mut EditorState, needle: &str, buffer: pmacs::buffer::BufferId) -> bool {
let deadline = Instant::now() + Duration::from_secs(5);
loop {
state.tick_processes();
if screen_text(state, buffer).contains(needle) {
return true;
}
if Instant::now() >= deadline {
return false;
}
thread::sleep(Duration::from_millis(20));
}
}
/// Give LOCAL a window on `buffer` and register/claim its terminal view,
/// which is what makes `dispatch_key`'s terminal arm reachable.
fn focus_terminal(state: &EditorState, buffer: pmacs::buffer::BufferId) -> WindowId {
state.core.borrow_mut().switch_active_buffer(buffer).ok();
let window = state.core.borrow().active_window_id();
let key = TerminalViewKey::new(FrontendId::LOCAL, window, buffer);
let mut manager = state.terminal_manager.borrow_mut();
manager.register_view(key);
manager.claim_controller(key);
let _ = manager.snapshot_for_view(key, viewport());
window
}
fn terminal_buffers(state: &EditorState) -> Vec<pmacs::buffer::BufferId> {
let manager = state.terminal_manager.borrow();
state
.core
.borrow()
.registry
.borrow()
.ids()
.iter()
.copied()
.filter(|id| manager.is_terminal(*id))
.collect()
}
/// Open a terminal from Lua and return the identity buffer it created.
///
/// The id is derived by diffing the manager's terminal set rather than
/// returned through Lua: `BufferIdLua` exposes no id accessor, and
/// diffing also asserts in passing that exactly one terminal appeared.
fn open_cat_terminal(state: &EditorState, lua_spec: &str) -> pmacs::buffer::BufferId {
let before = terminal_buffers(state);
exec(
state,
&format!("TERM_BUF = pmacs.terminal.open {{ {lua_spec} }}"),
);
let after = terminal_buffers(state);
let mut fresh: Vec<_> = after
.into_iter()
.filter(|id| !before.contains(id))
.collect();
assert_eq!(fresh.len(), 1, "exactly one terminal must have opened");
fresh.remove(0)
}
/// `cat -v` is the echo instrument, deliberately: the terminal screen
/// rejects C0/C1 controls before they enter cells (Vterm Stage 1
/// criterion 2), so a raw echoed `Ctrl-X` would be invisible and a test
/// probing for it could never pass. `-v` renders it as the printable
/// two-character `^X`, which is what makes "the configured chord reached
/// the child" observable at all.
const CAT_PROFILE: &str = r#"
pmacs.terminal.profiles.echo = {
command = "/bin/sh",
args = { "-c", "printf 'READY\r\n'; exec cat -v" },
}
"#;
/// Did the last key ARM the terminal escape?
///
/// Observed behaviorally rather than through an accessor: while the
/// escape is armed the next key goes to ordinary dispatch, so it never
/// reaches the child. `cat` echoes anything that does reach it, which
/// makes "the probe character did not appear" the exact observable for
/// "that chord was consumed as the escape".
fn escape_was_armed(state: &mut EditorState, buffer: pmacs::buffer::BufferId, probe: char) -> bool {
// Count occurrences rather than testing for presence: the screen
// already holds the child's own output, and a single-character probe
// like 'R' collides with the "READY" banner. Only an INCREASE proves
// this keystroke reached the child.
let before = screen_text(state, buffer).matches(probe).count();
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char(probe), KeyModifiers::NONE),
);
let deadline = Instant::now() + Duration::from_secs(2);
loop {
state.tick_processes();
if screen_text(state, buffer).matches(probe).count() > before {
return false;
}
if Instant::now() >= deadline {
return true;
}
thread::sleep(Duration::from_millis(20));
}
}
/// Acceptance 1: a profile spec is strict, and rejects before anything spawns.
#[test]
fn acc1_profile_specs_are_strict_and_reject_before_spawning() {
let state = EditorState::new();
let before = state.core.borrow().registry.borrow().ids().len();
exec(
&state,
r#"pmacs.terminal.profiles.bad = { command = "/bin/sh", nonsense = true }"#,
);
let err = eval_err(&state, r#"return pmacs.terminal.open { profile = "bad" }"#);
assert!(
err.contains("unknown field") && err.contains("nonsense"),
"the error must name the offending field: {err}"
);
exec(&state, "pmacs.terminal.profiles.wrong = { command = 42 }");
let err = eval_err(
&state,
r#"return pmacs.terminal.open { profile = "wrong" }"#,
);
assert!(err.contains("must be a string"), "typed field error: {err}");
assert_eq!(
state.core.borrow().registry.borrow().ids().len(),
before,
"a rejected profile must create no buffer"
);
assert_eq!(state.terminal_manager.borrow().len(), 0);
}
/// Acceptance 2: an unknown profile names the known ones and creates nothing.
#[test]
fn acc2_unknown_profile_lists_known_names_and_creates_nothing() {
let state = EditorState::new();
exec(&state, CAT_PROFILE);
exec(
&state,
r#"pmacs.terminal.profiles.other = { command = "/bin/sh" }"#,
);
let before = state.core.borrow().registry.borrow().ids().len();
// Via the default setting.
exec(
&state,
r#"pmacs.config.set("terminal.default-profile", "ghost")"#,
);
let err = eval_err(&state, "return pmacs.terminal.open {}");
assert!(err.contains("ghost"), "names the missing profile: {err}");
assert!(
err.contains("echo") && err.contains("other"),
"must LIST the known profiles: {err}"
);
// An explicit bad profile fails even though the default is now valid —
// a typo must not silently fall back (Q#TC3a).
exec(
&state,
r#"pmacs.config.set("terminal.default-profile", "echo")"#,
);
let err = eval_err(&state, r#"return pmacs.terminal.open { profile = "typo" }"#);
assert!(err.contains("typo"), "explicit bad profile errors: {err}");
assert_eq!(
state.core.borrow().registry.borrow().ids().len(),
before,
"no buffer, session, or process is created"
);
assert_eq!(state.terminal_manager.borrow().len(), 0);
}
/// Acceptance 2 (malformed table): `pmacs.terminal.profiles` is a raw
/// user table, so a diagnostic that walks its keys must be total over
/// them. A table holding both a string and a numeric key made
/// `table.sort` raise "attempt to compare number with string" — on the
/// unknown-profile path, replacing the exact error being asked for.
#[test]
fn acc2_malformed_profile_keys_do_not_mask_the_unknown_profile_error() {
let state = EditorState::new();
exec(&state, CAT_PROFILE);
exec(
&state,
r#"pmacs.terminal.profiles[1] = { command = "/bin/sh" }"#,
);
let err = eval_err(
&state,
r#"return pmacs.terminal.open { profile = "ghost" }"#,
);
assert!(
err.contains("ghost") && err.contains("echo"),
"the unknown-profile error must survive a malformed table: {err}"
);
assert!(
!err.contains("attempt to compare"),
"listing known profiles must not raise: {err}"
);
// Rendering the REQUESTED name is partial too: `%q` raises on a
// table, and the name arrives straight from the caller.
let err = eval_err(&state, r"return pmacs.terminal.open { profile = {} }");
assert!(
err.contains("is not defined") && err.contains("known profiles"),
"a non-string profile name must render, not raise: {err}"
);
assert_eq!(state.terminal_manager.borrow().len(), 0);
}
/// Acceptance 3: explicit beats profile beats setting beats `$SHELL`, and
/// `env` MERGES rather than replacing.
#[test]
fn acc3_field_resolution_order_and_env_merge() {
let mut state = EditorState::new();
exec(
&state,
r#"
pmacs.terminal.profiles.merged = {
command = "/bin/sh",
args = { "-c", "printf 'PROFILE:%s:%s\r\n' \"$FROM_PROFILE\" \"$SHARED\"; exec cat" },
env = { FROM_PROFILE = "p", SHARED = "profile" },
}
"#,
);
let buffer = open_cat_terminal(
&state,
r#"profile = "merged", env = { SHARED = "explicit" }"#,
);
assert!(
tick_until(&mut state, "PROFILE:p:explicit", buffer),
"profile env survives and explicit env overrides the same key: {:?}",
screen_text(&state, buffer)
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 3 (explicit command wins) and 4 (`""` means no profile).
#[test]
fn acc3_acc4_explicit_command_wins_and_empty_default_means_no_profile() {
let mut state = EditorState::new();
exec(&state, CAT_PROFILE);
exec(
&state,
r#"pmacs.config.set("terminal.default-profile", "echo")"#,
);
// Explicit command beats the profile's.
let explicit = open_cat_terminal(
&state,
r#"command = "/bin/sh", args = { "-c", "printf 'EXPLICIT\r\n'; exec cat" }"#,
);
assert!(tick_until(&mut state, "EXPLICIT", explicit));
// `""` is the no-profile sentinel: falls through to $SHELL.
exec(
&state,
r#"pmacs.config.set("terminal.default-profile", "")"#,
);
let bare = open_cat_terminal(&state, "");
let spec_ok = state.terminal_manager.borrow().is_terminal(bare);
assert!(spec_ok, "an empty default must open a $SHELL terminal");
assert!(
!screen_text(&state, bare).contains("READY"),
"the echo profile must NOT have been applied"
);
state.process_supervisor.borrow_mut().shutdown();
}
/// A child that overflows the 24-row screen and then goes quiet, so its
/// early output can only still be found in RETAINED HISTORY. Zero-padded
/// so `LINE001` is not a substring of `LINE100`.
const FILL_PROFILE: &str = r#"
pmacs.terminal.profiles.fill = {
command = "/bin/sh",
args = { "-c",
"i=1; while [ $i -le 200 ]; do printf 'LINE%03d\r\n' $i; i=$((i+1)); done; printf 'DONE\r\n'; exec cat" },
}
"#;
/// Acceptance 5: the scrollback SETTING reaches the screen's retained
/// history, an explicit spec value overrides it, and `0` is legal.
///
/// Asserted end to end, through a real child and a real view, rather
/// than by reading the value back out of the registry: a registry
/// round-trip is a test of the registry, and would stay green with the
/// setting's only consumer (`terminal.lua`'s `resolved.scrollback_rows`
/// fallback) deleted outright.
#[test]
fn acc5_scrollback_setting_reaches_retained_history() {
let mut state = EditorState::new();
exec(&state, FILL_PROFILE);
// Arm 1: `0` is legal, and means the early rows are GONE.
exec(&state, r#"pmacs.config.set("terminal.scrollback-rows", 0)"#);
let none = open_cat_terminal(&state, r#"profile = "fill""#);
assert!(tick_until(&mut state, "DONE", none), "child finished");
let window = focus_terminal(&state, none);
let none_key = TerminalViewKey::new(FrontendId::LOCAL, window, none);
let oldest = oldest_view_text(&state, none_key);
assert!(
!oldest.contains("LINE001"),
"with scrollback 0 the oldest retained row must not be the \
child's first line: {oldest:?}"
);
// Arm 2: a large setting retains it, reachable by scrolling back.
exec(
&state,
r#"pmacs.config.set("terminal.scrollback-rows", 10000)"#,
);
let kept = open_cat_terminal(&state, r#"profile = "fill""#);
assert!(tick_until(&mut state, "DONE", kept), "child finished");
let window = focus_terminal(&state, kept);
let kept_key = TerminalViewKey::new(FrontendId::LOCAL, window, kept);
let oldest = oldest_view_text(&state, kept_key);
assert!(
oldest.contains("LINE001"),
"with scrollback 10000 the first line must survive in history: \
{oldest:?}"
);
// Arm 3: an explicit spec value beats the setting, which is still 10000.
let overridden = open_cat_terminal(&state, r#"profile = "fill", scrollback_rows = 0"#);
assert!(tick_until(&mut state, "DONE", overridden), "child finished");
let window = focus_terminal(&state, overridden);
let overridden_key = TerminalViewKey::new(FrontendId::LOCAL, window, overridden);
let oldest = oldest_view_text(&state, overridden_key);
assert!(
!oldest.contains("LINE001"),
"an explicit scrollback_rows = 0 must beat the setting: {oldest:?}"
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 5 (bounds): the registered range rejects out-of-range
/// values, and `0` is inside it rather than a disabled sentinel.
#[test]
fn acc5_scrollback_bounds() {
let state = EditorState::new();
exec(&state, r#"pmacs.config.set("terminal.scrollback-rows", 0)"#);
assert_eq!(
state
.lua_host
.lua()
.load(r#"return pmacs.config.get("terminal.scrollback-rows")"#)
.eval::<i64>()
.unwrap(),
0,
"0 is a legal scrollback value meaning 'retain no history'"
);
let err = eval_err(
&state,
r#"return pmacs.config.set("terminal.scrollback-rows", -1)"#,
);
assert!(
err.contains("-1") || err.contains("min"),
"below range: {err}"
);
let err = eval_err(
&state,
r#"return pmacs.config.set("terminal.scrollback-rows", 4000001)"#,
);
assert!(
err.contains("4000001") || err.contains("max"),
"above range: {err}"
);
}
/// Acceptance 6 and 9: the configured chord escapes, repeating it sends
/// THAT chord to the child, and an ordinary `C-c` still reaches the child.
#[test]
fn acc6_acc9_configured_escape_chord_and_literal_repeat() {
let mut state = EditorState::new();
exec(&state, CAT_PROFILE);
let buffer = open_cat_terminal(&state, r#"profile = "echo""#);
assert!(tick_until(&mut state, "READY", buffer));
focus_terminal(&state, buffer);
exec(&state, r#"pmacs.config.set("terminal.escape-key", "C-x")"#);
// `C-x C-x` must send Ctrl-X (0x18), which `cat` echoes back. Against
// the pre-change hardcoded `&[0x03]` this sends Ctrl-C instead.
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('x'), KeyModifiers::CONTROL),
);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('x'), KeyModifiers::CONTROL),
);
assert!(
tick_until(&mut state, "^X", buffer),
"C-x C-x must send literal Ctrl-X: {:?}",
screen_text(&state, buffer)
);
// With the escape moved, an ordinary C-c is just another key.
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('c'), KeyModifiers::CONTROL),
);
assert!(
tick_until(&mut state, "^C", buffer),
"plain C-c must reach the child once the escape moved: {:?}",
screen_text(&state, buffer)
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 7, 8 and 8a: per-terminal escape resolution, an A→B→A parse
/// count that does not grow, and a cache that dies with its terminal.
#[test]
fn acc7_acc8_acc8a_per_terminal_escape_cache_identity_and_lifecycle() {
let mut state = EditorState::new();
exec(&state, CAT_PROFILE);
let a = open_cat_terminal(&state, r#"profile = "echo""#);
exec(&state, "TERM_A = TERM_BUF");
let b = open_cat_terminal(&state, r#"profile = "echo""#);
exec(&state, "TERM_B = TERM_BUF");
assert!(tick_until(&mut state, "READY", a));
assert!(tick_until(&mut state, "READY", b));
// Different buffer-local escapes, then NO further writes.
exec(
&state,
r#"pmacs.config.set_local(TERM_A, "terminal.escape-key", "C-x")"#,
);
exec(
&state,
r#"pmacs.config.set_local(TERM_B, "terminal.escape-key", "C-b")"#,
);
// Prime both caches. Each priming press ARMS the escape, so it is
// consumed with a probe — otherwise the next chord would be read as
// the escape repeat rather than a fresh escape.
focus_terminal(&state, a);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('x'), KeyModifiers::CONTROL),
);
assert!(escape_was_armed(&mut state, a, 'M'), "A primes on its C-x");
focus_terminal(&state, b);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('b'), KeyModifiers::CONTROL),
);
assert!(escape_was_armed(&mut state, b, 'N'), "B primes on its C-b");
let primed = state.terminal_manager.borrow().escape_parses();
assert_eq!(
state.terminal_manager.borrow().escape_caches(),
2,
"each primed terminal holds its own cache"
);
// Acceptance 7 — BOTH directions. Asserting only that A still works
// after A->B->A is not enough: an epoch-only cache hands whichever
// entry it finds to every terminal, so A keeps working by accident
// while B silently inherits A's chord. The discriminating assertion
// is that EACH terminal honors its OWN chord and NOT the other's.
focus_terminal(&state, b);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('b'), KeyModifiers::CONTROL),
);
assert!(
escape_was_armed(&mut state, b, 'R'),
"terminal B must escape on its own C-b"
);
// ...and A's chord must be ordinary input in B, not an escape.
focus_terminal(&state, b);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('x'), KeyModifiers::CONTROL),
);
assert!(
!escape_was_armed(&mut state, b, 'S'),
"terminal A's C-x must NOT escape terminal B"
);
focus_terminal(&state, a);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('x'), KeyModifiers::CONTROL),
);
assert!(
escape_was_armed(&mut state, a, 'Q'),
"terminal A must still escape on its own C-x after A->B->A"
);
// Acceptance 8: that round trip parsed nothing new. A single
// last-entry cache would have reparsed twice.
assert_eq!(
state.terminal_manager.borrow().escape_parses(),
primed,
"A->B->A with no setting written must not reparse"
);
// Acceptance 8a: the cache dies with its terminal.
//
// Waiting for the SESSION count to fall is not the assertion — a
// session set that drains while an editor-side `HashMap<BufferId,
// EscapeCache>` keeps its entry (the rejected implementation named
// in Q#TC4c, which has no purge hook) satisfies it exactly. The
// discriminating observable is the CACHE count, which such a map
// would hold at its high-water mark of 2.
let sessions_before = state.terminal_manager.borrow().len();
exec(&state, "pmacs.terminal.terminate(TERM_A)");
exec(&state, "pmacs.buffer.kill(TERM_A)");
// Pruning is tick-driven (the manager reaps on the process tick), so
// the session outlives the kill call by design.
let deadline = Instant::now() + Duration::from_secs(5);
while state.terminal_manager.borrow().len() >= sessions_before {
state.tick_processes();
assert!(
Instant::now() < deadline,
"killing the terminal must remove its session"
);
thread::sleep(Duration::from_millis(20));
}
assert_eq!(
state.terminal_manager.borrow().escape_caches(),
1,
"killing terminal A must drop ITS cache, not merely its session"
);
// ...and the surviving cache is B's, so the right one was dropped.
focus_terminal(&state, b);
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('b'), KeyModifiers::CONTROL),
);
assert!(
escape_was_armed(&mut state, b, 'T'),
"terminal B must still escape on its own C-b after A was killed"
);
assert_eq!(
state.terminal_manager.borrow().escape_parses(),
primed,
"B's surviving cache must not have been reparsed"
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 10 and 10a: an unparseable value falls back, reports through
/// the status line, and reports once per terminal per effective bad value.
#[test]
fn acc10_acc10a_invalid_escape_falls_back_and_reports_once() {
let mut state = EditorState::new();
exec(&state, CAT_PROFILE);
let buffer = open_cat_terminal(&state, r#"profile = "echo""#);
assert!(tick_until(&mut state, "READY", buffer));
focus_terminal(&state, buffer);
exec(
&state,
r#"pmacs.config.set("terminal.escape-key", "not-a-chord")"#,
);
state.core.borrow_mut().status.clear();
// Acceptance 10: falls back to C-c, so the terminal stays escapable.
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('c'), KeyModifiers::CONTROL),
);
// Read the report BEFORE probing: `status` is a single slot, and the
// probe key's own rejected self-insert would overwrite it.
let reported = state.core.borrow().status.clone();
assert!(
reported.contains("terminal.escape-key") && reported.contains("not-a-chord"),
"the report must name the setting and the bad value: {reported:?}"
);
assert!(
escape_was_armed(&mut state, buffer, 'Q'),
"an invalid escape-key must fall back to C-c, not leave the \
terminal unescapable"
);
// Acceptance 10a: the same bad value does not report again.
state.core.borrow_mut().status.clear();
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('c'), KeyModifiers::CONTROL),
);
assert!(
state.core.borrow().status.is_empty(),
"an unchanged invalid value must not re-report: {:?}",
state.core.borrow().status
);
let _ = escape_was_armed(&mut state, buffer, 'W');
// A DIFFERENT bad value is new information, so it reports again.
exec(
&state,
r#"pmacs.config.set("terminal.escape-key", "also-bad")"#,
);
state.core.borrow_mut().status.clear();
state.dispatch_key(
FrontendId::LOCAL,
KeyEvent::new(KeyCode::Char('c'), KeyModifiers::CONTROL),
);
assert!(
state.core.borrow().status.contains("also-bad"),
"a different invalid value must report: {:?}",
state.core.borrow().status
);
state.process_supervisor.borrow_mut().shutdown();
}
/// Acceptance 11: the opening binding exists, resolves to the command, and
/// shadowed nothing (`keymap.bind` is strict, so loading the runtime at all
/// proves the second half).
#[test]
fn acc11_terminal_opening_binding_is_bound_and_shadowed_nothing() {
let state = EditorState::new();
let command: Option<String> = state
.lua_host
.lua()
.load(r#"local d = pmacs.describe.key("C-c t"); return d and d.command"#)
.eval()
.expect("describe.key");
assert_eq!(
command.as_deref(),
Some("terminal"),
"C-c t must open a terminal"
);
}
/// Acceptance 12: with no settings written and no profiles registered, the
/// defaults reproduce the pre-arc behavior.
#[test]
fn acc12_defaults_reproduce_prior_behavior() {
let state = EditorState::new();
let lua = state.lua_host.lua();
assert_eq!(
lua.load(r#"return pmacs.config.get("terminal.default-profile")"#)
.eval::<String>()
.unwrap(),
""
);
assert_eq!(
lua.load(r#"return pmacs.config.get("terminal.scrollback-rows")"#)
.eval::<i64>()
.unwrap(),
10_000
);
assert_eq!(
lua.load(r#"return pmacs.config.get("terminal.escape-key")"#)
.eval::<String>()
.unwrap(),
"C-c"
);
assert!(
lua.load("return next(pmacs.terminal.profiles) == nil")
.eval::<bool>()
.unwrap(),
"no profiles are registered by default"
);
}

735
tests/typed_edit_chain_acceptance.rs Normal file
View File

@ -0,0 +1,735 @@
//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a,
//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46h).
//!
//! The chain owns the single `buffer.after-edit` subscriber that reads
//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in
//! priority order. These tests pin the chain's OWN behavior — take-once,
//! priority ordering, claim-stops-chain, throw containment, per-consumer
//! record isolation, snapshot iteration under re-entrant registration,
//! the registration lifecycle, and the Q#AP7 flush ordering it inherited
//! from `pair.lua`.
//!
//! They deliberately do not re-test auto-pairing: criterion 46 requires
//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that
//! suite is the no-behavior-change pin. Pairing appears here only as
//! the chain's last consumer, which is how 46c observes that a claim
//! really stopped the chain.
//!
//! Dispatch-driven throughout: `dispatch_key` is the producer that arms
//! the record for a grid frontend.
use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers};
use pmacs::editor::EditorState;
use pmacs::lua_bindings::StateDir;
use pmacs::protocol::FrontendId;
use std::path::PathBuf;
use std::sync::atomic::{AtomicUsize, Ordering};
use std::time::{Duration, Instant};
fn fresh_state_dir() -> PathBuf {
static SEQ: AtomicUsize = AtomicUsize::new(0);
let dir = std::env::temp_dir().join(format!(
"pmacs-typededit-{}-{}",
std::process::id(),
SEQ.fetch_add(1, Ordering::Relaxed)
));
std::fs::create_dir_all(&dir).unwrap();
dir
}
fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent {
KeyEvent {
code,
modifiers: mods,
kind: KeyEventKind::Press,
state: KeyEventState::NONE,
}
}
fn type_str(s: &mut EditorState, text: &str) {
for ch in text.chars() {
s.dispatch_key(
FrontendId::LOCAL,
key(KeyCode::Char(ch), KeyModifiers::NONE),
);
}
}
fn exec(s: &EditorState, src: &str) {
s.lua_host.lua().load(src.to_string()).exec().unwrap();
}
fn eval<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)"
);
}