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

Merge canonical main into bottom-panel Stage 2B-1 

Integrate the Journey Stage 1a merge without rewriting the already
reviewed protocol branch. Record the approved three-way Stage 2B split,
advance the canonical recovery anchor, remove the landed Journey lane,
and put 2B-1 into its full-gating state.
This commit is contained in:
Levi Neuwirth 2026-07-27 22:16:11 -04:00
parent 56301eda02 c2d56ff48b
commit d88d60eba6
21 changed files with 8045 additions and 652 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

117
COHERENCE.md
View File

@ -95,7 +95,7 @@ remain open to them.
| § | Concern | Grade | One-line state |
|---|---|---|---|
| 2 | Golden product journey | **Broken at entry** | `pmacs .` exits 1; only "launch" and "edit" pass cleanly zero-config |
| 2 | Golden product journey | **Runs to step 5** | `pmacs .` opens the directory (Journey Stage 1a); thin from step 6 on |
| 3 | Zero-configuration state | **Partial** | Defaults genuinely strong; missing-tool failure is silent, not graceful |
| 4 | Progressive disclosure | **Inverted** | The advanced level is real; the beginner level is the missing one |
| 5 | Unified discoverability | **Substrate without surface** | Best-in-class registration metadata; almost no way for a user to reach it |
@ -112,7 +112,7 @@ remain open to them.
| 16 | Semantic frontend | **Strong** | v6..=v20 negotiated protocol; degradation practiced; TUI/GPU share the model |
| 17 | Distribution | **Missing** | CI is test-only; no binaries, channels, checksums, or update path |
| 18 | Onboarding | **Missing** | No welcome, no tutorial; `C-h` deletes a word; `M-x` is the only door in |
| 19 | Coherence acceptance tests | **Missing (culture ready)** | Superb per-arc acceptance discipline; zero cross-subsystem journey tests |
| 19 | Coherence acceptance tests | **Started** | `tests/journey_acceptance.rs` exists (steps 2, 3, 5); the other five scenarios are still unwritten |
Three cross-cutting patterns explain most of the table; they are
detailed in §1.1–§1.3: **substrate without surface**, **the silence
@ -339,7 +339,8 @@ the journey.
### Ground truth: the journey today
**Grade: broken at step 3.** Verified empirically at audit time:
**Grade: reaches step 5; thin from step 6 on.** Was **broken at step 3**
at audit time:
```
$ ./target/release/pmacs .
@ -347,15 +348,23 @@ pmacs: Is a directory (os error 21)
EXIT=1
```
The literal first arrow of the diagram above fails. `load_file`
The literal first arrow of the diagram above failed. `load_file`
(`src/file_io.rs:81-87`) does `File::open` (succeeds on a directory)
then `read_to_end` → EISDIR, which is not `NotFound`, so
`EditorState::open` returns `Err` and `main` prints and exits
(`src/main.rs:411-414`). Multiple file arguments are also rejected
(`"multiple files not yet supported"`, `src/main.rs:227`). Everything
from step 6 onward is gated on a file being open, and the only
zero-config way to open one is naming it on the command line — which
requires already knowing the path.
`EditorState::open` returned `Err` and `main` printed and exited.
**Journey Stage 1a fixed that arrow** (`docs/journey-stage1a-framing.md`).
`resolve_target_buffer` now answers `ResolvedTarget::Directory` *ahead*
of the load, `pmacs .` lists the directory in dired, `RET` visits a
file, and a self-insert lands in it — steps 3 and 5 run end to end,
pinned by `tests/journey_acceptance.rs`. Which surface opens a directory
is a `path.open-directory` chain with dired as a replaceable fallback,
so this did not grow a second directory surface.
Still true: multiple file arguments are rejected (`"multiple files not
yet supported"`, `src/main.rs:227`), and everything from step 6 onward
is gated on a file being open — but the zero-config way to open one is
no longer "already know the path".
Full verdict table:
@ -363,7 +372,7 @@ Full verdict table:
|---|---|---|---|
| 1 | Install | **Partial** | Source build only: `cargo build --release --workspace --features pmacs/crdt` (`README.md`). No binaries, no packaging. Runtime deps (`/bin/sh`, git, tar, coreutils) documented, never checked at runtime |
| 2 | Launch unconfigured | **Works** | `EditorState::new()` → empty `*scratch*`; missing config is not an error (`src/config.rs:7-9`); recentf/saveplace/autosave default-on |
| 3 | Open real project | **Missing at the CLI** | `pmacs .` still exits 1 (above): `load_file` does `File::open` (which succeeds on a directory) then `read_to_end` → EISDIR, which is not `NotFound`, so `resolve_target_buffer`'s create-a-`[new file]` arm never fires. Dired Stage 1 (merged #165) supplies the buffer a directory should resolve *to*; routing `pmacs .` into it is Journey Stage 1's work, which must not invent a second directory surface |
| 3 | Open real project | **Works at the CLI** | Journey Stage 1a: `resolve_target_buffer` answers `ResolvedTarget::Directory` before the EISDIR-producing load, and `EditorState::open` / the daemon bootstrap dispatch the `path.open-directory` chain, whose fallback is dired (#165's buffer, reached rather than duplicated). Startup no longer fails: an unreadable directory, a crashed resolver, and a cleared handler all report on the status line and leave the session running. Because the listing is async and the bootstrap is synchronous, the commit runs against a destination captured at request time (`pmacs.window.commit_to`) rather than against the ambient frontend |
| 4 | Understand interface | **Partial** | Mode line gives name/modified/L:C/scroll + mode/LSP/terminal segments; but no welcome text (`EditorCore::new` sets `status: String::new()`), no cheat sheet, and `C-h` deletes a word (§18) |
| 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 |
@ -1041,12 +1050,15 @@ 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 eight settings**: `editing.auto-pair` (pair.lua),
- **Adoption is nine 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), and `terminal.default-profile` +
(window.lua), `terminal.default-profile` +
`terminal.scrollback-rows` + `terminal.escape-key` (terminal.lua,
#173). Everything else a user might set — theme, fonts, LSP
#173), and `lean.abbrev` (lean_input.lua, Arc 8 Stage 4b) — a
`live` boolean read against the typed edit's SOURCE buffer, the
`editing.auto-pair` shape including its correction to resolve
`rec.buffer` rather than the active buffer. 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`
@ -1076,7 +1088,7 @@ layering, provenance, and adoption have not followed.**
- **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 eight settings registered, level 1
hooks+keymaps / packages), but with nine 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.
@ -1222,14 +1234,23 @@ Primitive-by-primitive against the list above:
`compile.lua`'s own comment admits ("command/menu undo stays
dispatchable"). `Buffer::set_generated_contents` (write + discard
history + assert `read_only`, in one authorized call) now fixes this
for the terminal snapshot; `*compilation*` and listview panels have
not yet adopted it and remain emptiable. **A second half of the same
for the terminal snapshot; **four writer mechanisms have not yet adopted
it and remain emptiable** — listview panels; `compile.lua`'s
`ensure_slot`, which serves `*compilation*` **and** `*shell-command*`;
the independent `*search-results*` panel in
`builtin/commands/default.lua`; and dired buffers. All pair an erroring
intercept with `bypass_intercept` writes over a still-writable rope.
(`*workers*`, `*help*` and `*buffer-list*` are generated but do not use
this idiom.) **A second half of the same
caveat, found in round 3: a rope write is only half of an edit.** The
owner-authorized write must be fanned out to the windows showing the
buffer and queued for replica mirrors, or the displaying window keeps
a line index describing the previous contents and the next paint
indexes the new rope with stale ranges. Adoption is therefore not a
one-line swap.
one-line swap — and the three appending buffers (`*compilation*`,
`*shell-command*`, `*search-results*`) need a streaming variant of the
primitive that does not exist yet. Listview and dired already write
whole-buffer replaces and are the cheap half.
- **Diagnostics collection** ✓ — `DiagnosticStore` + signs + unified
`error.next` source.
- **Transient selector** ✓ — the minibuffer (though its `source`
@ -1443,20 +1464,24 @@ subsystems, complementing (not replacing) subsystem tests:
### Ground truth
**Grade: missing — but the culture that would make them excellent is the
project's strongest process asset.**
**Grade: started — the first suite exists; five of the six scenarios
above do not.**
Zero cross-subsystem journey tests exist. Every acceptance suite in the
tree pins one subsystem's contract (superbly — bite-verified,
falsified-by-revert, vacuity-checked). Several of the scenarios above
are currently *untestable* because the behavior doesn't exist (install
in-session, disable, open a directory); the ones that are testable
(first launch, command discovery, worker cancellation, remote
attach/reconnect) could be written today and would immediately pin the
journey against regression. The first coherence acceptance suite should
be the §2 journey itself, growing a step at a time as steps become
real — that is how "the journey is a release gate" stops being
aspirational.
At audit time zero cross-subsystem journey tests existed. **Journey
Stage 1a created `tests/journey_acceptance.rs`**, the §2 journey itself,
seeded with steps 2 (launch unconfigured), 3 (open a real project), and
5 (edit immediately), and declared a ratchet: stages add rows, none
removes them. That is the "first launch" scenario, partially — missing
tools still have no actionable guidance to assert.
The rest is unchanged. Every other acceptance suite in the tree pins one
subsystem's contract (superbly — bite-verified, falsified-by-revert,
vacuity-checked). Command discovery, workspace lifecycle, worker
ownership, package lifecycle, and remote execution have no
cross-subsystem suite; several remain *untestable* because the behavior
doesn't exist (install in-session, disable). Steps 6–12 join
`journey_acceptance.rs` as later stages make them real — that is how
"the journey is a release gate" stops being aspirational.
(Related lesson already in the handoff: `compile_mode_acceptance`
accidentally reads the real user config — an *unintentional*
@ -1474,14 +1499,18 @@ missing runtime entity — a real arc).
### Priority 1: Protect the golden product journey
Establish the end-to-end workflow; treat regressions as release
blockers. **State: broken at step 3 (§2). Mostly wiring, and unusually
cheap:** directory-argument handling (the remaining half of step 3 —
dired Stage 1 landed the buffer it should resolve to); a find-file
surface (**done**: #162 open-by-path, #165 browsing); surfacing the
LSP spawn failure with guidance (§1.2); a
blockers. **State: runs to step 5; thin from step 6 (§2). Mostly wiring,
and unusually cheap:** directory-argument handling (**done**: Journey
Stage 1a); a find-file surface (**done**: #162 open-by-path, #165
browsing); surfacing the LSP spawn failure with guidance (§1.2); a
compile keybinding + `cargo build`/`test` default from the existing
`ProjectKind::Cargo`; a terminal keybinding; a welcome buffer. The
journey acceptance suite (§19) is the ratchet that keeps it fixed.
`ProjectKind::Cargo`; a terminal keybinding (**done**: `C-c t`, #173); a
welcome buffer. The journey acceptance suite (§19) is the ratchet that
keeps it fixed — it **exists now** (`tests/journey_acceptance.rs`,
Stage 1a), seeded with steps 2, 3, and 5.
Journey Stage 1b is the named remainder: the compile binding + Cargo
defaults, LSP spawn guidance, and the welcome buffer.
### Priority 2: Make workspace and location explicit
@ -1545,11 +1574,13 @@ Candidate arc cuts, honoring one-feature-one-branch-one-PR and the
framing workflow (each needs its own scout + framing before any
implementation — this list is direction, not commitment):
1. **Journey Stage 1** (P1): directory open + compile defaults +
LSP-failure surfacing + bindings + welcome buffer + the first
journey acceptance suite. Dired Stage 1 has landed (#165), so the
buffer a directory resolves *to* already exists; this arc routes
`pmacs .` into it rather than growing a second directory surface.
1. **Journey Stage 1** (P1): split at the new-Rust-primitive line.
**Stage 1a — landed**: directory open, the `EditorState::open` →
`resolve_target_buffer` unification, the destination-scope substrate,
and the first journey acceptance suite. It routes `pmacs .` into
#165's dired buffer rather than growing a second directory surface.
**Stage 1b — remaining**: compile defaults, LSP-failure surfacing,
bindings, welcome buffer.
2. **Discovery surface** (P4): the describe/list/where-is command
family, M-x rich rows, help unification, help prefix.
3. **Transient keymap layer** (§6): the overlay scope + lifetime

15
builtin/hooks/default.lua
View File

@ -61,6 +61,21 @@ define {
kind = "all-must-succeed",
}
define {
name = "path.open-directory",
description = "Fired when a directory path is opened (Journey Stage 1a). " ..
"Receives the canonical absolute path and an opaque " ..
"destination. Return false to CLAIM the directory and stop " ..
"the fan-out; return nothing to decline. No builtin " ..
"subscribes -- because hook callbacks only ever append, a " ..
"subscribing builtin would always claim before any user " ..
"listener could run, so this hook is the user's chain and " ..
"pmacs.path.directory_handler is the default surface it " ..
"falls back to. A callback that RAISES stops the chain and " ..
"suppresses that fallback.",
kind = "short-circuit",
}
define {
name = "editor.before-quit",
description = "Fired before the editor exits. Return false to veto.",

11
builtin/runtime/async.lua
View File

@ -77,6 +77,17 @@ end
-- inside a coroutine spawned by pmacs.async --- a bare call from main
-- thread will raise on the first yield.
function Handle:await()
-- Journey Stage 1a (Q#JR14b): `pmacs.window.commit_to` scopes the
-- acting frontend for the dynamic extent of its callback, using an
-- RAII guard on the Rust stack. Yielding out of that extent would
-- restore the scope while this coroutine is still parked, so the rest
-- of the commit would resume ambient -- silently reintroducing the
-- misrouting the scope exists to prevent. Do the awaiting BEFORE
-- entering the commit, which is what dired does with its listing.
if async_mod._in_commit_scope() then
error("await: cannot await inside pmacs.window.commit_to; " ..
"await first, then commit")
end
if not async_mod._is_complete(self._id) then
-- Yield self so pmacs.async's step() can park us. R46 carve-out:
-- this `coroutine.yield` is runtime code; package code uses

111
builtin/runtime/dired.lua
View File

@ -571,7 +571,15 @@ end
-- deliberately so (Q#DR10): the next directory is the same kind of
-- thing as the current one and belongs in the same slot, while a file
-- is not a dired buffer and belongs in the document area.
local function display(handle, opts, departed)
--
-- `captured` (Journey Stage 1a, Q#JR14) is the destination window a
-- background open must land in. It is NOT the same as "wherever the
-- scoped frontend is looking now": the scope fixes the *frontend*, and
-- within one frontend the selected window can still have moved to
-- another split while the listing was in flight. The preflight cannot
-- catch that -- the captured window is still live and still holds its
-- captured buffer -- so honoring it is this function's job.
local function display(handle, opts, departed, captured)
local side = nil
if departed ~= nil then
-- Dired's own window, not the request's: walking a tree in a side
@ -587,6 +595,11 @@ local function display(handle, opts, departed)
-- both the substrate's documented policy and Emacs's, so dired does
-- not try to unpin the user's panel.
pmacs.window.display(handle.buf, { side = side, select = true })
elseif captured ~= nil then
-- `select = true` because the rest of the commit -- seat_cursor via
-- `pmacs.editor.move_to_line` -- acts on the frontend's ACTIVE
-- window, so the seat would land in the wrong window otherwise.
pmacs.window.display(handle.buf, { window = captured, select = true })
else
pmacs.window.switch_buffer(handle.buf)
end
@ -598,7 +611,7 @@ end
pmacs.dired = pmacs.dired or {}
local OPEN_OPTS = { display = true, select_name = true }
local OPEN_OPTS = { display = true, select_name = true, dest = true }
-- Open `path`'s dired buffer, replacing `departed` (a handle) in the
-- window it occupies when this is a navigation rather than a fresh
@ -629,36 +642,76 @@ local function open_directory(path, opts, departed)
local sort_mode = (handle_for_path(canonical) or {}).sort_mode or SORT_MODES[1]
local entries, errors = read_listing(canonical, sort_mode)
local handle = claim_handle(canonical)
handle.entries = entries
handle.errors = errors
handle.sort_mode = sort_mode
-- Everything from here down MUTATES: it claims or finds a handle,
-- creates a buffer, reads the ambient buffer for `prev`, and paints.
-- None of it is undoable, and none of it may run against a
-- destination that has gone away -- so when the caller captured one
-- (Journey Stage 1a, Q#JR14), the whole commit runs inside
-- `pmacs.window.commit_to`, which validates the destination BEFORE
-- invoking this and scopes the acting frontend for its extent.
--
-- Note the await above is deliberately OUTSIDE the commit: awaiting
-- inside it is refused (Q#JR14b), because a yield would restore the
-- scope while this coroutine is still parked.
local function commit()
-- The captured window, read once. Everything below that would
-- otherwise consult "the active window" must consult THIS instead:
-- the scope pins the frontend, not the selected window, and a split
-- or panel can take focus within that frontend while the listing is
-- in flight (Q#JR14).
local captured = opts.dest ~= nil and opts.dest:window() or nil
-- `q` returns to the buffer you came from, never to another dired
-- buffer (which would trap `q` walking back down the tree); on a
-- descent the arriving buffer inherits the departing one's origin.
if departed ~= nil then
handle.prev = departed.prev
else
local active = pmacs.window.buffer()
if active ~= nil and handle_for_buffer(active) == nil then
handle.prev = active
local handle = claim_handle(canonical)
handle.entries = entries
handle.errors = errors
handle.sort_mode = sort_mode
-- `q` returns to the buffer you came from, never to another dired
-- buffer (which would trap `q` walking back down the tree); on a
-- descent the arriving buffer inherits the departing one's origin.
if departed ~= nil then
handle.prev = departed.prev
else
local active
if captured ~= nil then
active = pmacs.window.buffer(captured)
else
active = pmacs.window.buffer()
end
if active ~= nil and handle_for_buffer(active) == nil then
handle.prev = active
end
end
paint(handle)
display(handle, opts, departed, captured)
-- Seating happens after the display: `switch_buffer` zeroes the
-- window cursor, so an earlier seat would be discarded.
seat_cursor(handle, opts.select_name, 1)
kill_departed(departed, handle)
return handle.buf
end
paint(handle)
display(handle, opts, departed)
-- Seating happens after the display: `switch_buffer` zeroes the
-- window cursor, so an earlier seat would be discarded.
seat_cursor(handle, opts.select_name, 1)
kill_departed(departed, handle)
return handle.buf
if opts.dest == nil then
-- Interactive path (`C-x d`, tree descent, refresh): the acting
-- frontend is still ambient a tick later, which is what dired has
-- always relied on. Migrating these onto a captured destination too
-- is a named deferral, not this stage's work.
return commit()
end
local ok, result = pmacs.window.commit_to(opts.dest, commit)
if not ok then
error(string.format("destination is gone (%s)", tostring(result)))
end
return result
end
function pmacs.dired.open(path, opts)
return open_directory(path, opts, nil)
end
-- Every interactive entry point funnels through here: spawn the
-- coroutine the await needs, and turn a failure into a status message
-- rather than an uncaught raise inside `pmacs.async` (which would land
@ -670,6 +723,20 @@ local function open_async(path, opts, departed, where)
end)
end
-- Journey Stage 1a (Q#JR7): dired is the DEFAULT directory surface, not
-- a `path.open-directory` subscriber.
--
-- It cannot be a subscriber and still be replaceable. `HookRegistry.add`
-- only appends, and builtins load before `init.lua`, so a dired
-- subscription would always run first and always claim -- no user
-- listener could ever win. The hook is therefore the user's chain and
-- this slot is the fallback the editor consults when that chain
-- declines. Replace it to change what opens a directory; set it to nil
-- to disable directory opening entirely.
pmacs.path.set_directory_handler(function(path, dest)
open_async(path, { dest = dest }, nil, "dired")
end)
-- ---------------------------------------------------------------------------
-- Commands
-- ---------------------------------------------------------------------------

1883
builtin/runtime/lean_abbrev.lua Normal file
View File

File diff suppressed because it is too large Load Diff

517
builtin/runtime/lean_input.lua Normal file
View File

@ -0,0 +1,517 @@
-- lean_input.lua --- the Lean 4 Unicode input method (Arc 8 Stage 4b).
--
-- Typing `\alpha` gives `α`; `\<>` gives `⟨⟩` with the point between.
-- The table is vendored in lean_abbrev.lua, generated from
-- vscode-lean4 — see that file's header and Q#LN11.
--
-- This is a typed-edit consumer (Stage 4a, Q#LN10) registered AHEAD of
-- auto-pairing at priority 50. The ordering is load-bearing, not
-- cosmetic: 64 abbreviation keys contain a character in the `lean4`
-- pair set (`\[[]]` → `⟦⟧`, `\{{}}` → `⦃⦄`), so with pairing first,
-- typing `\[` would insert `[]` with the point between and corrupt the
-- pending key to `\[]` before the second `[` arrives — `\[[]]` becomes
-- unreachable. Priority, not load order, is what decides this; that is
-- the whole reason Stage 4a exists.
--
-- The consumer therefore claims every keystroke that EXTENDS an open
-- pending abbreviation, not merely one that completes an expansion. A
-- consumer that claimed only completed expansions would hand each
-- intermediate `[` to pairing, which is the same corruption by a
-- different route. "Claimed" means the chain stops, not that an edit
-- was made (Q#LN22).
--
-- UNDO IS CROSS-PEER-DEGRADED, and this is accepted rather than papered
-- over (Q#LN21). `classify_key` (src/optimistic.rs) returns `Insert(c)`
-- for `\` and for every ASCII letter — only the nine built-in pair
-- chars are excluded — so on a CRDT frontend `\alpha` arrives as six
-- SOURCE-peer optimistic inserts while the expansion is a single
-- DAEMON-peer replace spanning all six. Undo across that boundary is
-- not chronologically arbitrated. This is the same defect Q#LN6 already
-- accepts for `⟨⟩`, one order of magnitude wider: it is every
-- abbreviation the user types, not a few brackets. The general fix is
-- chronological cross-peer undo arbitration, named substrate work.
-- `set_round_trip_input` would fix it and is rejected — it also makes
-- `dispatch_idle` report false, so RET would stop inserting a newline.
--
-- Framing: docs/lean4-mode-framing.md Q#LN11, Q#LN21, Q#LN22.
pmacs.lean_input = pmacs.lean_input or {}
local ed = pmacs.editor
local LEADER = "\\"
local CURSOR = "$CURSOR"
pmacs.config.define {
name = "lean.abbrev",
description = "Expand \\-prefixed abbreviations into Unicode symbols in Lean 4 buffers.",
type = "boolean",
default = true,
mutability = "live",
}
-- ---------------------------------------------------------------------
-- The table, and the two indexes derived from it at load time
-- ---------------------------------------------------------------------
-- `best[p]` is the symbol for the shortest key having `p` as a prefix,
-- ties broken by the key's position in the vendored sequence. Both
-- halves matter: 101 prefixes have equal-shortest candidates that
-- resolve to DIFFERENT symbols (`f` → `‹` from `f<`, not `›` from
-- `f>`), and the sequence's order is the only place that tie is
-- recorded. `pairs` over a map-shaped table could not express it.
--
-- `eager[k]` marks the 1,550 keys that are complete and have no longer
-- key extending them — the ones that expand the moment they are typed,
-- with no terminator. `to` is NOT one of them (`top`, `to0`, `toa`),
-- which is exactly the case that reads as eager until the table is
-- consulted.
local best, eager = {}, {}
do
local seq = pmacs.lean_abbrev
if type(seq) ~= "table" then seq = {} end
local extended = {}
for i = 1, #seq do
local entry = seq[i]
local key, symbol = entry[1], entry[2]
-- Walk every prefix of the key, including the key itself. Iterating
-- the sequence in order and only overwriting on a STRICTLY shorter
-- key is what makes the source-order tiebreak fall out: an equal
-- length arriving later loses to the one already recorded.
for n = 1, #key do
local p = key:sub(1, n)
local cur = best[p]
if cur == nil or #key < cur.len then
best[p] = { symbol = symbol, len = #key }
end
if n < #key then extended[p] = true end
end
end
for i = 1, #seq do
local key = seq[i][1]
if not extended[key] then eager[key] = true end
end
end
-- Test seam (leading underscore = not stable API). Acceptance 45g reads
-- these to pin self-consistency properties a corrupt emit would break —
-- it cannot diff against `abbreviations.json`, which is not shipped.
function pmacs.lean_input._resolve(text)
local hit = best[text]
return hit and hit.symbol or nil
end
function pmacs.lean_input._is_eager(key)
return eager[key] == true
end
-- ---------------------------------------------------------------------
-- Pending state: one record per FRONTEND (Q#LN22)
-- ---------------------------------------------------------------------
-- Keyed by frontend id, with the buffer stored inside and compared by
-- value. Q#LN22 specifies the key as `(frontend, buffer)`; a per-
-- frontend slot is equivalent here and avoids inventing a scalar
-- buffer key (`BufferId`'s inner value is deliberately private, R22).
-- The generality a two-level map would add is unreachable: a frontend
-- has one point, and `buffer.after-switch` clears that frontend's slot,
-- so no frontend can hold pending state in a buffer it is not in.
--
-- Per-frontend rather than per-buffer is NOT a refinement — a buffer-
-- keyed table lets either frontend consume or discard the other's
-- half-typed abbreviation in a shared buffer, which is the ordinary
-- TUI-plus-GPU configuration this project ships.
local pending = {}
-- Expansions the chain consumer decided on but did NOT perform, keyed
-- the same way. See `run_deferred` below for why they wait.
local deferred = {}
local function frontend_id()
local ok, id = pcall(function() return pmacs.frontend.id() end)
if ok then return id end
return nil
end
-- Is `rec` a typed edit that continues `p` exactly? Conservative by
-- construction (Q#LN22): abandonment is LAZY because pmacs has no
-- cursor-motion hook, so every guard that would have been checked at
-- the moment the user left is checked here instead, at the next typed
-- edit.
local function still_valid(p, rec, buf)
if p.buffer ~= rec.buffer or p.window ~= rec.window then return false end
-- The point must still be at the end of the pending span: the leader,
-- plus what has been typed into it, plus the character that just
-- landed.
if rec.effective_start ~= p.start_offset + 1 + #p.text then return false end
-- Exactly one edit since this frontend last extended the pending
-- abbreviation — the one being processed now. Deliberately strict
-- across frontends: `revision()` is BUFFER-GLOBAL, so a peer editing
-- the shared buffer invalidates this record even though it edited
-- elsewhere. Keeping it alive would mean translating and validating
-- the span through arbitrary peer edits, substrate Stage 4b does not
-- add.
local ok, rev = pcall(function() return buf:revision() end)
if not ok or rev ~= p.expected_revision + 1 then return false end
return true
end
-- ---------------------------------------------------------------------
-- Expansion
-- ---------------------------------------------------------------------
-- Right-gravity translation of `pos` through the effective edit —
-- pair.lua's shape, for the same reason: the point sits AFTER the
-- replaced span (on the terminator, or on a closer pairing inserted)
-- and has to move with it.
local function translate(pos, estart, estop, einserted)
if pos < estart then return pos end
if pos > estop then return pos - (estop - estart) + einserted end
return estart + einserted
end
-- Replace the pending span (leader + typed text) with `symbol`.
--
-- The span deliberately STOPS BEFORE the terminator. Including the
-- terminator would make the expansion and the terminator one edit, but
-- it would also swallow whatever auto-pairing did with that terminator
-- — and a pair character is a legal terminator (`\alp(`). One undo
-- restores the same text either way, because the terminator was its own
-- insert to begin with.
--
-- ONE `buf:replace`: one undo step, one CRDT op, one effective-edit
-- verification. A rejection drops the pending state and does not retry,
-- the same discipline as comment.lua's Q#CT5 and pair.lua.
local function expand(buf, start, span_end, symbol)
local cursor_at = symbol:find(CURSOR, 1, true)
local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol
-- The context to compare against AFTER the edit. A buffer intercept
-- may switch window or buffer while the replace runs; the point in
-- whatever it switched to is not ours to move.
local win0 = pmacs.window.current()
local point0 = ed.cursor()
local ok, estart, estop, einserted = pcall(function()
return buf:replace(start, span_end, text)
end)
if not ok then
ed.set_status("lean abbreviation rejected by buffer intercept")
return nil
end
if estart ~= start or estop ~= span_end or einserted ~= #text then
ed.set_status("lean abbreviation altered by buffer intercept")
return nil
end
-- The point MUST be placed explicitly. Unlike pairing's at-cursor
-- insert, this replace SHRINKS the buffer — `\alpha` (6 bytes)
-- becomes `α` (2) — and a point left at the pre-edit offset is past
-- the new end. Every later self-insert is then silently rejected and
-- the editor looks dead. There is no daemon re-grounding that covers
-- this; that only holds for an edit that lands at the cursor.
--
-- Context-guarded exactly as pair.lua's `repair_cursor` is: if the
-- intercept switched us elsewhere, `goto_byte` would move the point
-- of a buffer that has nothing to do with this expansion.
if pmacs.window.current() == win0 and pmacs.window.buffer() == buf then
if cursor_at then
ed.goto_byte(start + cursor_at - 1)
else
ed.goto_byte(translate(point0, estart, estop, einserted))
end
end
return start + #text
end
-- ---------------------------------------------------------------------
-- The consumer
-- ---------------------------------------------------------------------
-- Chain invocations not yet matched by a `run_deferred`.
--
-- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly
-- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`,
-- and a nested run re-enters every subscriber — including this module's
-- deferred-expansion subscriber, while the OUTER chain is still walking
-- its consumer list and pairing has not yet seen the terminator. A
-- nested run that performed the expansion would reproduce exactly the
-- bug deferring exists to fix: pairing resumes afterwards holding a
-- record the replace has invalidated, declines, and the closer is lost.
--
-- Counting has to happen INSIDE the chain and BEFORE any consumer that
-- might start a nested fan-out. A subscriber registered alongside
-- `run_deferred` is too late — the whole nested fan-out completes
-- inside the outer chain's subscriber, before either of them runs. And
-- counting in the expander itself is not enough: a lower-priority
-- consumer may CLAIM and stop the chain before the expander is
-- reached, so a nested pass would go uncounted while its
-- `run_deferred` still ran (round 11's fix, round 12's defect).
--
-- Hence a separate no-op consumer at the minimum priority, which runs
-- first in every chain invocation that reaches any consumer at all.
-- Its guarantee is exactly the ordering contract the chain already
-- rests on, and it degrades safely: the only thing that can skip it is
-- a claim ahead of it, which skips the expander too, so nothing is
-- queued in that fan-out either.
local depth = 0
local function count_fan_out()
depth = depth + 1
return false
end
local function on_typed_edit(rec)
local fid = frontend_id()
if fid == nil then return false end
-- A fan-out carrying no record is still information: a paste,
-- programmatic edit or replicated op landed, so whatever this
-- frontend had pending no longer describes the buffer. Drop it and
-- decline — this is why the chain calls consumers with nil rather
-- than skipping them (Q#LN10).
if not rec then
pending[fid] = nil
return false
end
if not (ed.this_command and ed.this_command() == "buffer.self-insert") then
pending[fid] = nil
return false
end
-- Both gates resolve against the SOURCE buffer of the typed edit, not
-- the active one — a context-switching command may have replaced it
-- by callback time (pair.lua round 2, finding 2).
if not pmacs.config.get("lean.abbrev", rec.buffer) then
pending[fid] = nil
return false
end
local lang
if pmacs.lsp and pmacs.lsp.buffer_language then
local ok, l = pcall(pmacs.lsp.buffer_language, rec.buffer)
if ok then lang = l end
end
if lang ~= "lean4" then
-- No pending abbreviation is ever OPENED outside a `lean4` buffer:
-- `\` in Rust is an ordinary character and `\[` there still pairs.
pending[fid] = nil
return false
end
local buf = pmacs.window.buffer()
if not buf or buf ~= rec.buffer or pmacs.window.current() ~= rec.window then
pending[fid] = nil
return false
end
-- Fail closed on a transformed source self-insert, as pairing does:
-- expanding on top of a relocated or rewritten character compounds
-- the intercept's result.
if not rec.clean then
pending[fid] = nil
return false
end
-- ...and on a source edit whose context is no longer current. The
-- buffer and window matching is not enough: a redefined self-insert
-- can insert the character and THEN move the point, and expanding
-- over a span the user has left teleports them back into it. Pairing
-- makes the same three-part check for the same reason.
if ed.cursor() ~= rec.post_cursor then
pending[fid] = nil
return false
end
local revision
do
local ok, rev = pcall(function() return buf:revision() end)
if not ok then
pending[fid] = nil
return false
end
revision = rev
end
local p = pending[fid]
if p and not still_valid(p, rec, buf) then
p = nil
pending[fid] = nil
end
local ch = rec.char
-- No pending abbreviation: only the leader opens one.
if not p then
if ch == LEADER then
pending[fid] = {
buffer = rec.buffer,
window = rec.window,
start_offset = rec.effective_start,
text = "",
expected_revision = revision,
}
-- Claimed: the leader belongs to the abbreviation, and pairing
-- has no interest in it either way.
return true
end
return false
end
-- Pending: does any key still have `text .. ch` as a prefix?
local extended = p.text .. ch
if best[extended] then
p.text = extended
p.expected_revision = revision
if eager[extended] then
pending[fid] = nil
deferred[fid] = {
buffer = rec.buffer,
window = rec.window,
start_offset = p.start_offset,
text = extended,
symbol = best[extended].symbol,
re_arm = false,
}
end
-- Claimed either way: an extension that has not yet completed must
-- NOT reach auto-pairing (`\[` in `\[[]]`), and a completing one is
-- part of the abbreviation, not a character pairing should react to.
return true
end
-- `ch` does not extend the abbreviation: it TERMINATES it, and a
-- terminator is an ordinary character that auto-pairing is entitled
-- to react to (`\alp(` must give `α()`). So the expansion is
-- DEFERRED to the subscriber below and this returns false, leaving
-- pairing a record whose offsets still describe the buffer.
--
-- Expanding here and returning false would not do: the replace makes
-- pairing's copy of the record stale, so pairing declines and the
-- closer is silently lost. Expanding here and returning true is
-- worse — it is what shipped in the first revision of this file, and
-- it makes every pair-character terminator silently unpaired.
pending[fid] = nil
if best[p.text] and #p.text > 0 then
deferred[fid] = {
buffer = rec.buffer,
window = rec.window,
start_offset = p.start_offset,
text = p.text,
symbol = best[p.text].symbol,
-- A terminating `\` re-arms as a NEW leader at its own position
-- (`\al\to` → `∀→`). Upstream gets this from `processChange`,
-- where a finished abbreviation reports `isAffected = false` and
-- so does not suppress the new-leader branch. This is NOT the
-- `\\` case: there the pending text is empty, `\` EXTENDS, and
-- the result is one literal backslash with nothing left open.
re_arm = ch == LEADER,
}
elseif ch == LEADER then
-- Nothing to expand, but the leader still opens a fresh
-- abbreviation where it landed.
pending[fid] = {
buffer = rec.buffer,
window = rec.window,
start_offset = rec.effective_start,
text = "",
expected_revision = revision,
}
return true
end
return false
end
-- The deferred expansion, on its own `buffer.after-edit` subscriber.
--
-- It runs AFTER the whole typed-edit chain — this chunk loads after
-- typed_edit.lua, and hook callbacks run in registration order — so
-- auto-pairing has already reacted to the terminator by the time the
-- expansion rewrites the text in front of it. Pairing's closer lands
-- after the terminator, outside the replaced span, so it survives.
--
-- It must also run BEFORE lsp.lua's subscriber (Q#AP7): that one
-- flushes `didChange` synchronously on the signature-trigger path, and
-- a server told about `\alp ` instead of `α ` stays wrong until the
-- next edit. This chunk loads before lsp.lua for exactly that reason.
--
-- A claim by ANY chain consumer stops the chain but not this — which
-- is the point. Pairing claims the terminator it reacts to.
local function run_deferred()
-- Match off this fan-out's chain invocation. `> 1` means the outer
-- chain is still mid-list — pairing has not had the terminator yet —
-- so the queued expansion stays queued for the outer pass. The clamp
-- keeps this honest if a claim beat the counting consumer, in which
-- case nothing was queued in that fan-out either.
local level = depth
if depth > 0 then depth = depth - 1 end
if level > 1 then return end
local fid = frontend_id()
if fid == nil then return end
local d = deferred[fid]
deferred[fid] = nil
if not d then return end
local buf = pmacs.window.buffer()
if not buf or buf ~= d.buffer or pmacs.window.current() ~= d.window then
return
end
-- The span must still hold exactly what was typed into it. Pairing
-- only edits at the point, which is past this span, so in practice
-- this holds; a buffer intercept is not obliged to be so polite.
local span_end = d.start_offset + 1 + #d.text
local ok, actual = pcall(function()
return buf:slice(d.start_offset, span_end)
end)
if not ok or actual ~= LEADER .. d.text then return end
local after = expand(buf, d.start_offset, span_end, d.symbol)
if after and d.re_arm then
local rev_ok, rev = pcall(function() return buf:revision() end)
if rev_ok then
pending[fid] = {
buffer = d.buffer,
window = d.window,
start_offset = after,
text = "",
expected_revision = rev,
}
end
end
end
-- Q#KR11's seam: a detached frontend's pending state must not outlive
-- it. Ids are monotonic, so this table would otherwise grow for the
-- life of the session.
pmacs.hook.add("frontend.detached", function(fid)
pending[fid] = nil
deferred[fid] = nil
end)
pmacs.hook.add("buffer.after-edit", run_deferred)
-- `buffer.after-switch` fires with NO arguments, so it cannot say whose
-- switch it was. The acting frontend is the one that produced the most
-- recent dispatched input event, which is what `pmacs.frontend.id()`
-- reports at callback time. Clearing every entry instead would let one
-- frontend's navigation discard another's half-typed abbreviation.
pmacs.hook.add("buffer.after-switch", function()
local fid = frontend_id()
if fid ~= nil then pending[fid] = nil end
end)
-- Runs first in every chain invocation that reaches a consumer at all,
-- which is what makes the nesting count trustworthy — see `depth`. It
-- declines, always: it observes, it does not participate.
pmacs.typed_edit.add_consumer {
name = "lean-abbrev-fan-out-counter",
priority = -2147483648,
fn = count_fan_out,
}
pmacs.typed_edit.add_consumer {
name = "lean-abbrev",
priority = 50,
fn = on_typed_edit,
}

634
docs/active-work.md
View File

@ -1,18 +1,22 @@
# Active work — cross-machine resume ledger
**Snapshot: 2026-07-26.** This file records volatile work that has not
**Snapshot: 2026-07-27.** 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.
**Two lane headers below are stale on purpose**, pending the docs updates
their own lanes owe: multi-root LSP affinity **#161 has merged** (the
Lean 4 lane still says IN REVIEW; its continuation is PR #167) and GPU
terminal input **#166 has merged** (its lane still says IN REVIEW; PR
#168 records it). Trust the canonical-base line below over a lane header:
if a PR number appears in `git log --first-parent githubsucks/main`, it
has landed regardless of what its lane says. (The inline-math lane was
here too until #172 removed it — that is the update those two owe.)
**One lane below is retained past its merge, and says so at its own
head**: the PTY terminate diagnostic (#176), because no landed-doc PR
owns moving its facts to `docs/agent-handoff.md` yet, and rule 4 removes
a lane only *after* that move. Every other merged lane has been removed —
the Lean 4 and GPU-terminal-input headers this paragraph used to
disclaim are gone, as are the inline-math (#172), dired (#169), and
terminal config + copy mode lanes — the last of these was #180's work,
folded into #182 so two open PRs would stop re-conflicting in this file.
**Trust the canonical-base line below over any lane header**: if a PR
number appears in `git log --first-parent githubsucks/main`, it has
landed regardless of what a lane says.
## Repository authority
@ -23,16 +27,15 @@ 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` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel
Stage 2A #177, the bottom-panel Stage 2 framing #175, terminal
configuration Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the
CRDT undo repro #157, the inline-math landed-doc refresh #172, the
bottom-panel landed-doc refresh #156, the inline-math slice #158,
dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2
#161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean 4
Stage 1 #160, and the minimap blank-slab fix #159; protocol v20). The
previous snapshot named `d152120`; the recovery check below accepts it
or anything newer.
`githubsucks/main` @ `c2d56ff` (Journey Stage 1a #182, which
incorporated terminal configuration + copy mode #180, atop Lean 4
Stage 4b #181 and the previously recorded landed work; protocol v20).
The previous snapshot named `42025e4`, and **the recovery floor
advances with it**: the check below now requires `c2d56ff` or newer,
so a tree at `42025e4` no longer passes. That is
deliberate — the floor moves with the base, because a check that
accepts an older commit than the declared base passes on a tree the
rest of this file does not describe.
**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
@ -68,14 +71,21 @@ git worktree list
git status --short --branch
```
The `git log` command must expose `c93f9ee` — the base named above — or a
The `git log` command must expose `c2d56ff` — the base named above — or a
newer intentional main. Keep this threshold and the canonical-base line in
step: a recovery check that accepts an older commit than the base it
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.
## PTY terminate diagnostic lane — IN REVIEW (PR #176)
## PTY terminate diagnostic lane — MERGED (PR #176)
> **Lane retained deliberately, and it is the next one to close.** #176
> merged into `main` @ `bf8878f` (2026-07-26); rule 4 below removes a
> merged lane, but only after its durable facts reach
> `docs/agent-handoff.md`. **That absorption is unowned** — no landed-doc
> PR exists for #176 — so removing the lane now would delete the record
> instead of moving it. Whoever opens that PR removes this section.
- Portable branch: `githubsucks/pty-terminate-eperm`; worktree
`../pmacs-math-slice`. **PR #176**, base `main`, based on `ccf29e3`
@ -161,176 +171,6 @@ If it does not, stop and repair the remote/fetch configuration.
to recur; the next occurrence carries its own evidence under whoever's
PR, and a Stage B framing follows then.
## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b, 4a MERGED; 4b is next
- **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.
### 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.
- **Stage 4a merged as #179** (`main` @ `a27f646`, 2026-07-26) — the
typed-edit consumer chain. Worktree `../pmacs-lean-stage4`, branched
off `main` @ `d400f30`; retained, carrying nothing unmerged.
`docs/lean4-mode-framing.md` **revision 8** remains the approved
framing. **Stage 4b (the Lean-specific half) is framed and not
started.**
- **Round 6 review found five P1s, four of them internal to rev 6** —
facts about pmacs the revision asserted without checking, while its
external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint
omitted the test file its own acceptance requires; pending
abbreviation state was keyed by buffer when pmacs is **multi-frontend**
(`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already
frontend-keyed, and `buffer.after-switch` fires with NO arguments, so
a buffer-keyed clear lets any frontend discard another's pending
state); the shortest-match rule was missing its **tie-break by source
declaration order**, which 101 prefixes depend on and a `pairs`-
iterated Lua map cannot express; and the generator's "abort on keys
needing escaping" rule **rejects the real table** (`\` is a key, `"`
begins eleven).
- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared
the upstream package ships no README after fetching the package root,
with the directory listing showing `src/README.md` already in hand.
The README states the tie rule in one sentence.
- **Round 7 review found one remaining P1 in acceptance 45i.** Rev 7
required A's pending abbreviation to survive B editing the same
buffer, while Q#LN22 also required an exact buffer-revision advance.
Those cannot both hold: revisions are buffer-global and every edit
bumps them. Rev 8 keeps the conservative guard and separates
ownership from survival — B cannot consume A's record, but B editing
the shared buffer invalidates A lazily; B switching buffers or
detaching remains frontend-scoped when no shared-buffer edit
intervenes.
- **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).**
4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua`
plus `pair.lua` re-expressed as one registered consumer, no behavior
change. 4b is the input method. The split is forced by §4's own rule,
which Stage 4's risk column ("refactors `pair.lua`'s provenance read")
broke while the prose called the stage Lean-only.
- **This is the SECOND consecutive re-scout to find that rule broken**
(round 4 found it for Stage 3). Rev 5 had even noticed the shape and
answered it with a commit boundary. **A commit boundary is not a review
boundary.** Re-check every remaining stage against §4 at scout time;
the rule is not self-enforcing.
- **Rev 5's expansion semantics were wrong in three ways**, found by
reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring
from behavior. Resolution is *shortest key having the input as a
prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no
terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'`
is a key, so `\\` → `\`); and an unmatchable tail is **appended**,
not dropped (`\alp7` → `α7`).
- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving
the cursor out abandons it") was not buildable. Abandonment is lazy —
validated at the next typed edit — and the criterion now asserts what
pmacs can actually detect. Upstream drives this off `changeSelections`;
that seam does not exist here.
- **`dispatch_key` is only half the production path for 4b.** The
auto-pair suite gets away with dispatch-only because Q#AP1 removed the
pair chars from the optimistic classifiers; `\` and the letters are
NOT excluded, so on a CRDT frontend the optimistic producer is the real
path. That producer is `#[cfg(feature = "crdt")]` and CI never enables
`crdt`, and the gate list runs `--features crdt` only for `--lib` — a
crdt-gated integration test is **dark twice over**.
- The whole expansion has cross-peer-degraded undo (Q#LN21): six
source-peer optimistic inserts replaced by one daemon-peer op.
`set_round_trip_input` would fix it and is rejected — it also disables
`dispatch_idle`, so RET stops inserting a newline.
- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all
keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are
proper prefixes of another (so 1,550 expand eagerly), **26** values
carry `$CURSOR`, and **119** are multi-codepoint — the 26
`$CURSOR`-bearing values plus 93 others.
- Citation sweep per COHERENCE §25: five live citations moved in the 50
commits since rev 5 — `take_typed_edit` 12827→12990,
`handle_server_requests` 1549→1815, `fs.stat` 93→133,
`detect_buffer_language` 452→457, `send_request`/`send_notification`
9342/9361→9507/9527.
### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch)
- 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.
## The CRDT half of the test corpus is dark in CI — NEEDS A LANE
- **No branch, no framing yet.** Found while gating #166, then measured
@ -342,11 +182,18 @@ If it does not, stop and repair the remote/fetch configuration.
Every `#[cfg(feature = "crdt")]` test is therefore **not compiled** in CI,
not merely skipped.
- **Measured, `--list` under CI's exact flags versus the same flags plus
`crdt`: 3,024 vs 3,288 — 264 tests dark.** Per target:
`crdt`: 3,176 vs 3,449 — 273 tests dark.** Re-measured at `74301d1`
(2026-07-26; at `fe8b8ba` it read 3,170 vs 3,443, the same 273 dark —
#176 added six tests, none of them `crdt`-gated). **The number moves
with every merge and must be
re-measured, not quoted.** #168 reported 3,024 vs 3,288 — 264 dark,
177 in the library — at `1b6a084`; #178 then added CRDT-only
generated-buffer coverage, and other lanes landed CRDT tests in
between. Per target:
| dark | CI | full | target |
|---:|---:|---:|---|
| 177 | 1,832 | 2,009 | **the library itself** (`src/lib.rs`) |
| 185 | 1,848 | 2,033 | **the library itself** (`src/lib.rs`) |
| 21 | 15 | 36 | `m5_5_acceptance` |
| 13 | 1 | 14 | `gpu_invocation_acceptance` |
| 13 | 1 | 14 | `gpu_initial_target_acceptance` |
@ -358,15 +205,20 @@ If it does not, stop and repair the remote/fetch configuration.
| 3 | 0 | 3 | `compile_mode_crdt_acceptance` |
| 2 | 22 | 24 | `theme_faces_acceptance` |
| 2 | 0 | 2 | `m11_5_semantic_acceptance` |
| 1 | 14 | 15 | `terminal_copy_mode_acceptance` |
| 1 | 9 | 10 | `vterm_stage1_acceptance` |
| 1 | 7 | 8 | `statusline_segments_acceptance` |
| 1 | 10 | 11 | `gpu_font_acceptance` |
| 1 | 0 | 1 | `auto_indent_crdt_acceptance` |
| 1 | 0 | 1 | `m10_11_perf` |
The rows sum to 273; the table is the whole census, not its head.
- **The single worst line is the library.** `cargo test --lib --features crdt`
is a REQUIRED local gate in `CLAUDE.md`, and CI has never run it. 177
library tests — the whole CRDT half — are developer-machine-only.
is a REQUIRED local gate in `CLAUDE.md`, and CI has never run it. 185
library tests — the whole CRDT half — are developer-machine-only, and
that count grows with every merged branch that adds a `crdt`-gated
unit test.
- **Ten suites run zero or one test in CI**, including `gpu_initial_target`
(#148's entire acceptance, 1/14), `gpu_invocation` (#141's, 1/14), and
`a37`, the Vterm Stage 3 real-daemon/real-PTY/real-wgpu path that #135
@ -420,287 +272,65 @@ If it does not, stop and repair the remote/fetch configuration.
- Mitigating fact, verified rather than assumed: #166's three unit pins are
**not** `crdt`-gated and do run under CI's exact flags, including the
controller-release pin whose only job is catching the plausible wrong fix.
- **This lane also owns a `--lib --features crdt` flake, observed and
scoped without overclaiming its cause** (inherited from #178's gating,
where the terminal lane recorded it). `cargo test --lib --features
crdt` failed ~1 run in 5 on
`process::tests::setsid_escapee_is_not_reaped_and_teardown_reclaims_readers`
— `active_reader_probe` returning `None` at `process.rs:3179` ("live
runtime probe"). **Pre-existing and unrelated to #178:** that branch
did not touch `src/process.rs` at all, and the test passed 10/10
standalone; the observed
failures were during parallel full-suite runs. That localizes the
trigger to suite load or interaction, but does **not** distinguish
parallelism from another full-suite effect — no serial full-suite bite
was run. The leading code-path explanation is the known `drain_until`
trap: draining for `Started` also ticks, and a tick can reap the leader
before the following `active_reader_probe`. That is an inference from
the failure site and control flow, not yet a falsified root cause.
Discriminating it belongs here. Two unnamed CRDT failures in #178's
round-2 gating are a plausible match but remain **unattributed** — no
test names were captured.
- **A second standing obstacle for this lane:** `cargo clippy --workspace
--all-targets --features crdt -- -D warnings` **fails on `main`** —
measured at `74301d1`: seven errors before the build aborts, four in
`src/daemon.rs` (`useless_conversion` at 3996, missing doc backticks at
4076, `too_many_lines` 112/100 at 4083, an unneeded `mut` at 4965) and
three in `tests/vterm_stage3_acceptance.rs` (`too_many_lines` at 637
and 793, a redundant `continue` at 843). **Treat that as a lower
bound, not an inventory:** Clippy abandons the remaining targets once
one fails, and a run on an older tree surfaced a further doc-backticks
error in `tests/auto_indent_crdt_acceptance.rs:42` that this run never
reached. The
standing gate list runs Clippy without `crdt`, so these lints have
never been enforced. Any CI job that compiles the `crdt` targets has to
fix them first or it will be red on arrival.
## Terminal config + copy mode arc — Stage 1 MERGED; Stage 2 IN REVIEW
## Bottom-panel lane (Arc 7) — 2B-1 IN GATING
- 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 MERGED as #173** (`main` @ `cf54270`, 2026-07-26, one review
round, all twelve checks green). Branch `githubsucks/terminal-config`
and worktree `../pmacs-terminal-config` retained. Profiles, scrollback,
a per-terminal configurable escape key, and the `C-c t` opening
binding; no protocol change. Main was integrated **twice** during the
single review round (`ccf29e3`, then `c93f9ee` after the first merge
left the PR conflicting) — see the no-CI-while-conflicting fact below.
- **Stage 2 = `githubsucks/terminal-copy-mode`**, worktree
`../pmacs-terminal-copy-mode`, based on `githubsucks/main` @
`cf54270`. Copy mode: `M-x terminal.copy-mode` / `C-c C-t`.
- **Stage 2 ships eight of nine criteria, and the missing one is named.**
Criterion 17 (a real semantic frontend proving neither daemon buffer
nor mirror mutates) is **not pinned**: the optimistic apply exists only
in `pmacs-gpu/src/main.rs`, and the headless `SemanticClient` every
other semantic test uses has no optimistic path, so a faithful test
must drive the real GPU binary — the `a37` foundation, which CI never
compiles, silently skips without the binary, and is load-sensitive. A
second test on that footing buys the appearance of coverage. Both
halves of the mechanism are pinned **ungated** instead: acceptance 16
(the guard is armed — `dispatch_idle` false while the snapshot is
focused) and 16b (the daemon holds — `is_read_only()` is **true** at
the rope, so an op that did arrive is refused by `ensure_writable()`).
**Rounds 2-3 changed what 17 must show.** 16b asserted `false` through
round 1, documenting the hazard; round 2 closed it. So the eventual
real-GPU test must look for **mirror mutation plus daemon refusal —
divergence** — not the "mutates both sides, silently" the criterion
originally specified, which after the fix cannot happen and would pass
for the wrong reason. The wire-level half stays an explicit obligation
of the CI `crdt`-coverage lane.
- Load-bearing Stage 2 decisions:
- **The snapshot MATERIALIZES into an ordinary buffer**, so isearch,
motion, selection and the kill ring work with no new substrate, and
"keys must not reach the child" dissolves structurally — the
transport arm keys on `is_terminal(buffer_id)` and a snapshot is not
a terminal. **The dispatch-shadow count stays at six.**
- **One serializer, not two** (Q#TC7): `copy_retained` builds a
whole-range *selection* and hands it to `copy_selection_bytes`.
- **`prune` reacts to removal rather than causing it** — it filters on
`!registry.contains(buffer_id)`, so a child exiting does NOT remove
the terminal buffer. That is why `on_removed` is a sound teardown
hook, and why a finished command's output stays readable.
- **Five bites, five different wrong implementations.** Removing
`set_round_trip_input` fails acceptance 16 **in the default
configuration** (the whole reason that pin is ungated); a naive
independently-written serializer fails all four unit pins, with the
diffs naming each drift mode (broken soft wrap, untrimmed blanks,
trailing newline); making re-invoke create a fresh buffer fails 18;
dropping the kill-with-terminal teardown fails 18; removing the
intercept fails 16b. Each failed exactly one test.
- **Review round 1 — four findings, all real, and they rhyme in pairs.**
Two P1 implementation defects and two P2 vacuous pins, all four tracing
to one root: **a name is not an identity, and a context-free readout is
not a state observation.**
- *P1 — a foreign same-named buffer was adopted and clobbered.* Snapshot
writes use `bypass_intercept`, so found-by-name adoption overwrote a
user's buffer; the reviewer reproduced "do not clobber" becoming 23
newlines. Fixed by dired's F7 rule: **ownership means "in our own
handle table"**, and a taken name yields a `<2>` variant.
- *P1 — snapshot identity was keyed by terminal NAME.*
`TerminalManager::open` uniquifies only the *derived* name, so an
explicit `name = "*same*"` lets two valid terminals share one; they
then shared a snapshot, `q` returned to the wrong terminal, and
killing either removed it. Now keyed by comparing buffer handles in an
array — `BufferIdLua` implements `__eq` but each wrapper is a distinct
table key, so **comparison works and hashing does not**.
- *P2 — the refresh pins were vacuous.* 19 compared a quiet terminal's
snapshot against itself and 18 counted buffers, so both passed with
`render_snapshot` replaced by a no-op. Now the test types a marker
into the `cat` child, requires it **absent** first, then refreshes.
- *P2 — the tail-follow pin could not observe view state.*
`manager.snapshot(buffer_id)` is context-free and always reads the
live screen, so it reported "at the tail" for a view forced to the
oldest retained row. Now read through `snapshot_for_view`'s
`at_bottom` and projected cells.
- **Four more bites, all discriminating.** Restoring adopt-by-name fails
18a *and* 18b; restoring name-keyed identity fails 18b; making
`render_snapshot` a no-op fails **both** 18 and 19 (the vacuity,
demonstrated); and forcing the view off the tail fails 20.
- **Review round 2 — one P1, and its fix retires half a named deferral.**
**Undo emptied the "read-only" snapshot.** `render_snapshot` wrote with
`bypass_intercept`, leaving ordinary undo history, and **`Buffer::undo`
reaches the rope through `ensure_writable` without ever consulting the
intercept chain** — so `C-/` *or* `M-x buffer.undo` replaced a freshly
rendered snapshot with an empty buffer. `set_round_trip_input` does not
help: it routes the key into the daemon command path, which is where
undo runs.
- **Rebinding the undo chords would NOT have fixed it**, and
`compile.lua` already says so in a comment — "command/menu undo stays
dispatchable". `*compilation*` and listview panels therefore carry the
same latent defect today.
- Fixed with `Buffer::set_generated_contents` (Lua
`pmacs.buffer.set_generated_contents`): lift `read_only`, replace
skipping intercepts, **discard history**, re-assert `read_only`. This
ships the deferred lane's two halves *as one primitive* — a bare
`set_read_only` would let a caller lock a buffer it can no longer
refresh, which is exactly why that lane was deferred. Clearing history
also stops a periodically refreshed buffer accumulating rope clones
nothing can ever pop.
- New pins: **acc16c** drives the real M-x path
(`command.invoke_interactive`), the chord, and redo, and asserts the
owner's refresh still works; **acc16b** flipped from asserting
`is_read_only()` is *false* to *true*, because the property it
described is the one that was fixed; plus three `buffer.rs` unit tests.
- Bite: restoring the `delete`+`insert` render reproduces the report
exactly — `left: Some("")` against the full snapshot — failing acc16c
and acc16b.
- **Still open:** `*compilation*` and listview remain emptiable by
`M-x buffer.undo`; the primitive they need now exists and is proven,
so the remainder is adoption plus a streaming-friendly variant.
- **Review round 3 — one P1 and two P2s, all on the round-2 primitive.**
The lesson: **a rope write is only half of an edit, and "discard
history" means whichever history the buffer actually has.**
- **P1 — the binding swallowed the edit.** `set_generated_contents`
returned `()`, so nothing called `notify_buffer_edit_to_windows`.
Two consequences, both reproduced by the reviewer: in the default
build a window showing the buffer kept a `TextView` line index
describing the *previous* contents, and the next paint indexed the
new rope with stale ranges — `assertion failed: end <= self.len()`
in `src/rope.rs`; in the CRDT build `pending_crdt_ops` stayed empty,
so replica mirrors never received the owner's write. The prior
`buf:delete`/`buf:insert` pair had done this fan-out for free.
Fixed by applying **one whole-buffer `Replace`**, returning its
`Edit`, and notifying from the binding.
- **P2 — "discard history" was false in CRDT mode.** The v0.1 stacks
are bypassed entirely there; the history lives in loro's
`UndoManager`. `read_only` stops the replay but not the retention,
which is the memory cost the contract claims to eliminate.
`UndoManager` has no `clear`, but needs none — it records only what
happens after construction, the property `CrdtState::from_bytes`
already uses to keep the seed insert out of undo. New
`CrdtState::clear_undo_history` rebinds a fresh manager to the
same doc.
- **P2 — the docs described the pre-fix architecture.** Q#TC6a said no
Lua binding sets `read_only` and round-trip input is the only guard;
the acceptance text still said `is_read_only() == false` while 16b
had been flipped to `true`; `terminal.lua`'s comment repeated the
obsolete claim. The architecture is **layered** and now says so:
rope-level read-only protects the daemon copy, round-trip input
protects the replica's optimistic mirror, and neither substitutes
for the other. Q#TC6a carries a superseded-in-part box rather than
being silently rewritten.
- New pins: **acc16d** paints the window after a *shrinking* generated
write (the stale offsets then point past the end, which is the
reported crash rather than stale pixels); **acc16e** asserts the
refresh is queued for mirrors through the real copy-mode path
(`crdt`-gated, therefore dark in CI — 16d is the half that runs);
plus a CRDT `buffer.rs` unit test that ten renders leave the
`UndoManager` with nothing recorded.
- Bites: dropping the notify panics acc16d at `rope.rs:145` and fails
acc16e with `queued: []`; dropping the `UndoManager` rebind fails
the new unit test on `can_undo`.
- **Still open:** the fan-out obligation makes `*compilation*`/listview
adoption more than a one-line swap — recorded in `COHERENCE.md` §14
alongside the undo half.
- **Review round 4 — one P2, docs only, and it is the interesting kind.**
**A fix can invalidate a test that was never written.** Criterion 17's
*bite* still described the pre-round-2 world: remove
`set_round_trip_input` and the op "mutates both sides, silently, with
no divergence to notice". True while nothing set `read_only` from Lua;
false once `set_generated_contents` did. A real-GPU test written to
that spec would hunt for a daemon-side edit that can no longer occur
and pass for the wrong reason — the specification would have leaked
the round-2 regression back in, through a test not yet built.
- Restated around **unauthorized mirror mutation plus daemon refusal =
divergence**, in all four places that carried the old claim: the
criterion, the Q#TC6a heading, the acceptance-16 doc comment, and the
bite roster. The heading's "ONLY thing" now says what it is the only
thing *for* — the replica's own mirror.
- Why round-trip input is still load-bearing rather than redundant: a
daemon refusal arrives after the frontend has already applied
optimistically and painted. It buys divergence instead of silent
agreement; it does not prevent the mutation the user sees.
- **Gate-run flake observed and scoped without overclaiming its cause.**
`cargo test --lib --features crdt` failed ~1 run in 5 on
`process::tests::setsid_escapee_is_not_reaped_and_teardown_reclaims_readers`
— `active_reader_probe` returning `None` at `process.rs:3179`
("live runtime probe"). **Pre-existing and unrelated:** this branch
does not touch `src/process.rs` (last changed by the Darwin PTY
signal-name fix), and the test passed 10/10 standalone; the observed
failures were during parallel full-suite runs. That localizes the
trigger to suite load or interaction, but does **not** distinguish
parallelism from another full-suite effect — no serial full-suite bite
was run. The leading code-path explanation is the known `drain_until`
trap: draining for `Started` also ticks, and a tick can reap the leader
before the following `active_reader_probe`. That is an inference from
the failure site and control flow, not yet a falsified root cause.
It belongs to the CI `crdt`-coverage lane for discrimination. The two
round-2 CRDT failures had no captured test names; this flake is a
plausible candidate for them, but they remain **unattributed**.
- 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.
Stage 1, the Stage 2 framing, and Stage 2A are on `main`. Framing
revision 5's three-way split of 2B was explicitly approved on
2026-07-27. **Stage 2B-1 is implemented, integrated with canonical
`main`, and awaiting its full gate result before a PR is opened.**
## Bottom-panel lane (Arc 7) — Stages 1, 2A + framing MERGED; 2B is next
Stage 1, the Stage 2 framing, and Stage 2A are all on `main`. **Stage 2B
has not started.**
- **Stage 2B-1 branch:** `bottom-panel-stage2b`, based on
`githubsucks/main` @ `c2d56ff` by merge because review had begun.
Recovery: `git fetch githubsucks && git checkout
bottom-panel-stage2b`. Everything described through the integration
checkpoint is committed and pushed; nothing depends on a worktree or
`/tmp`. No PR exists yet.
- **Ships only the v21 wire layer:** the four wire shapes, version bump,
shared cell-grid validator, and version-ladder move. It has no
producer, consumer, or capability change; `panel_capable` stays
`false`, so this slice changes no user-visible journey grade.
- **Review round 1 closed:** two P1s and one P2, all corrected at
`9b364ad`: `PanelFrame` now identifies its buffer, the transport
ratchet covers the actual attach path rather than a detached codec
assertion, and shared grid bounds have one validator.
- **Next ordering is fixed:** 2B-2 branches from `main` only after 2B-1
lands; 2B-3 branches only after 2B-2 lands. The daemon epoch machine
belongs to 2B-2; the GPU band and negotiated capability flip belong
to 2B-3.
- **Stage 2A MERGED as #177** (`main` @ `0a3fcd1`, 2026-07-26, all twelve
checks green at `8424172`, three review rounds). Branch
@ -713,19 +343,7 @@ has not started.**
`primary_document_window` returns `view.active` in every existing
configuration, so this is seam adoption that becomes load-bearing in
2B.
- **Stage 2B is approved and unstarted.** It branches from `main`, **not
stacked on 2A**, per the framing §9. Scope: protocol v21, the daemon
panel projection, the GPU band, and the negotiated `panel_capable`
flip. `docs/bottom-panel-stage2-framing.md` §7.2 carries its five
acceptance criteria (A2B-1..5) plus the reassertion of parent
criterion 52, and §8 records **no open items**, so 2B needs no further
framing round. Its sharpest trap is §5.3's three-boundary split: the
GPU `text_area_bottom` is `status_band_top`,
`geometry_capacity_bottom` and `document_text_bottom` at once, and a
blanket rewrite moves the status chrome along with the document while
still satisfying an "everything moved" assertion — hence A2B-4's
contrast form.
- Verification on the merge result: `cargo fmt --check` clean; strict
- **Stage 2A verification on its 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
@ -781,26 +399,29 @@ has not started.**
`docs/agent-handoff.md` §1; the two round lessons are in §5.
- Landed-docs follow-up merged as **#156** (`main` @ `d152120`,
2026-07-25).
- **Stage 2 framing: `docs/bottom-panel-stage2-framing.md` revision 4**,
- **Stage 2 framing: `docs/bottom-panel-stage2-framing.md` revision 5**,
on branch `githubsucks/bottom-panel-stage2-framing` (three commits,
one per revision), worktree `../pmacs-bp-stage2`, based on
one per pre-implementation revision), worktree `../pmacs-bp-stage2`, based on
`githubsucks/main` @ `ccf29e3`. Round 1 closed 2 blocking + 3 high;
round 2 closed 1 blocking + 2 high + 1 medium and decided both open
items; round 3 closed 1 blocking + 1 high + 1 medium. No open items
remain. The approved
remain. Revision 5 adds no decision; it records the approved
2B-1/2B-2/2B-3 implementation split. The
parent framing `docs/bottom-panel-framing.md` (rev 4) remains
authoritative, **including its acceptance criteria 37–55**.
- Retained, carrying nothing unmerged: branch `bottom-panel` and worktree
`../pmacs-bottom-panel`.
- **Stage 2 ships as two serial slices**, 2A landing before 2B branches:
- **Stage 2 ships as four serial implementation slices**, each landing
before the next branches:
**2A** = classified §1.3 census routing + `paint_frame` per-window
painter extraction (with the active-window auto-scroll preparation), no
protocol change; **2B** = protocol **v21**
protocol change; **2B-1** = protocol **v21**
(`InstanceMessage::PanelFrame` plus
`FrontendEvent::{FrontendCellGeometry, PanelResizeRows, PanelPointer}`,
gated both directions, each extended enum byte-pinned on its own
previous final variant), daemon panel projection, the GPU band, and the
negotiated `panel_capable` flip. Stage 3 is the adopter default flip.
previous final variant); **2B-2** = daemon panel projection and epoch
machine; **2B-3** = the GPU band and negotiated `panel_capable` flip.
Stage 3 is the adopter default flip.
- **Correction — this entry previously mis-stated the census contract.**
It is **not** "route every consumer through `primary_document_window`".
Q#BP14 classifies the 23 reads into four classes and routes only the
@ -883,6 +504,24 @@ git worktree add --track \
## Closed since the last snapshot
- **Terminal configuration + copy mode arc — BOTH STAGES MERGED, lane
removed.** Stage 1 **#173** (`main` @ `cf54270`, one review round) and
Stage 2 **#178** (`main` @ `fe8b8ba`, **four review rounds**, twelve
checks green on head `1b44c69` — verified by `head_sha`, not by the
check summary), both 2026-07-26, both with no protocol change.
Approved framing: `docs/terminal-config-and-copy-mode-framing.md` rev
4, committed as the first commit of Stage 1's branch; its Q#TC6a
carries a superseded-in-part box rather than a silent rewrite. Durable
facts moved to `docs/agent-handoff.md` §1 (the arc bullet) and §4 (the
`set_generated_contents` invariant) per rule 3 below, and to
`COHERENCE.md` §14. **Stage 2 ships eight of nine criteria and the
missing one is named** — criterion 17 needs a real GPU frontend, so it
waits on the `a37` footing; the handoff records what it must assert.
Branches `githubsucks/terminal-config` and
`githubsucks/terminal-copy-mode` with worktrees
`../pmacs-terminal-config` and `../pmacs-terminal-copy-mode` are
retained. The gate-run flake found while gating #178 moved to the CI
`crdt`-coverage lane above, which owns its discrimination.
- **Dired Stage 1 (the directory view) — MERGED as #165** (`main` @
`c8ec8f3`, 2026-07-25, after one review round). pmacs has a directory
surface: `C-x d` / `C-x C-j`, one read-only buffer per directory named
@ -932,6 +571,15 @@ git worktree add --track \
reproduces in-process and so is not the GUI/TUI asymmetry; and a geometry
change appearing to clear the visible screen, which reproduces pre-fix).
Branch `gpu-terminal-input` and worktree `../pmacs-gui-term-input` retained.
**Its landed-doc pair MERGED as #168** (`main` @ `1b6a084`,
2026-07-26): #166 recorded as landed, the CI `crdt`-coverage gap
measured (**264 tests dark workspace-wide**, 177 in the library — a
reading taken at `1b6a084` and kept here only as history. **The CI
`crdt`-coverage lane above is the authority for the live figure**;
do not quote this one forward), the
vterm audit corrected — "only 3 of 9 acceptances drive a real daemon"
was optimistic; without the frontend binary the honest number is
**2** — and the a37 findings folded into the coverage lane.
- **Inline-math slice — MERGED as #158** (`main` @ `5aa9044`,
2026-07-25). Detect → parse → layout → draw for `$…$`, entirely inside
`pmacs-gpu`, no protocol change. Verified by the user's manual pass on

253
docs/agent-handoff.md
View File

@ -1,9 +1,15 @@
# Agent handoff — cross-machine continuity
**Last updated: 2026-07-26, after Lean 4 Stage 4a (#179) — the typed-edit
**Last updated: 2026-07-27, after Journey Stage 1a (#182) — the
directory-open seam and golden-journey ratchet, incorporating terminal
configuration + copy mode (#180) — and after terminal copy mode (#178) — `C-c C-t`
materializes a terminal's whole retained range into an ordinary buffer,
plus `Buffer::set_generated_contents`, the first genuinely immutable
generated-buffer write path — and its landed-doc pair (#168); following
Lean 4 Stage 4a (#179) — the typed-edit
consumer chain — and bottom-panel Stage 2A (#177), the classified census
routing that makes every Projection-class consumer ask
`primary_document_window`; following the bottom-panel Stage 2 framing
`primary_document_window`; the bottom-panel Stage 2 framing
(#175), terminal configuration Stage 1 (#173) — profiles, scrollback, a
per-terminal configurable escape key, and the `C-c t` opening binding —
Lean 4 stages 3a and 3b (#167, #170), pmacs' first Lean language server;
@ -35,9 +41,13 @@ 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-26)
## 1. Where the project stands (2026-07-27)
- `main` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel Stage 2A
- `main` @ `c2d56ff` (Journey Stage 1a #182, incorporating terminal
configuration + copy mode #180, atop Lean 4 Stage 4b #181, the dired
Stage 1 landed docs #169 and the PTY-terminate diagnostic #176,
terminal copy mode #178, the GPU-terminal-input landed docs #168, Lean 4 Stage 4a
#179, bottom-panel Stage 2A
#177, the bottom-panel Stage 2 framing #175, terminal configuration
Stage 1 #173, Lean 4 Stage 3b #170, Stage 3a #167, the CRDT undo repro
#157, the inline-math landed-doc refresh #172, the bottom-panel
@ -54,11 +64,100 @@ commands, read `docs/active-work.md` immediately after this file.
standard new work is evaluated against. Per `CLAUDE.md`, **every new
framing doc must state its coherence impact** — journey steps touched,
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
attribution. Its §2 grades the golden journey; **Journey Stage 1a
moved that grade off "broken at step 3"** — see the arc bullet below.
- **Journey arc (P1) — Stage 1a LANDED**
(`docs/journey-stage1a-framing.md`). `pmacs .` opens a directory
instead of exiting 1, on **one** path: `resolve_target_buffer` gained a
`ResolvedTarget::Directory` arm *ahead* of the load, `EditorState::open`
became a caller of it rather than a parallel implementation, and the
daemon/GPU bootstrap shares the same arm. Which surface handles a
directory is the `path.open-directory` chain with dired as a
replaceable fallback slot. `tests/journey_acceptance.rs` is the new
cross-subsystem ratchet (steps 2, 3, 5 seeded; **stages add rows, none
removes them**). No protocol change.
- **A hook a builtin subscribes to can never be first-claimant-wins
for users.** `HookRegistry::add` only appends and builtins load
before `init.lua`, so a dired subscription would always claim before
any user listener. That is why dired is a *slot*
(`pmacs.path.directory_handler`) and not a subscriber — and why
clearing the slot has to leave startup succeeding with a status,
not exiting 1.
- **A raise and a `false` are indistinguishable in `proceed`.**
`run_short_circuit` returns `proceed = false` for both; only
`HookOutcome.errors` separates them, and it decides whether to
*report*, not whether to fall back. Getting this backwards produces a
fallback that runs after a user's resolver crashed mid-handling.
- **The listing is async; the bootstrap is synchronous.** The whole
post-await commit therefore runs against a destination captured at
request time (`pmacs.window.commit_to`), which preflights every
precondition *before* invoking the callback — dired mutates handle
state, `prev`, and paint long before it reaches anything that could
refuse, so validating at display time is four mutations too late.
Awaiting inside a commit is refused: a yield would restore the scope
while the coroutine is still parked.
- **The scope swaps `core.active_frontend`, not just an override** —
`pmacs.window.buffer()`'s no-arg arm reads the ambient active buffer
directly, so dired's `prev` capture would otherwise follow whatever
frontend happened to be dispatching. The override *also* exists, and
is load-bearing in exactly one case: a commit reached from inside an
interactive command, where the origin would otherwise outrank the
ambient value. Bite-testing found N4 green without it.
- **`replace_active_buffer` does not drop the startup scratch buffer**,
despite its doc comment having claimed so for as long as it has
existed. Its body is one `switch_active_buffer` call. The comment is
corrected here; changing the lifetime is separate work.
- Stage 1b is the named remainder: compile binding + Cargo defaults,
LSP spawn guidance, welcome buffer.
- **Terminal configuration + copy mode arc — COMPLETE**
(`docs/terminal-config-and-copy-mode-framing.md` rev 4; Stage 1 #173,
Stage 2 #178; no protocol change in either, still v20). Stage 1 ships
profiles, scrollback, a per-terminal configurable escape key and the
`C-c t` opener; Stage 2 ships copy mode — `M-x terminal.copy-mode` /
`C-c C-t`.
- **The snapshot MATERIALIZES into an ordinary buffer.** That is the
arc's organizing decision: isearch, motion, selection and the kill
ring work with no new substrate, and "keys must not reach the child"
dissolves structurally, because the transport arm keys on
`is_terminal(buffer_id)` and a snapshot is not a terminal. **The
dispatch-shadow count therefore stays at six.**
- **`prune` reacts to buffer removal rather than causing it** — it
filters on `!registry.contains(buffer_id)`, so a child exiting does
**not** remove the terminal buffer. That is what makes `on_removed` a
sound teardown hook, and why a finished command's output stays
readable.
- **Ownership means "in our own handle table", never found-by-name**
(dired's F7 rule, re-learned here): snapshot writes use
`bypass_intercept`, so adopting a same-named foreign buffer clobbers
user data. Snapshot identity is keyed by **comparing buffer handles
in an array** — `BufferIdLua` implements `__eq` but each wrapper is a
distinct table key, so comparison works and hashing does not.
- **Profiles are a raw Lua table**, joining `pmacs.lsp.config` and
`pmacs.pair.sets`, because `ConfigValue` is four scalars with no
table kind. The two open-time settings resolve through the **global**
chain (they are read before the identity buffer exists); only
`terminal.escape-key` resolves per buffer, and its cache lives on
**`TerminalSession`** so its lifetime is the terminal's —
`value_epoch` alone is not a sufficient key, because it does not
advance when focus moves between terminals holding different
buffer-local values.
- **Criterion 17 is deliberately unpinned, and its bite is now stated
correctly.** A real semantic frontend proving neither copy is mutated
needs the actual GPU binary (the optimistic apply exists only in
`pmacs-gpu/src/main.rs`; the headless `SemanticClient` has no
optimistic path), i.e. the `a37` footing §5 warns about. After
`set_generated_contents` the eventual test must look for
**unauthorized mirror mutation plus daemon refusal — divergence**,
not the "mutates both sides silently" the criterion originally
specified, which can no longer happen and would pass for the wrong
reason. *A fix can invalidate a test that was never written.*
- 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 such probes must **count
occurrences rather than test presence**, because a single-character
probe collides with the child's own banner text.
- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b, 4a, 4b ALL LANDED**
(`docs/lean4-mode-framing.md`; #160, #161, #167, #170, #179, #181). 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
@ -101,9 +200,10 @@ commands, read `docs/active-work.md` immediately after this file.
config swap invalidates. The durable lesson is to heal at
**consumption** — the point where a stale record is handed out — not
at the moment of the swap.
- **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
- **Stage 4a (the typed-edit consumer chain) MERGED as #179**
(branch `lean4-stage4a-typed-edit-chain`, framing rev 8; it is part
of the main anchor above). 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
@ -117,10 +217,51 @@ commands, read `docs/active-work.md` immediately after this file.
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`.
- **Round 8's durable lesson: `run_all_must_succeed` does NOT abort
the fan-out.** `src/hook.rs:332` collects each callback's error and
continues to the remaining subscribers, marking only the run
failed — so an uncontained throw inside a hook subscriber does not
stop `lsp.lua` from flushing didChange. Two framing revisions
asserted the opposite to justify a `pcall`. The guard was right and
the reason was wrong, and by the time review caught it the wrong
reason had been copied into a module comment, an acceptance
criterion, a test comment, and the ledger. **Correct the source a
rationale derives from, not only the sites that quote it.**
- **Stage 4b (the Unicode input method) MERGED as #181**
(framing rev 9): a vendored
1,855-entry table generated from `leanprover/vscode-lean4@17d1d08`
by `scripts/regen-lean-abbrev`, plus a consumer registered on the
Stage 4a chain at priority 50, ahead of pairing. **A consumer
cannot both edit and let a later consumer act on the same
keystroke**: the chain hands each consumer a copy of the record made
before any consumer ran, so an edit invalidates every copy still to
be used. The expansion therefore runs on a SECOND
`buffer.after-edit` subscriber after the chain — which is how a
pair character that terminates an abbreviation still pairs
(`\alp(` → `α()`). And **deferring work past a fan-out means
owning which fan-out it belongs to**: these fan-outs NEST, so a
consumer between the expander and pairing that calls
`pmacs.hook.run` re-enters the deferred subscriber while the outer
chain is still mid-list, and the count that recognises this has to
come from a MINIMUM-PRIORITY consumer — the expander is optional
(a claim can stop the chain first) and a subscriber beside the
deferred one is too late (the nested fan-out finishes inside the
outer chain's subscriber). Its other durable facts:
the table must stay an ORDERED SEQUENCE (equal-length ties resolve
by source declaration order, which a `pairs`-iterated map cannot
express); a generator round-trip check must re-read the BYTES ON
DISK, because comparing in-memory strings cannot see an encoding
applied by the write itself; and an expansion that SHRINKS the
buffer must place the point explicitly, or every later self-insert
is silently rejected and the editor looks dead.
- **Round 9 corrected three approved acceptance criteria** by
simulating the state machine over all 1,855 entries rather than
re-reading the prose. Four review rounds over the text had not
found them, because each named an example that reads as obviously
right and is wrong only against the data.
- Remaining: 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
@ -319,12 +460,14 @@ commands, read `docs/active-work.md` immediately after this file.
required GPU 152; initial-target 14 CRDT; all three vterm suites; folding
Stage 2 48. All 12 CI checks green at merge.
- **Stage 2 (the GPU panel band) is FRAMED** —
`docs/bottom-panel-stage2-framing.md`, four review rounds, no open
items. It takes protocol **v21** and ships as two serial slices:
**2A** classified census routing + per-window painter extraction (no
wire change), then **2B** the wire, the daemon projection, the band,
and the negotiated `panel_capable` flip. Parent acceptance 37–55
remains authoritative. Stage 3 is the adopter default flip.
`docs/bottom-panel-stage2-framing.md` rev 5, four review rounds, no
open items; the rev-5 implementation split was explicitly approved
2026-07-27. It takes protocol **v21** and ships as four serial
implementation slices: **2A** classified census routing +
per-window painter extraction (no wire change), **2B-1** the wire,
**2B-2** the daemon projection and epoch machine, then **2B-3** the
GPU band and negotiated `panel_capable` flip. Parent acceptance
37–55 remains authoritative. Stage 3 is the adopter default flip.
- **The §1.3 census is CLASSIFIED, not uniformly redirected.** Only the
Projection class (#1–#12, #21–#22) routes through
`primary_document_window`; focus/input (#13–#15, #23), focus chrome
@ -951,6 +1094,72 @@ before trusting them:
## 4. Substrate invariants (do not undo; tests enforce most of these)
**Generated buffers: `Buffer::set_generated_contents` is the ONE
authorized write** (terminal copy mode #178) — lift `read_only`, replace
via a single whole-buffer `Replace` skipping intercepts, discard history,
re-assert `read_only`, and **return the `Edit`**. Three things make it a
unit rather than a convenience:
- **An intercept is not read-only.** `Buffer::undo` reaches the rope
through `ensure_writable` and never consults the intercept chain, so an
intercept-only "read-only" buffer is emptied by `M-x buffer.undo`.
Rebinding the undo *chords* buffer-locally does **not** close it —
`compile.lua`'s own comment says so ("command/menu undo stays
dispatchable"). Only rope-level `read_only` does.
- **A bare `set_read_only` would be worse than nothing**, because it also
refuses the owner's refresh — the operation such buffers exist for.
That is why the pairing, not the setter, is the primitive. There is
deliberately no Lua `set_read_only`.
- **A rope write is only half of an edit.** The returned `Edit` must be
fanned out (`notify_buffer_edit_to_windows`, which also queues the
daemon-origin CRDT op). Skip it and a displaying window keeps a
`TextView` line index describing the previous contents — the next paint
indexes the new rope with stale ranges and trips
`assertion failed: end <= self.len()` — while replica mirrors never
import the write at all.
History clearing is load-bearing twice (nothing can pop entries
`read_only` makes unreachable, so they leak), and must clear **whichever
history the buffer has**: the v0.1 stacks are bypassed in CRDT mode, where
it lives in loro's `UndoManager`. That has no `clear`, and needs none — a
manager records only what happens after construction, so
`CrdtState::clear_undo_history` rebinds a fresh one to the same doc.
**Not yet adopted — the inventory is four writer mechanisms covering
five buffers.** *Every remaining intercept-protected writer* uses the
older idiom: an erroring intercept plus `set_round_trip_input`, written
through `bypass_intercept`, with the rope left writable. All are
emptiable by `M-x buffer.undo`:
| writer | buffers | shape |
|---|---|---|
| `builtin/runtime/listview.lua:60-61` | every listview panel | delete-all + insert |
| `builtin/runtime/compile.lua` (`ensure_slot`) | `*compilation*`, `*shell-command*` | **append** per output batch |
| `builtin/commands/default.lua:869` | `*search-results*` | reset per query, then **append** per match batch |
| `builtin/runtime/dired.lua:371` | every dired buffer | whole-buffer replace |
**Do not read `ensure_slot` as covering the search panel** — it serves
`*compilation*` and `*shell-command*` only (`compile.lua:1090,1125`).
`*search-results*` is an independent panel with its own intercept,
round-trip mark and writes, and `compile.lua` names it only in a
predicate. Nor is the scope "every generated buffer": `*workers*`,
`*help*` and `*buffer-list*` are generated too but do not use this
idiom, and the REPL package's intercept
(`builtin/packages/repl/init.lua:187`) is an op-filtering editing
policy, not a read-only panel — neither group belongs to this lane.
Adoption is not a one-line swap. It inherits the fan-out obligation, and
the three appending buffers need a **streaming variant** of the
primitive; listview and dired already write whole-buffer replaces and
are the cheap half. Recorded in `COHERENCE.md` §14.
**And it does not replace `set_round_trip_input`.** The protection is
layered across two copies: rope-level `read_only` refuses the op at the
daemon; round-trip input stops a semantic frontend applying
optimistically to its **own mirror**, which a daemon-side refusal cannot
reach — the refusal arrives after the frontend has already painted, so it
buys divergence, not prevention.
**Command boundaries (Arc 2 kill-ring substrate)** —
`EditorCore.command_history: HashMap<FrontendId, CommandBoundary{this, last}>`,
per frontend. Rotate on: keybound command, self-insert, menu invoke,

8
docs/bottom-panel-stage2-framing.md
View File

@ -1,8 +1,8 @@
# Bottom panel Stage 2 — the GPU panel band (framing)
**Revision 5 — 2A merged, 2B in progress. Ground truth: canonical
`main` @ `42025e4`, protocol v20 on `main` and v21 on
`bottom-panel-stage2b`, 2026-07-26.** Revisions 1–4 were
**Revision 5 — APPROVED 2026-07-27; 2A merged, 2B-1 in progress.
Ground truth: canonical `main` @ `c2d56ff`, protocol v20 on `main` and
v21 on `bottom-panel-stage2b`.** Revisions 1–4 were
pre-implementation; rev 5 records the three-way slice of Stage 2B
(§0.0, §7.2, §9) after its first slice was already built.
@ -885,7 +885,7 @@ suites: the shared validator and the wire enums are exactly the kind of
change whose breakage surfaces in a consumer rather than at its own
definition.
Gates for both: the standing suite from `CLAUDE.md`, plus the **touched
Gates for each slice: the standing suite from `CLAUDE.md`, plus the **touched
acceptance suites named explicitly** — the standing rule is to run the
suites a change touches, and "standing suite" does not name them:

20
docs/gpu-initial-target-framing.md
View File

@ -282,8 +282,17 @@ observers; they are not the transport implementation.
- Any `NotFound` from the initial load creates an empty path-backed buffer,
including when a parent is currently absent; save-time errors remain
save-time errors, matching local `pmacs FILE`.
- `PermissionDenied`, `IsADirectory`, invalid path bytes at the OS boundary,
and other non-`NotFound` errors fail startup.
- `PermissionDenied`, invalid path bytes at the OS boundary, and other
non-`NotFound` errors fail startup.
- **`IsADirectory` is superseded by Journey Stage 1a**
(`docs/journey-stage1a-framing.md`). A directory no longer reaches the
load at all: `resolve_target_buffer` answers `ResolvedTarget::Directory`
ahead of it, so a directory target now *succeeds*, dispatching the
`path.open-directory` chain and replying `Opened`. Deliberate
supersession, not drift — the whole point of that stage is that
`pmacs .` must not exit 1, and a daemon/GPU bootstrap that still failed
would leave the two entry points disagreeing about the same argument.
Non-directory failures are unchanged.
- The buffer display name may use `Path::display()` and therefore replacement
characters; this must never replace the raw backing path used for dedup,
load, or save.
@ -550,12 +559,17 @@ process behavior.
9. **New file:** a nonexistent target produces an empty snapshot, `[new file]`
status/path identity, accepts an edit/save through the real session, and
creates the requested file under the launcher cwd—not the daemon cwd.
10. **Open error:** a directory/permission-denied target returns a specific
10. **Open error:** a permission-denied target returns a specific
failure before ready/window creation and makes root fail. The daemon shuts
down that failed session's socket; a client that lingers or sends another
event cannot reach uninstalled session state. An existing daemon remains
connectable; a pre-existing frontend's active buffer and contents remain
unchanged.
**Amended by Journey Stage 1a:** the *directory* case is deliberately
superseded and moved to the success path — see Q#GT6. A directory
target now reaches ready and the document window shows dired, pinned
by `initial_target_directory_reaches_ready` and its two siblings in
`src/daemon.rs`. Permission-denied is unchanged and still fails.
11. **Dedup preserves unsaved edits:** frontend A opens and modifies a file
without saving; target-launch frontend B opens the same normalized path and
receives A's authoritative unsaved text with the same `BufferId`, not disk

1082
docs/journey-stage1a-framing.md Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -46,7 +46,7 @@ during a rebase.
## 0.1 Revision history
Revision 1 — initial. Current revision: **8**.
Revision 1 — initial. Current revision: **12**.
### Round 1 (rev 1 → rev 2)
@ -503,6 +503,110 @@ documentation cleanups.
others — matching §2.11 and Q#LN11.
3. **§9.1's revision label was stale.** It now names rev 8.
### Round 9 (rev 8 → rev 9)
Found during Stage 4b implementation, by simulating Q#LN22's state
machine over all 1,855 vendored entries and re-reading upstream's
`TrackedAbbreviation.ts` and `AbbreviationProvider.ts` at `17d1d08`.
**Three acceptance criteria named examples that the real table
contradicts** — every one of them written from what the abbreviation
*looks* like rather than from whether the table makes it eager.
1. **Acceptance 41 was false.** `\to` does not expand eagerly: `to` is a
proper prefix of `top`, `to0`, `toa` and others, so upstream's
`isAbbreviationUniqueAndComplete` is false and `to` is not among the
1,550 eager keys. The criterion now uses `\alpha`, which has no
extension, and additionally pins that `\to` alone does **not**
expand — the false half is worth an assertion because it reads as
correct until the table is consulted.
2. **Acceptance 42 was false.** `\zzzz` + space yields `ζzzz `, not
literal text: `z` opens a pending abbreviation (`ze`, `zeta`,
`zsqrtd`) and the second `z` finishes it. Exactly six printable
characters open no key — `$ % , ; @ W` — and the criterion now uses
`\WWWW`.
3. **Acceptance 38's undo claim was false for its own example.**
`alpha` is eager, so `\alpha` expands before the space is typed and
the space is a separate edit; one undo removes the space rather than
restoring `\alpha `. The criterion now states the finish path and the
eager path separately, since "one expansion is one undo step" is true
of both while the text an undo restores is not.
The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were
errors in the examples chosen to pin it, which is why a simulation over
the real data found them and four review rounds over the prose did not.
### Round 10 (rev 9 → rev 10)
Review of the Stage 4b implementation. Three defects in the expander,
all of them about what happens AROUND the expansion rather than about
resolving an abbreviation, plus one stale count.
1. **A pair character that terminates an abbreviation never reached
auto-pairing.** Q#LN22 already said the terminator is not claimed;
the implementation claimed it whenever an expansion succeeded, so
`\alp(` gave `α(`. Not claiming is necessary and not sufficient —
the chain hands each consumer a copy of the record made before any
consumer ran, so expanding inside the chain invalidates the copy
pairing is holding and the closer is lost anyway. Q#LN22 now
specifies the deferred subscriber and the span that stops before the
terminator; acceptance 45j pins all three failure modes.
2. **Post-insert point motion was mistaken for a valid pending span.**
The relevance check compared buffer and window but not
`ed.cursor() == rec.post_cursor`, so a redefined self-insert that
inserts and then moves the point still expanded — and teleported the
point back. Pairing has made this three-part check since #110.
Acceptance 45k.
3. **Cursor placement could move the wrong buffer.** A buffer intercept
may switch buffers during `buf:replace`; the unguarded `goto_byte`
afterwards moved the switched-to buffer's point. `repair_cursor` is
the precedent. Acceptance 45l.
4. **The coherence census contradicted itself** — nine settings in one
paragraph, eight three paragraphs below.
Acceptance 45m was added with them: the expansion now runs on its own
`buffer.after-edit` subscriber, which is a new instance of Q#AP7 and
was unpinned.
### Round 11 (rev 10 → rev 11)
One P1 in the round-10 fix, and one stale comment.
1. **The deferred expansion was not tied to the fan-out that queued
it.** `buffer.after-edit` fan-outs nest — the typed-edit contract
supports a consumer calling `pmacs.hook.run` — and a nested run
re-enters the expander's subscriber while the OUTER chain is still
mid-list. A consumer at priority 75 running one nested fan-out made
`\alp(` yield `α(` again: the nested pass expanded, and outer
pairing then resumed with a record the replace had invalidated.
Round 10's own failure mode, reached through re-entrancy instead of
claiming. Q#LN22 now specifies matching chain invocations against
expander invocations so only the outermost pass expands; acceptance
45n pins it.
2. **A test comment still described the discarded span design** — it
said the expansion replaces the span "INCLUDING the terminator",
which round 10 deliberately stopped doing. The behaviour it asserts
was correct; only the explanation was stale.
### Round 12 (rev 11 → rev 12)
One P1: round 11's counter was in the wrong place.
1. **The nesting count lived in the expander, which is optional.** A
consumer at a lower priority can claim and stop the chain before the
expander runs, while that fan-out's deferred-expansion subscriber
still runs — so the nested pass went uncounted, looked like the
outermost one, expanded early, and outer pairing resumed with an
invalidated record. `\alp(` gave `α(` again. The count now comes
from a no-op consumer at the minimum priority, which runs first in
every chain invocation that reaches any consumer; acceptance 45o
pins the short-circuit path that 45n does not reach.
The pattern across rounds 10–12 is worth naming: each fix was correct
about the failure it was shown and wrong about the boundary of the
mechanism it relied on — the chain's copy semantics, then its
re-entrancy, then its short-circuit. **A queue that outlives the thing
that filled it needs to name that thing, not approximate it.**
## 1. What ships
Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
@ -1686,8 +1790,9 @@ reconstruction of it:
- A subsequent self-insert `c` is claimed iff at least one key has
`text .. c` as a prefix; then `text = text .. c`. If it is also
uniquely-and-completely matching (one of the 1,550), expand now.
- If no key extends `text .. c`, expand `text` **first**, then let `c`
land normally — the chain does *not* claim `c`.
- If no key extends `text .. c`, `c` TERMINATES the abbreviation: the
chain does *not* claim it, and the expansion of `text` is
**deferred** until after the chain has run (round 10; see below).
- **A terminating `c` that is itself `\` is then reprocessed as a new
leader**, opening a fresh pending abbreviation at its position. This
is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6
@ -1701,6 +1806,69 @@ reconstruction of it:
broken by source rank, unmatchable tail appended (`\alp7` → `α7`).
- `$CURSOR` is stripped from the symbol and its index becomes the point.
**The expansion is deferred past the chain, and its span stops before
the terminator** (round 10). "Not claiming the terminator" is necessary
and not sufficient: a pair character is a legal terminator (`\alp(` must
give `α()`), and the chain hands every consumer a *copy* of the record
made before any consumer ran. So expanding inside the chain and then
declining leaves auto-pairing holding offsets the replace has already
invalidated — pairing declines and the closer is silently lost, which a
probe confirmed. Claiming the terminator instead suppresses pairing
outright. Neither is recoverable from inside the chain.
The expander therefore records the pending expansion and performs it on
its **own `buffer.after-edit` subscriber**, registered after
typed_edit.lua's and before lsp.lua's. A claim by any consumer stops the
chain but not a separate subscriber — which is the point, since pairing
claims the terminator it reacts to. The replaced span covers the leader
and the typed text only; whatever pairing did lands after it and
survives untouched. One undo restores the same text either way, because
the terminator was always its own insert.
**The deferred expansion must belong to its own fan-out** (round 11).
`buffer.after-edit` fan-outs NEST — Q#AP9 and typed_edit.lua's header
both say so explicitly, and a consumer may call `pmacs.hook.run`. A
nested run re-enters every subscriber, including the deferred
expansion's, while the OUTER chain is still walking its consumer list
and pairing has not yet seen the terminator. A nested pass that
performed the expansion would reproduce the exact bug deferring exists
to fix, reached through the chain's documented re-entrancy seam instead
of through claiming.
The nesting level is counted by a **no-op consumer registered at the
minimum priority**, matched off in the expander's subscriber. Only the
outermost pass expands; a nested one leaves the expansion queued. No
new seam in typed_edit.lua, which is merged substrate.
Where the count lives is the whole difficulty, and two plausible places
are both wrong (round 12):
- **A subscriber registered beside the expander's is too late.** The
entire nested fan-out completes inside the OUTER chain's subscriber,
before any subscriber registered after it runs.
- **The expander itself is optional.** A lower-priority consumer may
claim and stop the chain before the expander is reached, so a nested
pass would go uncounted while its `run_deferred` still ran — and
would then look like the outermost one.
A minimum-priority consumer runs first in every chain invocation that
reaches any consumer at all. Its guarantee is exactly the ordering
contract the chain already rests on, and it degrades safely: the only
thing that can skip it is a claim ahead of it, which skips the expander
too, so nothing is queued in that fan-out either.
Two guards this exposes, both of which pairing already carries:
- The relevance check is **three-part**, not two: buffer, window, **and
`ed.cursor() == rec.post_cursor`**. A redefined self-insert can insert
the completing character and then move the point, and expanding over a
span the user has left teleports them back into it.
- Cursor placement after the replace is **context-guarded**. A buffer
intercept may switch window or buffer while `buf:replace` runs; an
unguarded `goto_byte` then moves the point of a buffer that has
nothing to do with the expansion. `pair.lua`'s `repair_cursor` is the
precedent.
**Ownership is per frontend, not per buffer** (§2.11). The key is
`(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still
match `rec.window` for the state to be usable — a frontend that moved
@ -2452,12 +2620,25 @@ criterion 46 requires to stay byte-identical.
**Stage 4b — the Unicode input method**
38. `\alpha` + space yields `α ` — the space lands first and the
expansion runs in the following `buffer.after-edit`, so the
terminator is **retained**, not consumed. The expansion is a single
undo step: one undo restores `\alpha ` (with its space), not
`\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be
true only if the terminator were swallowed.
38. **Terminators are retained, and one expansion is one undo step —
but which text an undo restores depends on the path.** Rev 8 stated
a single rule here and it is wrong against the real table, because
it assumed `\alpha` takes the finish path when `alpha` is in the
1,550-key eager set (round 9; see 41).
- *Finish path.* `\alp` + space yields `α `: the space lands first
and the expansion runs later in the same `buffer.after-edit`
fan-out, so the terminator is **retained**, not consumed. It sits
OUTSIDE the replaced span, which covers only the leader and the
typed text (round 10) — the observable text and the post-undo
text are the same either way, because the terminator was its own
insert. One undo restores `\alp ` — with its space, not `\al`.
Rev 6 wrote the post-undo text without the terminator, which
would be true only if the terminator were swallowed.
- *Eager path.* `\alpha` yields `α` with no terminator typed, and a
following space is a **separate** edit. One undo removes the
space; a second restores `\alpha`. Asserting the finish-path undo
text here would fail, which is the trap this split exists to
record.
39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR`
placeholder.
40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is
@ -2467,9 +2648,21 @@ criterion 46 requires to stay byte-identical.
only completed expansions rather than pending extensions — **both
failure modes must be shown**, since they are distinct bugs with the
same symptom.
41. `\to` yields `→` eagerly on uniqueness, with no terminator typed.
42. A prefix with no match (`\zzzz` + space) is left as literal text; no
edit is made.
41. **Eager expansion on uniqueness**, with no terminator typed:
`\alpha` yields `α` the moment the final `a` lands. Rev 8 used `\to`
here and that is false against the real table (round 9): `to` is a
proper prefix of `top`, `to0`, `toa` and others, so
`isAbbreviationUniqueAndComplete` is false and `to` is **not** in
the 1,550-key eager set. `\to` alone stays `\to`; `\to` + space
yields `→ ` by the finish path. Both are asserted, because the
wrong one reads as correct until the table is consulted.
42. A prefix that opens no key at all — `\WWWW` + space — is left as
literal text and **no edit is made**. Rev 8 used `\zzzz`, which
expands (round 9): `z` opens a pending abbreviation because `ze`,
`zeta` and `zsqrtd` exist, and the second `z` finishes it, giving
`ζzzz `. Exactly six printable characters open no key: `$ % , ; @
W`. Bites against an implementation that treats "no complete match"
as "no pending state".
43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion
hook, this asserts what pmacs can actually detect: after `\alp`, an
explicit `goto_byte` elsewhere followed by typing `h` inserts a
@ -2544,6 +2737,49 @@ criterion 46 requires to stay byte-identical.
`$CURSOR` more than once;
- the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`,
`n`, `setminus`, and the tie cases from 45h.
45j. **A pair character that TERMINATES an abbreviation still pairs**
(round 10). `\alp(` yields `α()` with the point between the pair.
Bites three ways, all of which produce different wrong answers:
claiming the terminator gives `α(`; expanding inside the chain and
then declining also gives `α(`, because the replace invalidates the
record copy pairing is holding; and pairing running first gives
`\alp()` unexpanded. Criterion 40 is the same collision from the
other side, and passing it says nothing about this one.
45k. **The relevance check is three-part.** A redefined
`buffer.self-insert` that inserts the completing character and then
moves the point must not expand: `\alph` + `a` under such an
override leaves literal `\alpha` with the point where the command
put it. Bites against checking only buffer and window — the
expansion would otherwise teleport the point back into a span the
user has left.
45l. **Cursor placement is context-guarded.** A buffer intercept that
switches buffers during `buf:replace` must not have the
switched-to buffer's point moved. Bites against an unguarded
`goto_byte`, which translates the LEAN buffer's pre-edit point
through the LEAN buffer's edit and applies it to whatever is
ambient.
45m. **Q#AP7 for the deferred subscriber.** The expansion runs on a
second `buffer.after-edit` subscriber, so it inherits pairing's
flush-ordering obligation: no `didChange` may ever carry the
unexpanded text. Pinned with the `sighelp` fake server and `(` as
the trigger — the flush carrying the terminator carries `α()`.
Falsified by loading lean_input.lua after lsp.lua.
45n. **A nested fan-out must not expand early** (round 11). A consumer
registered BETWEEN the expander and pairing that calls
`pmacs.hook.run("buffer.after-edit")` once still yields `α()` for
`\alp(`. Bites against a deferred slot consumed by whichever
fan-out happens to reach it: the nested pass would expand, and the
outer chain would then hand pairing a record the replace had
invalidated — the round-10 failure again, through the chain's
documented re-entrancy seam rather than through claiming.
45o. **A nested fan-out that never reaches the expander must not
expand early either** (round 12). Same shape as 45n, but the nested
pass is short-circuited by a consumer at priority 25 that claims
when the record is nil — so the expander never runs on it. Bites
against counting fan-outs in the expander, which is optional by
construction: the uncounted nested pass looks outermost, expands,
and outer pairing resumes with an invalidated record. 45n passes
against that bug, which is why both are pinned.
45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` —
`f<` and `f>` are both length 2, and `f<` is declared first. Same
for `\"` + space → `Ä`, first of eleven equal-length candidates.
@ -2698,7 +2934,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from
languages other than Lean, and §4's rule is what keeps them out of a Lean
PR.
### 9.1 Coherence impact — stages 4a and 4b (rev 8)
### 9.1 Coherence impact — stages 4a and 4b (rev 12)
**Sections served.** §6 (interaction islands) primarily, and in the
*preventing* direction rather than the fixing one — see below. §11

20
docs/terminal-config-and-copy-mode-framing.md
View File

@ -564,11 +564,21 @@ additive, on its own binding, and does not replace scroll-and-select.
would replay, and it stops a periodically refreshed buffer accumulating
rope clones that `read_only` guarantees nothing can ever pop.
**What remains of the lane:** `*compilation*` and listview panels still
rely on intercept-plus-round-trip and are still emptiable by
`M-x buffer.undo`. The primitive they need now exists and is proven, so
the remaining work is adoption plus a streaming-friendly variant
(`*compilation*` appends rather than replacing wholesale).
**What remains of the lane — four writer mechanisms over five
buffers**, not the two this section first named (round 5 found the
inventory short; round 6 found the corrected version misattributing
the search panel). Every remaining intercept-protected writer still
relies on intercept-plus-round-trip over a writable rope, and every one
is still emptiable by `M-x buffer.undo`: listview panels
(`listview.lua:60-61`); `compile.lua`'s `ensure_slot`, which serves
`*compilation*` and `*shell-command*` — **not** `*search-results*`,
which `compile.lua` names only in a predicate; the independent
`*search-results*` panel in `builtin/commands/default.lua:869`, with
its own intercept and writes; and dired buffers (`dired.lua:371`). The
primitive they need now exists and is proven, so the remaining work is
adoption plus a streaming-friendly variant — the three appending
buffers need it, while listview and dired already write whole-buffer
replaces and are the cheap half.
**The CRDT half is closed too** (review round 3). Clearing the v0.1
stacks proves nothing in CRDT mode, where they are bypassed entirely and

254
scripts/regen-lean-abbrev Executable file
View File

@ -0,0 +1,254 @@
#!/usr/bin/env python3
"""Regenerate builtin/runtime/lean_abbrev.lua from vscode-lean4.
Usage: scripts/regen-lean-abbrev <vscode-lean4-commit>
Fetches `lean4-unicode-input/src/abbreviations.json` at the given commit
and rewrites the vendored Lua table, including the provenance header, so
the artifact is self-describing to whoever next touches it. A refresh is
an ordinary PR with a visible diff — the diff is the review.
There is no automatic sync and none is wanted: an editor that silently
re-downloads its input method has a supply-chain problem, not a feature
(docs/lean4-mode-framing.md Q#LN11).
The emit is an ORDERED SEQUENCE, not a map. Upstream resolves
equal-length abbreviation ties by source declaration order — 101
prefixes depend on it — and a Lua `{ [key] = symbol }` table iterated
with `pairs` cannot carry that. A map-shaped emit would also be
nondeterministic across builds and, once a hash order happened to be
stable, stably wrong.
This script ABORTS rather than emitting something plausible when the
source is corrupt: a duplicate key after decoding (JSON permits them,
the table must not), a key or symbol that is not well-formed UTF-8, or a
round-trip mismatch. That last check re-parses the script's own output
with an independent unescaper and compares the full ordered sequence to
the source, entry for entry. It is what makes the vendored file
trustworthy, and it belongs here rather than in the acceptance suite:
the suite cannot see `abbreviations.json`, which is not shipped.
"""
import json
import pathlib
import sys
import urllib.request
REPO = "leanprover/vscode-lean4"
PATH = "lean4-unicode-input/src/abbreviations.json"
LICENSE = "Apache-2.0"
OUT = pathlib.Path(__file__).resolve().parent.parent / "builtin/runtime/lean_abbrev.lua"
# Canonical, lossless, byte-deterministic. Rev 6 of the framing said the
# generator should abort on "a key containing a character the emitted Lua
# would have to escape"; that rule rejects the real table, where `\` is a
# key and `"` begins eleven of them.
SHORT = {"\\": "\\\\", '"': '\\"', "\n": "\\n", "\r": "\\r", "\t": "\\t"}
def die(msg):
print(f"regen-lean-abbrev: {msg}", file=sys.stderr)
raise SystemExit(1)
def lua_escape(s):
"""Escape one string for a Lua double-quoted literal.
Operates on CHARACTERS, not bytes. Decomposing to UTF-8 bytes and
emitting each as `chr(byte)` produces a latin-1-shaped string that
`write_text(..., encoding="utf-8")` then re-encodes — every
non-ASCII symbol lands in the file double-encoded, and a round-trip
check that compares in-memory strings agrees with itself and misses
it entirely. Only control bytes, which are single-byte by
definition, become `\\ddd`.
"""
out = []
for ch in s:
if ch in SHORT:
out.append(SHORT[ch])
elif ord(ch) < 0x20 or ord(ch) == 0x7F:
out.append(f"\\{ord(ch):03d}")
else:
out.append(ch)
return "".join(out)
def lua_unescape(s):
"""Independent reader for the round-trip check.
Deliberately not the inverse of `lua_escape` sharing its table: a
check that reuses the encoder's own assumptions cannot detect that
those assumptions are wrong.
"""
out = bytearray()
i = 0
raw = s.encode("utf-8")
while i < len(raw):
b = raw[i]
if b != ord("\\"):
out.append(b)
i += 1
continue
i += 1
if i >= len(raw):
die("round-trip: trailing backslash in emitted string")
nxt = chr(raw[i])
if nxt in ("\\", '"'):
out.append(ord(nxt))
i += 1
elif nxt in ("n", "r", "t"):
out.append({"n": 10, "r": 13, "t": 9}[nxt])
i += 1
elif nxt.isdigit():
digits = ""
while i < len(raw) and chr(raw[i]).isdigit() and len(digits) < 3:
digits += chr(raw[i])
i += 1
out.append(int(digits))
else:
die(f"round-trip: unknown escape \\{nxt} in emitted string")
return out.decode("utf-8")
def main():
if len(sys.argv) != 2:
die(f"usage: {sys.argv[0]} <vscode-lean4-commit>")
commit = sys.argv[1]
url = f"https://raw.githubusercontent.com/{REPO}/{commit}/{PATH}"
with urllib.request.urlopen(url, timeout=60) as resp:
raw = resp.read()
try:
raw.decode("utf-8")
except UnicodeDecodeError as e:
die(f"source is not well-formed UTF-8: {e}")
# `object_pairs_hook` keeps declaration order AND exposes duplicate
# keys, which a plain dict would silently collapse.
pairs = json.loads(raw, object_pairs_hook=lambda kv: kv)
seen = {}
for i, (key, symbol) in enumerate(pairs):
if key in seen:
die(f"duplicate key {key!r} at entries {seen[key]} and {i}")
seen[key] = i
for label, s in (("key", key), ("symbol", symbol)):
if not isinstance(s, str):
die(f"{label} at entry {i} is not a string: {s!r}")
try:
s.encode("utf-8")
except UnicodeEncodeError as e:
die(f"{label} at entry {i} is not well-formed UTF-8: {e}")
cursor = sum(1 for _, v in pairs if "$CURSOR" in v)
for i, (key, symbol) in enumerate(pairs):
if symbol.count("$CURSOR") > 1:
die(f"symbol for {key!r} at entry {i} has more than one $CURSOR")
body = "".join(
f' {{ "{lua_escape(k)}", "{lua_escape(v)}" }},\n' for k, v in pairs
)
text = HEADER.format(
repo=REPO,
path=PATH,
commit=commit,
license=LICENSE,
count=len(pairs),
cursor=cursor,
bytes=len(raw),
script=pathlib.Path(sys.argv[0]).name,
) + "pmacs.lean_abbrev = {\n" + body + "}\n"
# Round-trip against the BYTES ON DISK, not the string in memory.
# The file is staged beside its destination, re-read, parsed, and
# only renamed into place once it compares equal entry for entry. A
# check that compares in-memory strings cannot see an encoding
# applied by the write itself, which is exactly how a
# double-encoding bug survived the first version of this script.
staged = OUT.with_suffix(".lua.staged")
staged.write_text(text, encoding="utf-8")
on_disk = staged.read_bytes().decode("utf-8")
got = []
# `str.splitlines()` is WRONG here: it also splits on U+2028, U+2029,
# U+0085 and the vertical-tab family, and 53 symbols in the real
# table contain one of those literally. It silently loses entries and
# the round-trip then reports a count mismatch that is the checker's
# bug, not the emit's. The emitted file's line structure is defined
# by the LF we write, and nothing else.
for line in on_disk.split("\n"):
line = line.strip()
if not line.startswith('{ "') or not line.endswith("},"):
continue
inner = line[1:-2].strip()
if not (inner.startswith('"') and inner.endswith('"')):
die(f"round-trip: unparsable emitted line: {line!r}")
fields, buf, esc, depth = [], [], False, 0
for ch in inner:
if esc:
buf.append(ch)
esc = False
elif ch == "\\":
buf.append(ch)
esc = True
elif ch == '"':
depth += 1
if depth % 2 == 0:
fields.append("".join(buf))
buf = []
elif depth % 2 == 1:
buf.append(ch)
if len(fields) != 2:
die(f"round-trip: expected 2 fields, got {len(fields)}: {line!r}")
got.append((lua_unescape(fields[0]), lua_unescape(fields[1])))
def fail(msg):
staged.unlink(missing_ok=True)
die(msg)
if len(got) != len(pairs):
fail(f"round-trip: emitted {len(got)} entries, source has {len(pairs)}")
for i, (want, have) in enumerate(zip(pairs, got)):
if tuple(want) != have:
fail(f"round-trip: entry {i} differs: source {want!r} vs emitted {have!r}")
staged.replace(OUT)
print(
f"wrote {OUT} — {len(pairs)} entries from {REPO}@{commit} "
f"({len(raw)} source bytes, {OUT.stat().st_size} emitted bytes), "
"round-trip verified against the bytes on disk"
)
HEADER = """\
-- lean_abbrev.lua --- VENDORED DATA. Do not edit by hand.
--
-- The Lean 4 abbreviation table, generated from:
--
-- repo: https://github.com/{repo}
-- path: {path}
-- commit: {commit}
-- license: {license}
-- entries: {count} ({cursor} carry $CURSOR)
-- source: {bytes} bytes
--
-- Regenerate with:
--
-- scripts/{script} {commit}
--
-- An ORDERED SEQUENCE, not a map: upstream resolves equal-length ties
-- by source declaration order (101 prefixes depend on it), and a
-- `pairs`-iterated Lua map cannot express that. The file's own line
-- order is the audit trail. Consumers must not reorder it.
--
-- Not fetched at runtime and not a package dependency: the input method
-- has to work offline and on first launch. Upkeep is a documented
-- manual process — see docs/lean4-mode-framing.md Q#LN11.
pmacs = pmacs or {{}}
"""
if __name__ == "__main__":
main()

395
src/daemon.rs
View File

@ -1627,18 +1627,97 @@ fn open_initial_target(
// create and select a side window, and bootstrap must reassert the
// requested buffer in a document window rather than overwriting a
// panel merely because it became `view.active`.
let (origin_window, buffer_id, fire) = {
let (origin_window, resolved) = {
let mut core = editor.core.borrow_mut();
core.active_frontend = frontend_id;
let origin_window = core
.primary_document_window(frontend_id)
.ok_or_else(|| "attaching frontend has no document window".to_string())?;
let (buffer_id, fire) = core.resolve_target_buffer(&path)?;
let resolved = core.resolve_target_buffer(&path)?;
(origin_window, resolved)
};
// Journey Stage 1a (Q#JR6/Q#JR9): a DIRECTORY installs nothing.
//
// Nothing can be installed, because the listing that satisfies a
// directory open is asynchronous and this block is synchronous — the
// frontend is blocked on `InitialTargetResult` and will not create
// its window until it arrives, so there is no tick in which a
// listing could settle. The reply therefore names the buffer the
// fresh view's document window ALREADY holds, which is a valid,
// ready session; the listing replaces it a tick or more later.
//
// That buffer is NOT necessarily `*scratch*`: `build_fresh_frontend_view`
// clones LOCAL's primary document buffer. If LOCAL holds a real
// document, this session briefly displays and snapshots it. Accepted
// and documented rather than papered over with a placeholder buffer,
// which would need reaping and would be fought by the reassert below.
//
// `publish_to_replicas` is false for the same reason an `AfterSwitch`
// dedup sets it false: this buffer is pre-existing and already
// published, not freshly loaded here.
let (buffer_id, fire) = match resolved {
crate::editor_core::ResolvedTarget::Directory { path } => {
let dest = editor
.capture_directory_destination(frontend_id, origin_window)
.ok_or_else(|| format!("cannot open {}: no document window", path.display()))?;
editor.dispatch_directory_open(&path, dest);
editor.reconcile_panel_layout(frontend_id);
// The reply must name what the window ACTUALLY holds now, not
// what it held before the dispatch.
//
// The chain runs synchronously. dired's handler defers (it
// spawns a coroutine for the listing), but a user's resolver
// is under no such obligation: a handler that opens something
// synchronously -- through `commit_to`, which is exactly the
// supported way to do it -- has already replaced this
// window's buffer by the time we get here. Reporting the
// captured id would then send the snapshot of one buffer and
// the identity of another, and the frontend would render a
// document nobody asked for.
//
// Re-reading also covers the case a hook closed the window,
// which is why this rehomes through `non_side_target` exactly
// as the file arm's reassert does rather than returning early
// and skipping that check.
let mut core = editor.core.borrow_mut();
core.active_frontend = frontend_id;
let destination = if core
.views
.get(&frontend_id)
.is_some_and(|view| view.layout.iter_ids().contains(&origin_window))
{
origin_window
} else {
core.non_side_target(frontend_id)
.map_err(|error| format!("cannot reselect {}: {error}", path.display()))?
};
core.focus_window(frontend_id, destination);
let buffer_id = core
.windows
.get(&destination)
.map(|window| window.buffer_id)
.ok_or_else(|| format!("cannot reselect {}: window died", path.display()))?;
return Ok(OpenedInitialTarget {
buffer_id,
// False whether or not the chain replaced the buffer: an
// untouched destination is pre-existing and already
// published, and a buffer a synchronous handler installed
// went through the ordinary display path, which publishes
// on its own terms.
publish_to_replicas: false,
});
}
crate::editor_core::ResolvedTarget::Buffer { id, fire } => (id, fire),
};
{
let mut core = editor.core.borrow_mut();
core.install_buffer_in_window(origin_window, buffer_id)
.map_err(|error| format!("cannot select {}: {error}", path.display()))?;
core.focus_window(frontend_id, origin_window);
(origin_window, buffer_id, fire)
};
}
match fire {
crate::editor_core::HookKind::AfterLoad => {
@ -3978,6 +4057,143 @@ mod tests {
);
}
/// Arc 8 Stage 4b acceptance 45f: the Lean abbreviation expander
/// works on the OPTIMISTIC producer, not only on `dispatch_key`.
///
/// This is the path most users take and the one no other Stage 4b
/// test covers. `classify_key` (`src/optimistic.rs`) returns
/// `Insert(c)` for `\` and for every ASCII letter — only the nine
/// built-in pair chars are excluded (Q#AP1) — so on a CRDT frontend
/// `\alpha` arrives here as six source-peer optimistic inserts,
/// while the expansion is a single daemon-peer replace spanning all
/// six. That asymmetry is the accepted undo degradation of Q#LN21;
/// what this pins is that the expansion happens at all.
///
/// It lives in `--lib` deliberately: the gate list runs
/// `--features crdt` only for `cargo test --lib`, so a crdt-gated
/// INTEGRATION test would be dark in CI and dark in the gates both.
///
/// The source frontend needs a REGISTERED WINDOW on the edited
/// buffer or nothing is armed at all — `handle_remote_crdt_op`
/// arms the record only when the source's active window displays
/// the buffer, so a source with no view fails closed and silently.
/// A version of this test without the view below passed six
/// fan-outs with a nil record and proved nothing.
#[cfg(feature = "crdt")]
#[test]
fn the_optimistic_producer_also_expands_a_lean_abbreviation() {
use crate::editor::EditorState;
use crate::protocol::FrontendId;
use crate::window::{FrontendView, Layout, Window, WindowId};
let dir = std::env::temp_dir().join(format!("pmacs-lean-opt-{}", std::process::id()));
std::fs::create_dir_all(&dir).expect("create temp dir");
let path = dir.join("a.lean");
std::fs::write(&path, "").expect("write fixture");
let source = FrontendId(77);
let mut editor = EditorState::new();
editor
.lua_host
.eval(Some("test"), "pmacs.lsp.config = {}")
.expect("clear lsp config");
editor
.lua_host
.eval(
Some("test-open"),
&format!(
"pmacs.buffer.find_or_open({:?}); pmacs.editor.goto_byte(0)",
path.display().to_string()
),
)
.expect("open the lean fixture");
let buffer_id = editor.core.borrow().active_window().buffer_id;
{
let mut core = editor.core.borrow_mut();
let mut reg = core.registry.borrow_mut();
reg.get_mut(buffer_id)
.expect("active buffer")
.upgrade_to_crdt(2)
.expect("upgrade to crdt");
drop(reg);
// The replica's own window on the shared buffer.
let text_view = {
let registry = core.registry.clone();
let reg = registry.borrow();
crate::text_view::TextView::new(reg.get(buffer_id).expect("buffer"))
};
let win_id = WindowId::next();
core.windows
.insert(win_id, Window::new(win_id, buffer_id, text_view));
core.register_frontend_view(
source,
FrontendView {
layout: Layout::single(win_id),
active: win_id,
fold_projection: true,
panel_capable: true,
frame_geometry: None,
panel_hidden: false,
},
);
}
let snapshot_bytes = {
let core = editor.core.borrow();
let reg = core.registry.borrow();
reg.get(buffer_id)
.expect("buffer")
.crdt_state()
.expect("crdt-backed")
.export_snapshot()
.expect("export snapshot")
};
let peer = loro::LoroDoc::new();
peer.set_peer_id(77).expect("set peer id");
peer.import(&snapshot_bytes).expect("import snapshot");
// One op per keystroke, exactly as the attach loop's
// optimistic-apply branch produces them.
for (i, ch) in "\\alpha".chars().enumerate() {
let v_before = peer.oplog_vv();
peer.get_text("body")
.insert(i, &ch.to_string())
.expect("peer insert");
let op_bytes = peer
.export(loro::ExportMode::updates(&v_before))
.expect("export op");
super::handle_remote_crdt_op(
&mut editor,
source,
buffer_id,
crate::rope::CrdtOp {
peer_id: 77,
bytes: op_bytes,
},
);
}
let text = match editor
.lua_host
.eval(
Some("test-readback"),
"local b = pmacs.window.buffer(); return b:slice(0, b:len())",
)
.expect("read buffer text")
{
mlua::Value::String(s) => String::from_utf8_lossy(&s.as_bytes()).into_owned(),
other => panic!("expected buffer text, got {other:?}"),
};
assert_eq!(
text, "α",
"the abbreviation expanded on the optimistic path — the \
record the expander reads is armed by handle_remote_crdt_op, \
not only by dispatch_key"
);
}
/// Q#AI9 (PR #109 round 1): the optimistic-apply arm clears an
/// EMPTY anchor on the source window — the GPU always takes this
/// path, and the TUI attach mirror tracks no selection state, so
@ -4899,6 +5115,177 @@ mod tests {
);
}
/// **N2** (Journey Stage 1a) — a DIRECTORY initial target reaches
/// readiness instead of failing.
///
/// This deliberately supersedes the directory half of the GPU
/// initial-target framing's Q#GT6 and its acceptance 10, which
/// required `IsADirectory` to fail before window creation.
/// Permission-denied and every other pre-readiness failure keep that
/// contract.
#[test]
fn initial_target_directory_reaches_ready() {
use crate::editor::EditorState;
use crate::protocol::FrontendId;
let dir = tempfile::tempdir().expect("tempdir");
std::fs::write(dir.path().join("alpha.txt"), b"alpha\n").expect("write");
let mut editor = EditorState::new();
editor
.lua_host
.lua()
.load("pmacs.lsp.config = {}")
.exec()
.expect("wipe lsp config");
let fid = FrontendId(131);
let view = build_fresh_frontend_view(&mut editor, false, false);
editor.core.borrow_mut().register_frontend_view(fid, view);
let opened = open_initial_target(
&mut editor,
fid,
InitialTarget {
path: dir.path().as_os_str().as_bytes().to_vec(),
cwd: dir.path().as_os_str().as_bytes().to_vec(),
},
)
.expect("a directory target must reach readiness, not fail");
// The reply names a live buffer in a live document window: a
// valid, ready session. The listing arrives later, asynchronously.
let core = editor.core.borrow();
assert!(
core.registry.borrow().contains(opened.buffer_id),
"the reported buffer must exist so its snapshot can be sent"
);
let active = core.views[&fid].active;
assert_eq!(
core.windows[&active].buffer_id, opened.buffer_id,
"the reported buffer is the one the document window shows"
);
}
/// **N5** — the bootstrap buffer is not necessarily `*scratch*`.
///
/// `build_fresh_frontend_view` clones LOCAL's PRIMARY DOCUMENT
/// buffer, so when LOCAL holds a real document the fresh session
/// briefly displays and snapshots it. Q#JR9 accepts that rather than
/// introducing a placeholder; this observes it instead of assuming.
#[test]
fn initial_target_directory_reports_a_non_scratch_primary() {
use crate::editor::EditorState;
use crate::protocol::FrontendId;
let dir = tempfile::tempdir().expect("tempdir");
let doc = dir.path().join("already-open.txt");
std::fs::write(&doc, b"local document\n").expect("write");
// LOCAL holds a real document, not scratch.
let mut editor = EditorState::open(doc.clone()).expect("open");
editor
.lua_host
.lua()
.load("pmacs.lsp.config = {}")
.exec()
.expect("wipe lsp config");
let local_primary = editor
.core
.borrow()
.primary_document_buffer(FrontendId::LOCAL)
.expect("LOCAL always has a document window");
let fid = FrontendId(132);
let view = build_fresh_frontend_view(&mut editor, false, false);
editor.core.borrow_mut().register_frontend_view(fid, view);
let opened = open_initial_target(
&mut editor,
fid,
InitialTarget {
path: dir.path().as_os_str().as_bytes().to_vec(),
cwd: dir.path().as_os_str().as_bytes().to_vec(),
},
)
.expect("a directory target must reach readiness");
assert_eq!(
opened.buffer_id, local_primary,
"the bootstrap reply names LOCAL's primary document buffer, \
which is a real document here rather than *scratch*"
);
}
/// **N2b (rev 6)** — a resolver that claims SYNCHRONOUSLY is reported
/// correctly.
///
/// The bug this pins: the arm captured the destination buffer id
/// *before* dispatching the chain and reported that. The chain runs
/// synchronously, so a handler that opens something immediately —
/// through `commit_to`, the supported way — had already replaced the
/// window's buffer, and the reply paired one buffer's snapshot with
/// another's identity.
///
/// Falsified by reporting the captured id instead of re-reading.
#[test]
fn initial_target_directory_reports_what_a_synchronous_handler_installed() {
use crate::editor::EditorState;
use crate::protocol::FrontendId;
let dir = tempfile::tempdir().expect("tempdir");
let mut editor = EditorState::new();
editor
.lua_host
.lua()
.load(
"pmacs.lsp.config = {}
claimed = pmacs.buffer.create('*claimed*')
pmacs.path.set_directory_handler(function(path, dest)
pmacs.window.commit_to(dest, function()
pmacs.window.display(claimed, { select = true })
end)
end)",
)
.exec()
.expect("install a synchronous handler");
let fid = FrontendId(133);
let view = build_fresh_frontend_view(&mut editor, false, false);
editor.core.borrow_mut().register_frontend_view(fid, view);
let opened = open_initial_target(
&mut editor,
fid,
InitialTarget {
path: dir.path().as_os_str().as_bytes().to_vec(),
cwd: dir.path().as_os_str().as_bytes().to_vec(),
},
)
.expect("a claimed directory target must reach readiness");
// Compare by NAME: the reported id must be the handler's buffer,
// and naming it is what makes the failure legible when it is not.
let core = editor.core.borrow();
let reported_name = core
.registry
.borrow()
.get(opened.buffer_id)
.expect("the reported buffer exists")
.name()
.to_string();
assert_eq!(
reported_name, "*claimed*",
"the reply must name what the handler installed, not the \
buffer captured before the dispatch"
);
let active = core.views[&fid].active;
assert_eq!(
core.windows[&active].buffer_id, opened.buffer_id,
"…and that buffer is what the window shows"
);
}
/// 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

356
src/editor.rs
View File

@ -26,7 +26,6 @@ use unicode_width::UnicodeWidthStr;
use crate::async_runtime::SharedAsyncRuntime;
use crate::cell::{CellCoord, CellSize};
use crate::editor_core::EditorCore;
use crate::file_io::load_file;
use crate::frontend::{Event, Frontend, KeyEvent, KeyEventKind, MouseEvent, install_panic_hook};
use crate::key::{Chord, display_sequence};
use crate::keymap_stack::{Action, KeyDispatcher};
@ -80,6 +79,109 @@ impl Drop for InteractiveCommandOriginGuard {
}
}
/// A frontend scope for **background** work — deliberately NOT
/// [`InteractiveCommandOrigin`] (Journey Stage 1a, Q#JR14e).
///
/// An async continuation (a settled directory listing, and eventually
/// any other post-await window work) needs to act for the frontend that
/// *requested* it rather than whichever one happens to be ambient when
/// the worker finishes. Reusing the interactive origin for that would be
/// wrong twice over:
///
/// 1. **It does not scope enough.** Only `acting_frontend` consults it,
/// so `pmacs.window.display` would be scoped while no-arg
/// `pmacs.window.buffer()` (which reads `active_buffer_id()`
/// directly) and `pmacs.editor.move_to_line` (which mutates the
/// core's ambient active window) stayed ambient — and those are
/// precisely the calls that capture and seat.
/// 2. **It is authenticated user-command authority.** It is what
/// distinguishes a user command's edit from a plugin's or the data
/// API's: the pre-edit unfold guard, `invoke_interactive`'s
/// command-boundary rotation, and the terminal surface's "requires an
/// interactive frontend context" checks all key off it. A background
/// listing must not acquire any of that.
///
/// So this is a separate slot, resolved *ahead* of the interactive
/// origin, whose guard **also** swaps `EditorCore::active_frontend` —
/// which is what covers the core-ambient APIs `acting_frontend` never
/// sees. That swap is not a workaround: `pmacs.window.buffer()`'s no-arg
/// arm documents its own correctness as resting on "dispatch sets
/// `active_frontend` to the acting frontend before running a command",
/// and this restores that invariant for a continuation.
#[derive(Clone, Default)]
pub(crate) struct ScopedFrontend(Rc<Cell<Option<FrontendId>>>);
impl ScopedFrontend {
/// The override in force, if any.
#[must_use]
pub(crate) fn current(&self) -> Option<FrontendId> {
self.0.get()
}
/// Enter a background frontend scope, also swapping the core's
/// ambient `active_frontend`. Both are restored on drop, on every
/// exit path including a raising callback.
pub(crate) fn enter(
&self,
core: &SharedCore,
commit_scope: &CommitScopeActive,
frontend_id: FrontendId,
) -> ScopedFrontendGuard {
let previous = self.0.replace(Some(frontend_id));
let previous_active = {
let mut core = core.borrow_mut();
let was = core.active_frontend;
core.active_frontend = frontend_id;
was
};
let previous_commit = commit_scope.0.replace(true);
ScopedFrontendGuard {
scope: self.clone(),
core: core.clone(),
previous,
previous_active,
commit_scope: commit_scope.clone(),
previous_commit,
}
}
}
pub(crate) struct ScopedFrontendGuard {
scope: ScopedFrontend,
core: SharedCore,
previous: Option<FrontendId>,
previous_active: FrontendId,
/// Cleared together with the scope, so an awaiting callback cannot
/// leave `await` refused after the commit ends (Q#JR14b).
commit_scope: CommitScopeActive,
previous_commit: bool,
}
impl Drop for ScopedFrontendGuard {
fn drop(&mut self) {
self.scope.0.set(self.previous);
self.core.borrow_mut().active_frontend = self.previous_active;
self.commit_scope.0.set(self.previous_commit);
}
}
/// Whether a `pmacs.window.commit_to` callback is currently running
/// (Journey Stage 1a, Q#JR14b).
///
/// Read from Lua as `pmacs._async._in_commit_scope()`; `Handle:await`
/// refuses while it is set. Lives beside the scope guard so the two can
/// never disagree.
#[derive(Clone, Default)]
pub struct CommitScopeActive(Rc<Cell<bool>>);
impl CommitScopeActive {
/// Whether a commit callback is on the stack.
#[must_use]
pub fn active(&self) -> bool {
self.0.get()
}
}
// ---------------------------------------------------------------------------
// EditorState
// ---------------------------------------------------------------------------
@ -261,6 +363,13 @@ impl EditorState {
let mut lua_host = LuaHost::with_registry(registry).expect("Lua runtime initialization");
let interactive_origin = InteractiveCommandOrigin::default();
lua_host.lua().set_app_data(interactive_origin.clone());
// Q#JR14e/Q#JR14b: the background frontend scope and the
// commit-scope flag live only as Lua app data -- `commit_to` and
// `Handle:await` are the only readers, and both reach them that
// way. No `EditorState` field, so there is no second handle that
// could disagree with the one the guard restores.
lua_host.lua().set_app_data(ScopedFrontend::default());
lua_host.lua().set_app_data(CommitScopeActive::default());
lua_host
.attach_editor(&core)
.expect("editor bindings + builtin chunks");
@ -445,6 +554,27 @@ impl EditorState {
include_str!("../builtin/runtime/pair.lua"),
)
.expect("load pair builtin chunk");
// Arc 8 Stage 4b: the Lean 4 Unicode input method. The vendored
// abbreviation table first — lean_input.lua reads it at chunk
// load to build its prefix and eager-key indexes. Both load
// after typed_edit.lua, which they register into.
//
// Load order does NOT decide whether abbreviation expansion or
// auto-pairing sees a keystroke first — the chain's priority
// does (50 vs 100), which is why Stage 4a exists. It matters
// only that the chain itself is already there.
lua_host
.eval(
Some("@pmacs/builtin/runtime/lean_abbrev.lua"),
include_str!("../builtin/runtime/lean_abbrev.lua"),
)
.expect("load lean_abbrev builtin chunk");
lua_host
.eval(
Some("@pmacs/builtin/runtime/lean_input.lua"),
include_str!("../builtin/runtime/lean_input.lua"),
)
.expect("load lean_input builtin chunk");
lua_host
.eval(
Some("@pmacs/builtin/runtime/lsp.lua"),
@ -769,35 +899,65 @@ impl EditorState {
/// Construct an editor for a path. Empty buffer with `[new file]`
/// status if the path does not exist; loaded contents otherwise.
///
/// Journey Stage 1a (Q#JR1): this is a thin caller of
/// [`EditorCore::resolve_target_buffer`], not a second
/// implementation of it. That primitive documents itself as "one
/// primitive, so two path-normalization, dedup, and hook
/// transactions cannot drift apart" — and local startup, which had
/// hand-written the same three-arm shape, was not one of its callers
/// until now.
///
/// Two things this caller still owns, and must keep owning:
///
/// * **The window install.** `resolve_target_buffer` deliberately
/// does not touch windows, so the caller places the buffer.
/// Startup uses [`Self::replace_active_buffer`], which switches
/// the ACTIVE window — an `install_buffer_in_window` into some
/// other window would load the file and leave the user looking at
/// scratch (Q#JR3).
///
/// It does **not** destroy the scratch buffer, despite what
/// `replace_active_buffer`'s own doc comment has long claimed:
/// that function only calls `switch_active_buffer`, which
/// reassigns the window's `buffer_id` and removes nothing. The
/// startup scratch survives in the registry, and did before this
/// stage too. Changing that is buffer-lifetime work with its own
/// consequences (what else may hold the id, what `C-x b` should
/// list) and is deliberately not smuggled in here.
/// * **Firing the hook outside the core borrow.** Listeners
/// re-enter `pmacs.editor.*`, which re-borrows the core
/// (Q#JR1a) — the same reason the daemon bootstrap and
/// `display_file` both fire theirs after their borrow blocks end.
///
/// A directory resolves to [`ResolvedTarget::Directory`] and is
/// dispatched to the directory resolver chain rather than opened as
/// a buffer (Q#JR6); see [`Self::open_directory_target`].
#[allow(
clippy::needless_pass_by_value,
reason = "stable public entry point mirroring `pmacs PATH` and \
`run(Option<PathBuf>)`; the body stopped consuming the \
PathBuf when this became a `resolve_target_buffer` caller, \
and churning the signature would touch every caller for no \
behavioral gain"
)]
pub fn open(path: PathBuf) -> io::Result<Self> {
let display_name = path.display().to_string();
let state = Self::new();
let mut state = Self::new();
let resolved = state
.core
.borrow_mut()
.resolve_target_buffer(&path)
.map_err(io::Error::other)?;
let mut fire_after_load = false;
match load_file(&path) {
Ok((bytes, meta)) => {
let new_id = state
.lua_host
.registry()
.borrow_mut()
.create_from_bytes(display_name, &bytes);
state.replace_active_buffer(new_id);
let mut core = state.core.borrow_mut();
core.set_buffer_path(new_id, Some(path));
core.set_buffer_meta(new_id, Some(meta));
fire_after_load = true;
Ok(())
match resolved {
crate::editor_core::ResolvedTarget::Buffer { id, fire } => {
state.replace_active_buffer(id);
fire_after_load = matches!(fire, crate::editor_core::HookKind::AfterLoad);
}
Err(e) if e.kind() == io::ErrorKind::NotFound => {
let new_id = state.lua_host.registry().borrow_mut().create(display_name);
state.replace_active_buffer(new_id);
let mut core = state.core.borrow_mut();
core.set_buffer_path(new_id, Some(path));
core.status = "[new file]".into();
Ok(())
crate::editor_core::ResolvedTarget::Directory { path } => {
state.open_directory_target(&path);
}
Err(e) => Err(e),
}?;
let mut state = state;
}
if fire_after_load {
// Fire the hook *after* the borrow on `core` is released
// (block above ends). Listeners may legitimately re-enter
@ -809,9 +969,147 @@ impl EditorState {
Ok(state)
}
/// Switch the active window to `buffer_id`, dropping any old
/// scratch buffer if the active window's previous buffer has no
/// other windows referencing it. Returns silently on a stale id.
/// Capture the destination a directory open must commit to
/// (Q#JR14), or `None` when `frontend` has no document window.
///
/// Synchronous by necessity: the listing settles a tick or more
/// later, and by then the ambient frontend, selected window, and
/// active buffer may all name something else.
pub(crate) fn capture_directory_destination(
&self,
frontend: crate::protocol::FrontendId,
window: crate::window::WindowId,
) -> Option<crate::editor_core::DirectoryDestination> {
let core = self.core.borrow();
let buffer = core.windows.get(&window)?.buffer_id;
Some(crate::editor_core::DirectoryDestination {
frontend,
window,
buffer,
})
}
/// Local-startup directory open (Q#JR6): resolve the destination
/// from `LOCAL`'s document window and dispatch the resolver chain.
///
/// Public because it is the whole of what `pmacs DIRECTORY` does
/// after resolution — acceptance drives this rather than
/// `resolve_target_buffer`, so a directory arm with no production
/// caller cannot pass.
pub fn open_directory_target(&mut self, path: &std::path::Path) {
// Canonicalize here as well as in the resolver arm. The two are
// not redundant: this is a public "open this directory" seam, so
// a caller that did not come through `resolve_target_buffer`
// must still hand the chain a canonical path (Q#JR8) --- and
// normalization is idempotent, so the startup path pays nothing.
let path = crate::editor_core::normalize_buffer_path(path.to_path_buf());
let path = path.as_path();
let window = self
.core
.borrow()
.primary_document_window(crate::protocol::FrontendId::LOCAL);
let dest = window.and_then(|window| {
self.capture_directory_destination(crate::protocol::FrontendId::LOCAL, window)
});
let Some(dest) = dest else {
self.core.borrow_mut().status =
format!("cannot open {}: no document window", path.display());
return;
};
self.dispatch_directory_open(path, dest);
}
/// Run the directory resolver chain for `path`, then its fallback
/// (Journey Stage 1a, Q#JR7/Q#JR15).
///
/// Order is user chain first, builtin default second — see
/// `install_path_module` for why that cannot be expressed as two
/// hook subscriptions.
///
/// **A raising listener stops the chain AND suppresses the
/// fallback.** `run_short_circuit` returns `proceed = false` both
/// for a literal `false` (a claim) and for a raise, so `proceed`
/// alone already suppresses correctly; `errors` is what distinguishes
/// them, and it decides only whether to *report*. Running the
/// fallback after a user's resolver crashed would open dired on a
/// directory that resolver may have been part-way through handling,
/// so a crash is treated as a claim that failed — reported through
/// the `*errors*` buffer (which `run_hook` already does) and the
/// status line (which it does not), and visible in both.
pub(crate) fn dispatch_directory_open(
&mut self,
path: &std::path::Path,
dest: crate::editor_core::DirectoryDestination,
) {
let display = path.display().to_string();
let args = {
let lua = self.lua_host.lua();
let destination =
match lua.create_userdata(crate::lua_bindings::DirectoryDestinationLua(dest)) {
Ok(userdata) => mlua::Value::UserData(userdata),
Err(error) => {
self.core.borrow_mut().status = format!("cannot open {display}: {error}");
return;
}
};
let path_value = match lua.create_string(display.as_bytes()) {
Ok(string) => mlua::Value::String(string),
Err(error) => {
self.core.borrow_mut().status = format!("cannot open {display}: {error}");
return;
}
};
mlua::MultiValue::from_vec(vec![path_value, destination])
};
match self.lua_host.run_hook("path.open-directory", args.clone()) {
// A listener raised. `run_hook` has already appended the
// record to *errors*; add the status line, and do NOT fall
// back (Q#JR15).
Some(outcome) if !outcome.errors.is_empty() => {
self.core.borrow_mut().status =
format!("cannot open {display}: a path.open-directory listener failed");
return;
}
// Claimed: a listener returned false.
Some(outcome) if !outcome.proceed => return,
// Declined, or no listeners at all.
_ => {}
}
let handler = {
let lua = self.lua_host.lua();
lua.globals()
.get::<mlua::Table>("pmacs")
.and_then(|pmacs| pmacs.get::<mlua::Table>("path"))
.and_then(|path| path.get::<mlua::Value>("directory_handler"))
.unwrap_or(mlua::Value::Nil)
};
let mlua::Value::Function(handler) = handler else {
// The slot is clear: nothing surfaces directories. The
// session started fine and simply has nothing to show for
// the argument, so this is a status message and NOT a
// startup failure (Q#JR10).
self.core.borrow_mut().status = format!("no handler for directory {display}");
return;
};
if let Err(error) = handler.call::<()>(args) {
self.core.borrow_mut().status = format!("cannot open {display}: {error}");
}
}
/// Switch the active window to `buffer_id`. Returns silently on a
/// stale id.
///
/// **Corrected (Journey Stage 1a).** This comment previously claimed
/// it dropped "any old scratch buffer if the active window's
/// previous buffer has no other windows referencing it". It never
/// did: the body is one `switch_active_buffer` call, which reassigns
/// `aw.buffer_id` and removes nothing from the registry. The claim
/// was load-bearing enough that a framing decision (Q#JR3) and an
/// acceptance pin were written against it before anyone checked the
/// body. Removing the stale scratch may well be worth doing; it is
/// separate work, and this comment no longer promises it.
fn replace_active_buffer(&self, buffer_id: crate::buffer::BufferId) {
let mut core = self.core.borrow_mut();
let _ = core.switch_active_buffer(buffer_id);

193
src/editor_core.rs
View File

@ -94,6 +94,77 @@ pub enum HookKind {
None,
}
/// What a path resolved to (Journey Stage 1a, Q#JR5).
///
/// A sum type rather than `(Option<BufferId>, HookKind)`: that pair
/// admits three states that cannot occur (`None` with `AfterLoad`,
/// `Some` with a directory, …), and every caller would have to
/// re-establish by hand which combinations are real.
///
/// **Do not confuse [`HookKind`] here with [`crate::hook::HookKind`]** —
/// unrelated types sharing a name. This one says *which* lifecycle hook
/// to fire; that one says how a hook's callbacks fan out. Every site
/// touching both writes them path-qualified (Q#JR5b).
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum ResolvedTarget {
/// A file buffer, plus the hook the caller must fire with the
/// destination window active.
Buffer {
/// The resolved buffer.
id: BufferId,
/// Which lifecycle hook this resolution owes.
fire: HookKind,
},
/// A directory. No buffer is created (Q#JR6) — the directory
/// resolver chain decides what surfaces it, and dired builds its own
/// buffer through `claim_handle` rather than adopting one.
///
/// `path` is **normalized** — absolute, tilde-expanded, lexically
/// clean. This is not free and must not be assumed: normalization
/// otherwise happens inside [`Self::set_buffer_path`], which never
/// runs on this arm, so a caller resolving `"."` would keep `"."`
/// (Q#JR8). A handler keying state by path needs the canonical form.
Directory {
/// The normalized directory path.
path: PathBuf,
},
}
/// Where a directory open was requested, captured **synchronously** at
/// resolve time (Journey Stage 1a, Q#JR14).
///
/// The listing that satisfies a directory open is asynchronous
/// (`pmacs.fs.read_dir` is worker-dispatched and must be awaited), so the
/// code that finally builds and displays the listing runs a tick or more
/// later — outside interactive dispatch, where `pmacs.window.*` acts on
/// the *ambient* frontend by documented design (`builtin/runtime/dired.lua`).
/// Without a captured destination, a second frontend dispatching in the
/// meantime silently redirects the listing.
///
/// All three fields are load-bearing:
///
/// * `frontend` — the scope the commit must run in.
/// * `window` — the exact destination; the ambient selected window is
/// not it.
/// * `buffer` — what that window held at capture time, so **stale
/// intent loses to the user** (Q#JR14c). A user who replaced the
/// buffer while the listing was in flight is newer information than
/// the launch argument, and must not be overwritten.
///
/// Exposed to Lua only as nonconstructible userdata (Q#JR14d): as a
/// table, the *same* value is handed to every resolver listener in turn,
/// so one could mutate it and then decline — redirecting later listeners
/// — and any Lua could fabricate a plausible triple.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub struct DirectoryDestination {
/// Frontend that requested the directory.
pub frontend: FrontendId,
/// Window the listing must land in.
pub window: WindowId,
/// Buffer that window held at capture time (stale-intent check).
pub buffer: BufferId,
}
/// A `display_buffer` request (Q#BP3).
///
/// `height` and `dedicated` are deliberately option-valued at the policy
@ -880,18 +951,41 @@ impl EditorCore {
/// One primitive, so two path-normalization, dedup, and hook
/// transactions cannot drift apart.
///
/// A **directory** resolves to [`ResolvedTarget::Directory`] before
/// any load is attempted (Journey Stage 1a, Q#JR5/Q#JR6). Without
/// that arm the load runs and fails: `File::open` succeeds on a
/// directory and `read_to_end` then returns `EISDIR`, which is not
/// `NotFound`, so the `[new file]` arm never fires and every caller
/// saw a hard error — the reason `pmacs .` exited 1 and the golden
/// journey was graded broken at step 3 (`COHERENCE.md` §2).
///
/// # Errors
/// Any load failure other than `NotFound`.
pub fn resolve_target_buffer(&mut self, path: &Path) -> Result<(BufferId, HookKind), String> {
pub fn resolve_target_buffer(&mut self, path: &Path) -> Result<ResolvedTarget, String> {
// Ahead of the load, deliberately: see the EISDIR note above.
if path.is_dir() {
return Ok(ResolvedTarget::Directory {
path: normalize_buffer_path(path.to_path_buf()),
});
}
match self.get_or_load_buffer(path) {
Ok((buffer_id, true)) => Ok((buffer_id, HookKind::AfterLoad)),
Ok((buffer_id, false)) => Ok((buffer_id, HookKind::AfterSwitch)),
Ok((id, true)) => Ok(ResolvedTarget::Buffer {
id,
fire: HookKind::AfterLoad,
}),
Ok((id, false)) => Ok(ResolvedTarget::Buffer {
id,
fire: HookKind::AfterSwitch,
}),
Err(error) if error.kind() == std::io::ErrorKind::NotFound => {
let display_path = path.display().to_string();
let buffer_id = self.registry.borrow_mut().create(display_path);
self.set_buffer_path(buffer_id, Some(path.to_path_buf()));
"[new file]".clone_into(&mut self.status);
Ok((buffer_id, HookKind::None))
Ok(ResolvedTarget::Buffer {
id: buffer_id,
fire: HookKind::None,
})
}
Err(error) => Err(format!("cannot open {}: {error}", path.display())),
}
@ -3472,16 +3566,56 @@ impl EditorCore {
fid: FrontendId,
existing: Option<BufferId>,
window: Option<WindowId>,
) -> Result<WindowId, String> {
self.probe_display_target_inner(fid, existing, window)
}
/// Whether `window` will accept `incoming` as its buffer — the one
/// dedication rule, shared by every consumer (Journey Stage 1a,
/// Q#JR14f).
///
/// A dedicated window refuses anything other than what it already
/// shows; an undedicated one accepts anything. `incoming` is
/// deliberately optional, and the `None` case is not a degenerate
/// spelling of "don't care" — it means **the replacement buffer does
/// not exist yet**, and a dedicated window must therefore be treated
/// as ineligible:
///
/// | caller | `incoming` | dedicated window |
/// |---|---|---|
/// | [`Self::display_buffer`] exact-target arm | `Some(request.buffer_id)` | eligible only when already showing it |
/// | [`Self::probe_display_target`] | its existing-buffer result | preserves the load-before-placement probe |
/// | `commit_to` preflight | `None` | always ineligible |
///
/// `commit_to` passes `None` because a directory open's destination
/// is validated *before* the handler builds its buffer. Passing the
/// captured bootstrap buffer instead would approve a window
/// dedicated to *that* buffer, the handler would then claim and paint
/// a different one, and the exact display would refuse afterwards —
/// after the mutations the preflight exists to prevent.
///
/// Extracted rather than reimplemented per caller: two copies of a
/// rule that must agree is exactly the drift this stage's
/// path-resolution unification exists to close, and a future
/// eligibility rule added to only one copy would reopen it.
#[must_use]
pub fn window_accepts_buffer(&self, window: WindowId, incoming: Option<BufferId>) -> bool {
self.windows.get(&window).is_some_and(|w| {
!w.params.dedicated || incoming.is_some_and(|buffer_id| w.buffer_id == buffer_id)
})
}
fn probe_display_target_inner(
&self,
fid: FrontendId,
existing: Option<BufferId>,
window: Option<WindowId>,
) -> Result<WindowId, String> {
let view = self
.views
.get(&fid)
.ok_or_else(|| format!("frontend {fid:?} has no window layout"))?;
let eligible = |id: WindowId| {
self.windows.get(&id).is_some_and(|w| {
!w.params.dedicated || existing.is_some_and(|buffer_id| w.buffer_id == buffer_id)
})
};
let eligible = |id: WindowId| self.window_accepts_buffer(id, existing);
if let Some(target) = window {
if !view.layout.iter_ids().contains(&target) {
return Err(format!(
@ -3563,7 +3697,7 @@ impl EditorCore {
.windows
.get(&target)
.ok_or_else(|| format!("display: window {} is not live", target.raw()))?;
if window.params.dedicated && window.buffer_id != request.buffer_id {
if !self.window_accepts_buffer(target, Some(request.buffer_id)) {
return Err(format!(
"display: window {} is dedicated to another buffer",
target.raw()
@ -5300,6 +5434,45 @@ mod tests {
assert!(s.active_window_for(FrontendId::LOCAL).is_some());
}
/// Journey Stage 1a (Q#JR14f): the three decisive rows of the shared
/// eligibility predicate.
///
/// The `None` row is the one that exists for `commit_to`, and it is
/// not a "don't care": a directory open validates its destination
/// *before* the handler creates the buffer that will land there, so
/// there is no incoming id to compare and a dedicated window must be
/// refused. Approving it would let the handler claim and paint, and
/// the display would refuse afterwards — after the mutations the
/// preflight exists to prevent.
#[test]
fn window_accepts_buffer_matrix() {
let mut s = fresh();
let window = s.views[&FrontendId::LOCAL].active;
let current = s.windows[&window].buffer_id;
let other = s.registry.borrow_mut().create(String::from("other"));
// Undedicated: accepts anything, including "not decided yet".
assert!(s.window_accepts_buffer(window, Some(current)));
assert!(s.window_accepts_buffer(window, Some(other)));
assert!(s.window_accepts_buffer(window, None));
s.windows.get_mut(&window).expect("live").params.dedicated = true;
// Dedicated: only what it already shows.
assert!(
s.window_accepts_buffer(window, Some(current)),
"a dedicated window still accepts the buffer it displays"
);
assert!(
!s.window_accepts_buffer(window, Some(other)),
"a dedicated window refuses a different buffer"
);
assert!(
!s.window_accepts_buffer(window, None),
"a dedicated window refuses an as-yet-unbuilt replacement"
);
}
#[test]
fn register_and_unregister_frontend_view() {
// T M10.8 — the lifecycle API the dispatcher uses on attach

85
src/lua_bindings/mod.rs
View File

@ -3650,9 +3650,74 @@ fn install_path_module(lua: &Lua) -> mlua::Result<Table> {
)
})?,
)?;
// Journey Stage 1a (Q#JR7): the directory fallback.
//
// The resolver for a directory open is a two-tier arrangement, and
// the split is forced by how registration works rather than chosen
// for elegance. `path.open-directory` is a short-circuit hook that
// **no builtin subscribes to** — because `HookRegistry::add` only
// appends and builtins load before `init.lua`, a subscribing builtin
// would always claim first and no user listener could ever run. So
// the hook is the user's chain, and the default surface is this
// slot, consulted only when the chain declines.
//
// A slot, not a `pmacs.config` setting: `ConfigValue` is four
// scalars and a handler is none of them (the same reason terminal
// profiles could not be settings). It is an UNOWNED singleton —
// last writer wins, no owning package, no `SourceLocation`, no
// removal lifecycle, absent from every inspection surface. That is a
// real `COHERENCE.md` §13 gap, recorded rather than dressed up: when
// §20 Priority 3 lands registration ownership and `hook.remove`,
// this becomes an ordinary lowest-priority subscription carrying its
// owner and this slot is deleted rather than extended.
//
// Readable as `pmacs.path.directory_handler` so a replacement can
// capture and chain to the previous one; `nil` disables directory
// opening entirely, which is what makes that path testable.
path.set("directory_handler", mlua::Value::Nil)?;
path.set(
"set_directory_handler",
lua.create_function(|lua, handler: mlua::Value| {
match &handler {
mlua::Value::Nil | mlua::Value::Function(_) => {}
other => {
return Err(mlua::Error::runtime(format!(
"pmacs.path.set_directory_handler: expected a function or nil, got {}",
other.type_name()
)));
}
}
let pmacs: Table = lua.globals().get("pmacs")?;
let path: Table = pmacs.get("path")?;
path.set("directory_handler", handler)?;
Ok(())
})?,
)?;
Ok(path)
}
/// Lua handle for a captured directory destination (Q#JR14d).
///
/// Deliberately **nonconstructible from Lua** and read-only. The same
/// value is passed to every `path.open-directory` listener in turn: as a
/// table, an earlier listener could mutate it and then decline,
/// redirecting later listeners or the fallback to a window the user
/// never asked for — and any Lua could fabricate a plausible
/// frontend/window/buffer triple and hand it to `commit_to`. Userdata
/// with no constructor and no setters makes both unrepresentable rather
/// than merely discouraged.
///
/// The single accessor exists because dired needs the exact window for
/// its `display{window = …}` target; nothing needs the frontend or the
/// captured buffer, which stay private to the preflight.
pub(crate) struct DirectoryDestinationLua(pub(crate) crate::editor_core::DirectoryDestination);
impl mlua::UserData for DirectoryDestinationLua {
fn add_methods<M: mlua::UserDataMethods<Self>>(methods: &mut M) {
methods.add_method("window", |_, this, ()| Ok(this.0.window.raw()));
}
}
/// Build the `pmacs.ansi.*` table. The only entry today is
/// `parser()`; future additions (e.g. an event-table-validator
/// helper) live alongside it.
@ -6938,6 +7003,26 @@ pub fn install_async(
)?;
}
// Journey Stage 1a (Q#JR14b): `pmacs.window.commit_to` runs its
// callback inside a Rust-stack RAII scope. Yielding out of that
// scope would let the guard's dynamic extent and the coroutine's
// suspension diverge — the guard would restore the frontend override
// while the continuation is still parked, so the rest of the commit
// would silently run ambient again, which is the exact bug the scope
// exists to prevent. `Handle:await` therefore refuses inside it.
//
// Enforced here rather than documented in the framing, because a
// rule that only exists in prose is one a future caller breaks
// without noticing.
async_mod.set(
"_in_commit_scope",
lua.create_function(|lua, ()| {
Ok(lua
.app_data_ref::<crate::editor::CommitScopeActive>()
.is_some_and(|scope| scope.active()))
})?,
)?;
{
let rt = runtime.clone();
async_mod.set(

162
src/lua_bindings/window_panel.rs
View File

@ -44,8 +44,22 @@ use crate::window::{DEFAULT_PANEL_ROWS, MIN_WINDOW_OUTER_ROWS, Side, WindowId};
/// call falls back to the ambient active frontend, exactly as the
/// terminal surface does.
pub(crate) fn acting_frontend(lua: &Lua, core: &SharedCore) -> FrontendId {
lua.app_data_ref::<crate::editor::InteractiveCommandOrigin>()
.and_then(|origin| origin.current())
// Journey Stage 1a (Q#JR14e): the background scope wins.
//
// Order is deliberate — scoped override, then interactive origin,
// then ambient. A `commit_to` callback runs for the frontend that
// *requested* the work, and it must win over whatever happens to be
// dispatching when the worker settles. It is a separate slot rather
// than a reuse of the interactive origin because that origin is
// authenticated user-command authority (the pre-edit unfold guard,
// command-boundary rotation, and the terminal surface all key off
// it), and a background continuation must not acquire it.
lua.app_data_ref::<crate::editor::ScopedFrontend>()
.and_then(|scope| scope.current())
.or_else(|| {
lua.app_data_ref::<crate::editor::InteractiveCommandOrigin>()
.and_then(|origin| origin.current())
})
.unwrap_or_else(|| core.borrow().active_frontend_key())
}
@ -350,6 +364,123 @@ pub(crate) fn finish_adopter_placement(
a coherent surface"
)]
pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result<()> {
{
let cc = core.clone();
win.set(
"commit_to",
lua.create_function(
move |lua,
(dest, body): (mlua::Value, mlua::Function)|
-> mlua::Result<mlua::MultiValue> {
// Journey Stage 1a (Q#JR14). Preflight FIRST, then
// scope, then run. The ordering is the whole point:
// an async handler mutates real state (dired claims
// a buffer, registers a handle, captures `prev`, and
// paints) long before it reaches any call that could
// refuse. Validating at display time is four
// mutations too late and leaves a hidden buffer
// behind, so every destination precondition is
// checked before the callback is invoked at all.
//
// Typed as `Value` rather than `AnyUserData` so this
// message is REACHABLE: with the narrower type mlua
// rejects a table during argument conversion, and a
// caller who fabricated one got "error converting Lua
// table to userdata" — true, but it names neither the
// rule nor how to get a real destination.
let dest = match &dest {
mlua::Value::UserData(userdata) => {
userdata.borrow::<super::DirectoryDestinationLua>().ok()
}
_ => None,
};
let dest = dest
.ok_or_else(|| {
mlua::Error::runtime(
"pmacs.window.commit_to: expected a destination captured by \
the editor (it cannot be constructed from Lua)",
)
})?
.0;
// 1. The requesting frontend still has a layout.
let refusal = {
let core = cc.borrow();
if !core.views.contains_key(&dest.frontend) {
Some("requesting frontend is gone".to_string())
} else if !core
.views
.get(&dest.frontend)
.is_some_and(|view| view.layout.iter_ids().contains(&dest.window))
{
// 2. The destination window is still live in it.
Some(format!("window {} is gone", dest.window.raw()))
} else if core
.windows
.get(&dest.window)
.is_some_and(|w| w.buffer_id != dest.buffer)
{
// 3. Stale intent (Q#JR14c): the user
// replaced the buffer while the work was
// in flight. Their action is newer
// information than the request, so the
// request loses.
Some(format!(
"window {} now shows another buffer",
dest.window.raw()
))
} else if !core.window_accepts_buffer(dest.window, None) {
// 4. Replaceability (Q#JR14f). `None`
// because the replacement does not exist
// yet — passing the captured buffer would
// approve a window dedicated to *it*, and
// the handler's different buffer would be
// refused later, after mutating.
Some(format!("window {} is dedicated", dest.window.raw()))
} else {
None
}
};
if let Some(reason) = refusal {
let mut out = mlua::MultiValue::new();
out.push_back(mlua::Value::String(lua.create_string(reason.as_bytes())?));
out.push_front(mlua::Value::Boolean(false));
return Ok(out);
}
let scope = lua
.app_data_ref::<crate::editor::ScopedFrontend>()
.ok_or_else(|| {
mlua::Error::runtime(
"pmacs.window.commit_to: no frontend scope installed",
)
})?
.clone();
let commit = lua
.app_data_ref::<crate::editor::CommitScopeActive>()
.ok_or_else(|| {
mlua::Error::runtime(
"pmacs.window.commit_to: no commit scope installed",
)
})?
.clone();
// Both the override and the core's ambient
// `active_frontend` are restored when this guard
// drops -- on the normal return AND on a raising
// callback, which is why the result is captured
// rather than `?`-propagated through the drop.
let result = {
let _guard = scope.enter(&cc, &commit, dest.frontend);
body.call::<mlua::MultiValue>(())
};
let mut out = result?;
out.push_front(mlua::Value::Boolean(true));
Ok(out)
},
)?,
)?;
}
{
let cc = core.clone();
win.set(
@ -397,10 +528,33 @@ pub(crate) fn install(lua: &Lua, core: &SharedCore, win: &Table) -> mlua::Result
.probe_display_target(fid, existing, explicit_window)
.map_err(mlua::Error::runtime)?;
// 3. Load, dedup, or create the path-backed buffer.
let (buffer_id, fire) = cc
//
// Journey Stage 1a (Q#JR13): a DIRECTORY raises here
// and does NOT enter the directory resolver chain.
// `display_file` is "put this file in a window", not
// a CLI router — and `find-file`'s accept arm
// (`builtin/commands/default.lua`) wraps this call in
// a `pcall` whose comment guarantees that "only a
// real failure (a directory, a permission error)
// reaches here", pinned by
// `find_file_accepting_a_directory_reports_instead_of_raising`.
// Routing it into dired would silently change what
// `C-x C-f` on a directory does. Opening dired from
// find-file is a named deferral, not a side effect of
// the CLI work.
let (buffer_id, fire) = match cc
.borrow_mut()
.resolve_target_buffer(&path_buf)
.map_err(mlua::Error::runtime)?;
.map_err(mlua::Error::runtime)?
{
crate::editor_core::ResolvedTarget::Buffer { id, fire } => (id, fire),
crate::editor_core::ResolvedTarget::Directory { path } => {
return Err(mlua::Error::runtime(format!(
"pmacs.window.display_file: {} is a directory",
path.display()
)));
}
};
// 4. Enter Q#BP4's transaction, so any hook observes
// the DOCUMENT TARGET as active.
let mut request = DisplayRequest::new(buffer_id);

1299
tests/journey_acceptance.rs Normal file
View File

File diff suppressed because it is too large Load Diff

1020
tests/lean_input_acceptance.rs Normal file
View File

File diff suppressed because it is too large Load Diff