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

Merge pull request #181 from levineuwirth/lean4-stage4b-input-method 

Lean 4 Stage 4b: the Unicode input method
This commit is contained in:
Levi Neuwirth 2026-07-26 22:23:55 +00:00 committed by GitHub
parent 74301d1670 d1bff6ac30
commit 42025e4acb
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
10 changed files with 4268 additions and 184 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
COHERENCE.md
View File

@ -1041,12 +1041,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 +1079,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.

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

289
docs/active-work.md
View File

@ -23,7 +23,8 @@ 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
`githubsucks/main` @ `74301d1` (the dired Stage 1 landed-doc refresh
#169 atop 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
@ -161,175 +162,145 @@ 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
## Lean 4 lane (Arc 8) — Stages 1–4a MERGED; Stage 4b IN REVIEW
- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`),
#161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full
- **Stages 1, 2, 3a, 3b and 4a are MERGED** — #160 (`main` @ `0827dd1`),
#161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`), #179
(`a27f646`). 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
a fresh machine should read them. `docs/lean4-mode-framing.md` rev 9
carries the decisions.
### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`)
- 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:
- Framing `docs/lean4-mode-framing.md` **revision 12** (rounds 10, 11
and 12 = review of the implementation). Stage
4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b,
the Lean content that registers on it.
- Footprint: `scripts/regen-lean-abbrev` (new, the generator),
`builtin/runtime/lean_abbrev.lua` (new, VENDORED DATA — 1,855 entries
from `leanprover/vscode-lean4@17d1d08`, Apache-2.0),
`builtin/runtime/lean_input.lua` (new, the consumer at priority 50),
`src/editor.rs` (two `include_str!` blocks),
`tests/lean_input_acceptance.rs` (new, 31 tests), and one
`#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs`
(acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart
from the load sites and that one test.
- **Round 9 corrected three acceptance criteria that the real table
contradicts** — found by simulating the state machine over all 1,855
entries and re-reading upstream at the pinned commit, not by reading
the prose again. `\to` is NOT eager (`top`, `to0`, `toa` extend it);
`\zzzz` expands to `ζzzz ` because `ze`/`zeta`/`zsqrtd` exist, and
only `$ % , ; @ W` open no key at all; and `\alpha`'s undo does not
restore `\alpha ` because `alpha` IS eager, so the terminator is a
separate edit. Criteria 38, 41 and 42 now state both paths.
- **Two generator bugs, both caught by its own round-trip check
failing closed:** `str.splitlines()` also splits on U+2028/U+2029,
and 53 symbols contain one literally, so the check reported a count
mismatch that was its own bug; then escaping via `chr(byte)` produced
a latin-1-shaped string that `write_text(encoding="utf-8")`
re-encoded, and every non-ASCII symbol landed double-encoded. The
first version of the check compared IN-MEMORY strings and agreed with
itself. **It now stages the file, re-reads the bytes from disk, and
renames into place only on a match.**
- **The point must be placed explicitly after the replace.** The
expansion SHRINKS the buffer (`\alpha` 6 bytes → `α` 2), so a point
left at the pre-edit offset is past the new end and every later
self-insert is silently rejected — the editor looks dead after the
first expansion. Pairing's "no cursor motion on the clean path" does
not generalize: that holds only for an insert AT the cursor.
- **Three tests were vacuous when first written and were found by
biting, not by review:** the abandonment test asserted text that a
wrongly-surviving record would also produce (claiming makes no edit —
it needed the follow-up keystroke that completes an eager key); the
re-arm test used the framing's own `\alpha\to`, which never reaches
the re-arm branch because `alpha` is eager and closes the record
first (`\al\to` does); and both buffer-switch tests passed through
`find_or_open`'s fresh-load path, which fires `buffer.after-load` and
a record-less edit rather than `buffer.after-switch` — deleting the
subscriber left them green. All three now bite.
- **Bite table** (each mutation, and the tests it fails):
| 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) |
| register at priority 150 (after pairing) | 2 |
| claim only completed expansions | 2 |
| longest match instead of shortest | 9 |
| equal-length tie keeps the LATER key | 3 |
| remove the eager branch | 8 |
| expand without the terminator in the span | 2 |
| remove the re-arm branch | 1 |
| remove the point-still-at-span-end check | 1 |
| remove the exact-revision check | 1 |
| leave the point where the replace found it | 5 |
| remove the `lean4` language gate | 1 |
| remove the `lean.abbrev` gate | 2 |
| `buffer.after-switch` clears every frontend | 1 |
| delete the `buffer.after-switch` subscriber | 1 |
| `frontend.detached` purges every frontend | 1 |
| claim the terminator | 1 |
| expand inside the chain, then decline | 2 |
| drop the `cursor() == post_cursor` check | 1 |
| place the point without the context guard | 1 |
| load lean_input.lua after lsp.lua | 1 |
| let a nested fan-out consume the deferred slot | 1 |
| stop counting chain invocations | 1 |
| count fan-outs in the expander instead of the sentinel | 1 |
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.
Acceptance 45f bit by construction: without a registered window for
the source frontend it ran six fan-outs with a nil record and proved
nothing, because `handle_remote_crdt_op` arms nothing unless the
source's active window displays the buffer.
- **Round 10 (review) found three defects, all about what happens
AROUND the expansion rather than about resolving an abbreviation.** A
pair character that TERMINATES an abbreviation never reached pairing
(`\alp(` gave `α(`): the first revision claimed the terminator, and
merely declining is not enough either, because the chain hands each
consumer a copy of the record made before any consumer ran — so
expanding inside the chain invalidates pairing's copy and the closer
is lost anyway (verified by mutation, not assumed). The expansion now
runs on **its own `buffer.after-edit` subscriber** after the chain,
with a span that stops before the terminator. That is a new instance
of Q#AP7, so it is now pinned with the sighelp fake server.
Post-insert point motion was also mistaken for a valid span (the
relevance check needs `cursor() == post_cursor`, as pairing's has
since #110), and cursor placement could move a buffer an intercept
had switched to.
- **Round 11 found the round-10 fix incomplete in one place:
`buffer.after-edit` fan-outs NEST.** A consumer between the expander
(50) and pairing (100) that calls `pmacs.hook.run("buffer.after-edit")`
re-enters the expander's subscriber while the OUTER chain is still
mid-list; the nested pass expanded and outer pairing then resumed with
an invalidated record — `α(` again, through the chain's documented
re-entrancy seam instead of through claiming. **Deferring work past a
fan-out means owning which fan-out it belongs to.** The chain's
subscriber and the expander's each run exactly once per fan-out, so
counting the first and matching it off in the second identifies the
nesting level with no new seam in merged Stage 4a substrate.
- **Round 12 found round 11's counter in the wrong place.** It counted
invocations of the EXPANDER, which is optional: a lower-priority
consumer can claim and stop the chain before the expander runs, while
that fan-out's deferred subscriber still runs — so the nested pass
went uncounted, looked outermost, expanded early, and outer pairing
resumed with an invalidated record. The count now comes from a no-op
consumer at the MINIMUM priority, which runs first in every chain
invocation that reaches any consumer, and degrades safely: the only
thing that can skip it is a claim ahead of it, which skips the
expander too. A subscriber registered beside `run_deferred` cannot
serve — the whole nested fan-out completes inside the outer chain's
subscriber, before it would run.
- **Rounds 10–12 share a shape worth naming.** Each fix was correct
about the failure it was shown and wrong about the boundary of the
mechanism it leaned on — first the chain's copy semantics, then its
re-entrancy, then its short-circuit. **A queue that outlives the
thing that filled it has to name that thing, not approximate it.**
- Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED,
named in the module header (Q#LN21): six source-peer optimistic
inserts replaced by one daemon-peer op. `set_round_trip_input` would
fix it and also disables `dispatch_idle`, so RET would stop inserting
a newline.
## The CRDT half of the test corpus is dark in CI — NEEDS A LANE

58
docs/agent-handoff.md
View File

@ -37,7 +37,8 @@ commands, read `docs/active-work.md` immediately after this file.
## 1. Where the project stands (2026-07-26)
- `main` @ `a27f646` (Lean 4 Stage 4a #179 atop bottom-panel Stage 2A
- `main` @ `74301d1` (the dired Stage 1 landed-doc refresh #169 atop
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
@ -101,9 +102,9 @@ 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 (typed-edit consumer chain) MERGED as #179** (`main` @
`a27f646`, two review rounds). 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 +118,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) is implemented and in review**
(branch `lean4-stage4b-input-method`, 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

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

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()

137
src/daemon.rs
View File

@ -3964,6 +3964,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

21
src/editor.rs
View File

@ -445,6 +445,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"),

1020
tests/lean_input_acceptance.rs Normal file
View File

File diff suppressed because it is too large Load Diff