From 3b54c784949847bd47b7b03f2ce91da2453cb88f Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:10:06 -0400 Subject: [PATCH 1/7] =?UTF-8?q?docs(lean4):=20rev=206=20=E2=80=94=20re-sco?= =?UTF-8?q?ut=20Stage=204=20and=20split=20it=20into=204a=20and=204b?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against main @ d400f30 produced six findings that change the plan and three that confirm it. The pmacs-side facts were verified in a worktree at that commit; the upstream facts by reading leanprover/vscode-lean4 @ 17d1d08. The split: Stage 4's risk column read "refactors pair.lua's provenance read" — every language's auto-pairing — for a stage the prose called the Lean input method, which is exactly the rule §4 states and exactly what round 4 found for Stage 3. Rev 5 had noticed the shape and answered it with a commit boundary; a commit boundary is not a review boundary. Stage 4a is now the typed-edit consumer chain (substrate, no Lean) and 4b the input method. Rev 5's expansion semantics were wrong in three ways. Resolution is the shortest key having the input as a prefix (\al yields ∀ from `all`, not `alpha`); there is no terminator list at all ('+ ' is a key, so space extends after \+; '\' is a key, so \\ yields \); and an unmatchable tail is appended rather than dropped (\alp7 yields α7). Three further findings. There is no cursor-motion hook, so acceptance 43 as written was not buildable and abandonment is lazy. dispatch_key is only half of 4b's production path — \ and the letters are not excluded from the optimistic classifier, and that producer is crdt-gated, so a crdt-gated integration test is dark in CI and dark in the gate list. And the whole expansion has cross-peer-degraded undo, a wider bite than Q#LN6's three bracket pairs; set_round_trip_input would fix it and is rejected with reasons. New decisions Q#LN21 (undo degradation) and Q#LN22 (the state machine); Q#LN10 and Q#LN11 rewritten; §2.11 records the upstream algorithm; §9.1 states the coherence impact for both stages. Acceptance keeps its existing numbers and adds letter suffixes on both sides of the split. Citation sweep per COHERENCE §25: five live citations moved in the 50 commits since rev 5. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 73 +++- docs/lean4-mode-framing.md | 703 +++++++++++++++++++++++++++++++------ 2 files changed, 667 insertions(+), 109 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index e4f0859..52d44ba 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -14,11 +14,13 @@ backlog. machine-local: `origin` may name this canonical URL, a release mirror, or something else, and therefore has no authority by name alone. - Canonical base at this snapshot: - `githubsucks/main` @ `d152120` (the bottom-panel landed-doc refresh #156 - atop the inline-math slice #158, dired Stage 1 #165, the GPU terminal - input fix #166, Lean 4 Stage 2 #161, the dired framing #164, - COHERENCE.md #163, find-file #162, Lean 4 Stage 1 #160, and the minimap - blank-slab fix #159; protocol v20). + `githubsucks/main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a + #167, the bottom-panel landed-doc refresh #156, the inline-math slice + #158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 + Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file + #162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159; + protocol v20). The previous snapshot named `d152120`; the recovery + check below accepts it or anything newer. - On the transfer source, `origin/main` named a release mirror at `d3fa632` and lagged badly. On the current destination, `origin` names the canonical URL. This difference is why all recovery begins by @@ -55,7 +57,7 @@ git status --short --branch The `git log` command must expose `d152120` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED +## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING - Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review round, all twelve checks green). Branch `githubsucks/lean4-stage1` @@ -189,7 +191,7 @@ If it does not, stop and repair the remote/fetch configuration. suites**; `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` and `-- --skip basedpyright`. -### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`) +### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`) - Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @ `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first @@ -253,7 +255,7 @@ If it does not, stop and repair the remote/fetch configuration. `#[cfg(unix)]` is NOT sufficient for such a fixture — `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. -### Stage 3b — the Lean language server (branch `lean4-stage3b-server`) +### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`) - Same worktree `../pmacs-lean-stage3`, **branched off `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response @@ -463,6 +465,61 @@ If it does not, stop and repair the remote/fetch configuration. describes the pushed tree; recording it late is the #161 fmt-blocker error in a slower form.) +### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) + +- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** + (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main + that had advanced 50 commits mid-review; the only conflict either time + was this ledger's own lane headings, resolved by keeping both sides. +- Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. + Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No + code. Awaiting user approval before implementation, per the workflow. +- **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`, **93** are multi-codepoint. +- 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. +- Verification: none yet — the branch carries no code. `git diff --check` + clean. + ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) - Approved framing: `docs/dired-framing.md` **revision 6** — rev 5 is the diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index ec62980..e39eb36 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -6,7 +6,7 @@ pmacs has no Lean support of any kind: `grep -rin lean` over `*.rs`, plain buffer — no grammar, no major mode, no comment syntax, no pair set, no server. -This lane closes that in eight stages. Stage boundaries are drawn where +This lane closes that in nine stages. Stage boundaries are drawn where the *substrate* changes, not where the feature list does — see §4. §9 states the lane's coherence impact per `COHERENCE.md` §20. @@ -21,11 +21,12 @@ the *substrate* changes, not where the feature list does — see §4. #144 (LaTeX), #146 (HTML+CSS). Stage 1 is that pattern almost exactly. - Stages 2 and 4–6 are **not** that pattern, and none should be mistaken for a one-liner. Stage 2 changes `ensure_server`, shared by every LSP - language. Stage 4 builds the editor's first input method. Stage 5 is the + language. Stage 4a changes how typed-character provenance is consumed + and Stage 4b builds the editor's first input method. Stage 5 is the first consumer of a non-standard LSP method family. Stage 6 adds a severity-routing policy to `LspServerSpec`. - The user's stated north star is **matching or exceeding what VS Code - does with Lean**. §5's bet 6 scores honestly how close the eight stages get + does with Lean**. §5's bet 6 scores honestly how close the nine stages get and names precisely what is still missing. Parallel-safety: Stage 1 touches `Cargo.toml`, `src/syntax.rs`, @@ -283,10 +284,131 @@ rather than a bare root), `ensure_server` 527 → **610**, pre-#161 line numbers inside Q#LN15 are left as written: that stage has landed and its citations are historical record, not navigation. +### Round 5 (rev 5 → rev 6) — Stage 4 re-scout and split + +Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main` +@ `d400f30` produced **six findings that change the plan** and three +that confirm it. The pmacs-side facts were verified in a worktree at +that commit; the upstream facts were verified by downloading and reading +`leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the +algorithm, not its documentation, since the `lean4-unicode-input` +package ships no README. + +1. **Stage 4 violated this document's own splitting rule — the same way + Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting + substrate change with Lean feature content," and §4's own risk column + for Stage 4 read *"refactors `pair.lua`'s provenance read."* + `pair.lua` is every language's auto-pairing; the refactor is + cross-cutting substrate by exactly the test that split out stages 2 + and 3a. Rev 5 already conceded the shape without acting on it — + Q#LN10 said the refactor "lands *first*, as its own commit with no + behavior change, so a regression bisects cleanly." A commit boundary + is not a review boundary. **Stage 4 is now 4a (the typed-edit + consumer chain, no Lean) and 4b (the input method).** Confirmed + `pair.lua:226` is still the **only** production `take_typed_edit` + caller; the other eight call sites are all in + `tests/auto_pair_acceptance.rs`. +2. **The expansion semantics in rev 5's Q#LN10 were wrong in three + ways.** Reading `AbbreviationProvider.ts` and `TrackedAbbreviation.ts` + rather than inferring from behavior: + - Rev 5 said expansion fires on "a unique complete match that no + longer key extends." Upstream's rule is + `findSymbolsByAbbreviationPrefix(abbrev)[0]` — the symbol of the + **shortest key having `abbrev` as a prefix**. `\alp` + space is not + a failure; it yields `α`, because `alpha` is the shortest key + starting with `alp`. Verified against the table: `\al` → `∀`, from + `all`, not from `alpha`. + - Rev 5 named "an explicit terminator (space, tab, RET, or a second + `\`)." **There is no terminator list upstream.** A character + terminates iff extending the pending key by it leaves zero prefix + matches. Space usually does — but `'+ '` **is a key** (one of + 1,855), so after `\+` a space extends rather than terminates. And a + second `\` is not a terminator either: `'\'` is a key mapping to + `\`, so `\\` extends, matches uniquely, and expands to a single + backslash. It terminates only when the pending key is non-empty and + no key extends it. + - Rev 5 did not carry the suffix rule at all. When no key has + `abbrev` as a prefix, upstream recurses on `abbrev` minus its last + character and **appends the leftover**: `\alp7` → `α7`. Dropping + this makes a large class of real input silently unexpandable. +3. **There is no cursor-motion hook, so acceptance 43 as written cannot + be built.** The Rust core fires exactly eight named hooks + (`builtin/hooks/default.lua`): `buffer.before-save`, + `buffer.after-load`, `buffer.after-edit`, `buffer.after-switch`, + `buffer.after-save`, `editor.before-quit`, `frontend.detached`, + `process.after-tick`. Upstream drives abandonment off + `changeSelections`, a seam pmacs does not have. Abandonment must + therefore be **lazy** — validated at the next typed edit against the + pending region — which changes what acceptance 43 can assert. Q#LN22 + states the state machine this forces. +4. **`dispatch_key` is only half of Stage 4b's production path.** Rev 5 + inherited the auto-pairing suite's dispatch-driven harness without + noticing why that harness is sufficient *there*: Q#AP1 removed the + pair characters from both optimistic classifiers, so for pair chars + dispatch **is** production. `\` and the ASCII letters are not + excluded — `classify_key` returns `Insert(c)` for them + (`src/optimistic.rs:144`: `Char(c) if !c.is_control() && + !is_builtin_pair_char(c)`), so on a CRDT frontend an abbreviation is + typed entirely through the *optimistic* producer, which arms the same + record from `handle_remote_crdt_op` (`src/daemon.rs:3965` pins the + classification). A dispatch-only Stage 4b suite would pin the path + real users do not take. The trap underneath: that producer is + `#[cfg(feature = "crdt")]`, and CI never enables `crdt` — so a + crdt-gated integration test is dark twice over, since the required + gate list runs `--features crdt` only for `--lib`. Q#LN22 and §7 say + what to do about it instead of discovering it in review. +5. **The whole expansion has cross-peer-degraded undo, and it is a + larger bite than `⟨⟩`'s.** Q#LN6 already accepts this for three + bracket pairs. But there the mismatch is one optimistic opener + against one daemon-peer closer; here the user's `\alpha` is six + source-peer optimistic inserts and the expansion is a single + daemon-peer `replace` **over all six**. Q#LN21 takes the decision — + including why `pmacs.buffer.set_round_trip_input`, which already + exists and would fix it, is the wrong instrument. +6. **The table's shape is sharper than "1,855 entries."** Re-counted at + `17d1d08`: 1,855 entries, all `string → string`, **all keys ASCII**, + longest key 25 characters, 36,861 bytes of JSON. **64** keys contain + a `lean4` pair-set character (rev 5's number, reproduced exactly). + Three numbers rev 5 did not have and the algorithm needs: **305** + keys are proper prefixes of another key (so 1,550 are eager-expandable + on uniqueness and 305 are not), **26** values carry `$CURSOR` (not + just `\<>`), and **93** values are multi-codepoint. Two values contain + a backslash — `n` → `\n` and `setminus` → `\` — which is why upstream + needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs + does not. + +Confirmations, recorded because each was load-bearing and unverified: + +7. **`take_typed_edit`'s one-shot contract is unchanged** + (`src/editor_core.rs:4047`): per-frontend, cleared by the producer + when the fan-out returns, nil to a nested manual `hook.run`. The + hazard rev 5 built Q#LN10 around is real and still the reason 4a + exists. +8. **Load order still constrains the chain.** `pair.lua` loads at + `src/editor.rs:430` and `lsp.lua` at `:436`, and Q#AP7's reason + holds: `lsp.lua`'s `buffer.after-edit` callback synchronously flushes + `didChange` on the signature-trigger path. An expansion that landed + after that flush would send the server the unexpanded text. +9. **Embedding the table needs no special machinery.** Every builtin + runtime chunk is an `include_str!`, and `lsp.lua` is already 111 KB + of the 414 KB total. A ~45 KB generated Lua table is within the + existing practice, so Q#LN11 embeds it rather than inventing a + lazy-load path. + +Citation drift repaired per COHERENCE §25, on the same terms as round +4's sweep. Five live citations moved in the 50 commits since rev 5: +`take_typed_edit` 12827 → **12990**, `handle_server_requests` 1549 → +**1815**, `fs.stat` 93 → **133**, `detect_buffer_language` 452 → +**457**, and `send_request`/`send_notification` 9342/9361 → +**9507**/**9527**. Left as written: the pre-#161 numbers inside Q#LN15 +and the revision-history entries above, which are historical record +rather than navigation. + ## 1. What ships -Eight stages, after round 4 split Stage 3. The north star is VS Code -parity; the honest statement of where that lands is in §5, bet 6. +Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The +north star is VS Code parity; the honest statement of where that lands +is in §5, bet 6. **Stage 1 — grammar, mode, and the editing table stakes.** `.lean` files highlight, carry a `lean4` major mode, and get comment-toggle and @@ -315,10 +437,19 @@ on 3a's seam. Adds `textDocument/waitForDiagnostics`. Diagnostics, hover, completion, goto-definition, document symbols, and semantic tokens all arrive through the existing typed surfaces. -**Stage 4 — the Unicode input method.** Typing `\alpha` produces `α`, +**Stage 4a — the typed-edit consumer chain.** Pure substrate, no Lean +content, split from Stage 4 in round 5 for the reason stages 2 and 3a +were: it changes machinery every language runs through. The one-shot +`take_typed_edit()` record stops being auto-pairing's private property +and becomes a small ordered chain that reads it once and offers it to +registered consumers. `pair.lua` becomes the chain's first and only +consumer, with no behavior change. + +**Stage 4b — the Unicode input method.** Typing `\alpha` produces `α`, `\to` produces `→`, `\<>` produces `⟨⟩` with the point between them. -1,855 abbreviations vendored from vscode-lean4. This is the stage that -makes Lean actually typable in pmacs. +1,855 abbreviations vendored from vscode-lean4, registered as a chain +consumer ahead of auto-pairing. This is the stage that makes Lean +actually typable in pmacs. **Stage 5 — the goal view.** A `*lean-goal*` panel that renders `$/lean/plainGoal` at the point, refreshed on a debounced tick and on @@ -405,7 +536,7 @@ injections_query }`. Adding a grammar is one entry plus one `Cargo.toml` line; the doc comment at `src/syntax.rs:756` says exactly this and it has held for every grammar since. -`builtin/runtime/syntax.lua:452` `detect_buffer_language` resolves, in +`builtin/runtime/syntax.lua:457` `detect_buffer_language` resolves, in order: modeline → `pmacs.parse.language_for_path` (the grammar extension table) → `pmacs.lsp.filetypes[ext]` → `pmacs.parse.language_from_filename` → shebang. A grammar entry claiming `lean` therefore resolves `.lean` @@ -486,13 +617,13 @@ and pin it.* - `pmacs.lsp` already exposes generic `send_request(id, method, params)` → request id and `send_notification(id, method, params)` - (`src/lua_bindings/mod.rs:9342`, `:9361`). Non-standard methods need no + (`src/lua_bindings/mod.rs:9507`, `:9527`). Non-standard methods need no new Rust to *send*. - `LspEventKind` (`src/lsp.rs:264`) has generic `Notification { method, params }` and `Response { id, result, error, method }` variants. Unknown server methods are delivered, not dropped. - **But `events_take` has exactly one consumer**: `handle_server_requests` - at `builtin/runtime/lsp.lua:1549`, driven off `pmacs._async.tick`. It + at `builtin/runtime/lsp.lua:1815`, driven off `pmacs._async.tick`. It `take`s — a drain. Its `if/elseif` chain handles five `request` methods and `initialized`, and **ignores every `notification` and every `response`**. A second module calling `events_take` would steal events @@ -556,7 +687,7 @@ character": subscribe to `buffer.after-edit`, gate on `ed.this_command() == "buffer.self-insert"` (`pair.lua:229`), then take the exact provenance record. -`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12827`) returns +`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12990`) returns `{ buffer, window, codepoint, char, requested_start, requested_end, effective_start, effective_end, inserted_len, post_cursor, clean }` — or nil. Its doc comment is explicit: @@ -570,7 +701,19 @@ it on every self-insert. A Lean abbreviation expander that independently calls `take_typed_edit()` in the same `buffer.after-edit` fan-out gets nil or steals it from auto-pairing, depending on hook order — and hook order is not a contract. This is the single load-bearing constraint on Stage 4 and -the reason Stage 4 is its own PR rather than a rider on Stage 1. +the reason Stage 4 is its own PR rather than a rider on Stage 1 — and, +after round 5, the reason its substrate half is Stage 4a rather than a +first commit on a Lean branch. + +Re-verified at `d400f30`: `pair.lua:226` remains the **only** production +caller. The eight other call sites in the tree are all in +`tests/auto_pair_acceptance.rs`. So the chain Stage 4a introduces has +exactly one consumer to migrate, which is what makes a no-behavior-change +substrate PR possible at all. + +Two producers arm the record, not one, and §2.11 is where that matters: +the dispatch fallback and — under `#[cfg(feature = "crdt")]` — the +optimistic CRDT arm reached from `handle_remote_crdt_op`. Related, from `pair.lua:30`'s Q#AP1 note: only the nine built-in pair chars `()[]{}"'` and backtick are excluded from the frontends' optimistic @@ -680,6 +823,78 @@ The publish path absorbs into the Rust store *and* still delivers the notification to `events_take`, so Lua can observe them; but suppressing them from the store needs a Rust-side policy, not a Lua filter. Q#LN18. +### 2.11 The upstream input method (external, verified by reading it) + +Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`, +package `lean4-unicode-input`, files `AbbreviationProvider.ts`, +`TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`, +`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no +README, so the algorithm below is read off the source. Apache-2.0. + +**Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key +having `p` as a prefix, sorts them by **key length ascending**, and maps +to symbols. `getReplacementText(a)`: + +1. If any key has `a` as a prefix, return the shortest such key's symbol. +2. Otherwise recurse on `a` minus its last character; if that yields + something, return it **with the dropped character appended**. +3. Otherwise undefined — no expansion. + +Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`), +`al` → `∀` (via `all`, *not* `alpha` — shortest wins, and this is +surprising enough to be worth an acceptance criterion), `alp7` → `α7` +via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches). + +**Tracking.** The leader `\` is inserted into the buffer like any other +character, and the tracked range starts after it; the replaced range +spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the +buffer literally shows `\alpha` until expansion, then that whole span +becomes `α`. + +**Termination.** There is no terminator set. On each typed character +`c`, if `findSymbolsByAbbreviationPrefix(a .. c)` is empty the +abbreviation is marked `finished`, **`c` is not absorbed into it**, and +the pending text expands before `c` lands. Otherwise `c` extends the +key. Two consequences the obvious "space ends it" model gets wrong: + +- `'+ '` is a key, so after `\+` a space **extends**. Space is a + terminator by consequence, never by rule. +- `'\'` is a key (→ `\`), so `\\` extends, is uniquely complete, and + eagerly expands to one backslash. A second `\` terminates only when + the pending key is non-empty and unextendable — at which point the + rewriter starts a *new* tracked abbreviation on it. + +**Eager expansion.** When `eagerReplacementEnabled`, an abbreviation +expands the moment it is *unique and complete*: exactly one key has it +as a prefix, and it is itself a key. 1,550 of the 1,855 keys qualify; +the other 305 are proper prefixes of some other key and must wait for +termination. `\to` is in the first group — it expands with no terminator +typed, which is why acceptance 41 is meaningful and not a restatement of +38. + +**Cursor placement.** `$CURSOR` is stripped from the symbol and its +index becomes the post-expansion point, applied only when the point sat +at the end of the abbreviation. 26 values carry it. + +**Abandonment.** Upstream expands on `changeSelections` — any tracked +abbreviation the cursor has left. pmacs has no cursor-motion hook +(round-5 finding 3), so this seam does not exist here and Q#LN22 makes +abandonment lazy instead. + +**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` → +`\n`, so an expansion can insert a backslash; upstream sets +`doNotTrackNewAbbr` across the replace so that backslash does not open a +new abbreviation. In pmacs the expansion is a programmatic `buf:replace` +that arms no typed-edit record, so the chain sees nothing and cannot +re-arm. The guard is unnecessary here **because of** the provenance +contract, not by accident — and the acceptance must pin it, because a +future consumer that inferred from buffer text rather than provenance +would reintroduce the bug. + +**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a +`Set` and sorts changes bottom-up for that reason; +pmacs has one point, so one pending abbreviation per buffer. + ## 3. Decisions ### Q#LN1 — Bundle `arborium-lean` 2.18; reject `tree-sitter-lean4` @@ -911,7 +1126,7 @@ file's directory. **How the walk tests for the marker — and why not the obvious way.** `pmacs.fs.stat` is asynchronous: it returns an awaitable handle -(`builtin/runtime/fs.lua:93`) that only settles under `:await()` inside a +(`builtin/runtime/fs.lua:133`) that only settles under `:await()` inside a coroutine. The resolver has no coroutine. It runs synchronously inside `ensure_server` ← `attach_buffer` ← the `buffer.after-load` hook, so awaiting is not merely slow there, it is unavailable — and blocking the @@ -1102,86 +1317,192 @@ The binding is general, not Lean-shaped: it serves every future function-valued `root`, and it is what lets #161's doc comment stop warning about a footgun and start naming a fix. -### Q#LN10 — Stage 4 mechanism: one shared provenance read, not two +### Q#LN10 — Stage 4a: one shared provenance read, not two The hazard is §2.6 — `take_typed_edit()` is one-shot and `pair.lua` -already consumes it. +already consumes it. A second independent caller in the same +`buffer.after-edit` fan-out gets nil or steals the record, depending on +hook order, and hook order is not a contract. Decision: **`pair.lua` stops being the sole consumer.** Extract the provenance read into a single `buffer.after-edit` subscriber owned by a -small shared module, which takes the record once and passes it to an -ordered list of typed-edit consumers (auto-pair, Lean abbreviation). -Consumers return whether they handled the edit; the first that does stops -the chain. +small shared module — `builtin/runtime/typed_edit.lua`, loaded +immediately before `pair.lua` — which takes the record once and offers +it to registered consumers in a defined order. A consumer returns +whether it **claimed** the edit; the first that claims stops the chain. -Two consequences worth stating up front: +`pmacs.typed_edit.add_consumer { name = , priority = , +fn = function(rec) ... end }`, lowest priority first, ties broken by +registration order. Priority is an explicit number rather than +load-order-implied because Q#LN22's collision makes ordering +load-bearing, and rev 5's "the abbreviation consumer runs first" is a +claim a reader must be able to check without reconstructing +`src/editor.rs`'s include list. -- This touches `pair.lua`, which is load-bearing for auto-pairing - acceptance. The full pairing suite is a required gate for Stage 4, and - the refactor lands *first*, as its own commit with no behavior change, - so a regression bisects cleanly. -- Ordering is a contract, not an accident, and the collision is real: - **64 of the 1,855 abbreviation keys contain a character in the proposed - `lean4` pair set** — `\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`, - `\{}` → `{$CURSOR}`. With pairing first, typing `\[` inserts `[]` - with the point between, so the pending key is corrupted to `\[]` before - the second `[` is ever typed and `\[[]]` becomes unreachable. The - abbreviation consumer runs first. +**Stage 4a ships this and nothing else.** Its whole content is: +`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer, +and the `include_str!` line. Round 5's finding 1 is why this is a PR and +not a first commit — `pair.lua` is every language's auto-pairing, and a +reviewer looking at a Lean PR should not have to also review a rewrite +of it. - (Rev 1 justified this with `\<>`, which was wrong: `<` is not in the - pair set per Q#LN6, so that key is safe under either order.) +**The no-behavior-change claim must be pinned, not asserted.** The full +`tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must +pass **unmodified** — a suite edited to accommodate the refactor proves +nothing (the recorded lesson: what a test suite pins is its assertions). +Three assertions the existing suite already makes are the load-bearing +ones, because they are what a chain could plausibly break: that a second +`take_typed_edit()` in the same fan-out yields nil, that pairing still +sees the exact record via `_capture_records`, and that the Q#AP7 ordering +against `lsp.lua`'s `didChange` flush still holds. -**The contract that collision exposes:** the abbreviation consumer must -claim a self-insert that **extends an open pending abbreviation**, not -only one that completes an expansion. A consumer that only claims -completed expansions hands every intermediate keystroke to auto-pairing, -which is exactly how `\[` gets corrupted. "Claimed" here means the chain -stops, not that an edit was made. +**What 4a deliberately does not do.** It does not change the `all-must- +succeed` contract, so a consumer that throws still fails the fan-out for +everyone. The chain owner therefore `pcall`s each consumer and reports +through `pmacs.editor.set_status`, matching `pair.lua`'s existing +never-throw-from-after-edit discipline — this is behavior-preserving for +pairing (which already never throws) and is the guardrail 4b needs. -Expansion semantics (matching vscode-lean4 and `lean4-input`): - -- `\` opens a pending abbreviation, tracked per buffer with its start - offset. Every subsequent self-insert that extends it is claimed. The - pending state is abandoned on any non-self-insert command, buffer - switch, or cursor move away from the pending region. -- Expansion fires on a unique complete match that no longer key extends, - or on an explicit terminator (space, tab, RET, or a second `\`). -- The vendored table's `$CURSOR` placeholder becomes the point position - after the replace — this is how `\<>` yields `⟨|⟩`. -- The whole expansion is **one `buf:replace`** — one undo step, one CRDT - op, one effective-edit verification. Same discipline as - `comment.lua`'s Q#CT5. -- Gated by `pmacs.config.define{ name = "lean.abbrev", type = "boolean", - default = true, mutability = "live" }`, read against the *source* buffer - of the typed edit — the `editing.auto-pair` precedent (`pair.lua:44`), - including its round-2 correction to resolve `rec.buffer` rather than - `pmacs.window.buffer()`. - -### Q#LN11 — Stage 4 data: vendor the table, generated, attributed +### Q#LN11 — Stage 4b data: vendor the table, generated, attributed `abbreviations.json` in `leanprover/vscode-lean4` is a flat -`string → string` object of **1,855 entries** (counted, not estimated), -of which **64 contain a character in the `lean4` pair set** — the -collision Q#LN10's ordering exists to handle. vscode-lean4 is Apache-2.0. +`string → string` object of **1,855 entries**, verified at commit +`17d1d08` (2026-05-29), 36,861 bytes, all keys ASCII, longest key 25 +characters. The counts the algorithm depends on, all re-derived from the +file rather than estimated: + +| Count | What it drives | +|---|---| +| 64 keys containing a `lean4` pair-set char | Q#LN22's ordering | +| 305 keys that are proper prefixes of another | which keys can expand eagerly | +| 1,550 keys uniquely-and-completely matching | the eager-expansion set | +| 26 values containing `$CURSOR` | point placement | +| 93 multi-codepoint values | the replace is not one-char-for-many | + +vscode-lean4 is Apache-2.0. Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header -recording source repo, commit, license, and the regeneration command — -the `builtin/queries/latex/highlights.scm` precedent (#144) for -third-party data, extended with provenance because this is a much larger -artifact under a named license. +recording source repo, commit, license, entry count, and the +regeneration command — the `builtin/queries/latex/highlights.scm` +precedent (#144) for third-party data, extended with provenance because +this is a much larger artifact under a named license. -Not fetched at runtime, not a package-manager dependency: the input method -must work offline and on first launch. +Not fetched at runtime, not a package-manager dependency: the input +method must work offline and on first launch. -**Upkeep is a documented manual process, not code.** There is no automatic -sync and none is wanted — an editor that silently re-downloads its input -method has a supply-chain problem, not a feature. The generator script -lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit as its -argument, and rewrites the file including its provenance header. The -header records source commit, license, entry count, and the regeneration -command, so the file is self-describing to whoever next touches it. A -refresh is an ordinary PR with a visible diff — which is the point: the -diff is the review. +**Embedded, not lazily loaded.** ~45 KB of generated Lua joins the 414 KB +of builtin runtime already compiled in by `include_str!`, of which +`lsp.lua` alone is 111 KB. Inventing a lazy-load path for an 11% increase +would be new machinery bought with no measurement, and the arithmetic is +stated here so a reviewer can disagree with it on numbers. + +**Upkeep is a documented manual process, not code.** There is no +automatic sync and none is wanted — an editor that silently re-downloads +its input method has a supply-chain problem, not a feature. The generator +script lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit +as its argument, and rewrites the file including its provenance header, +so the file is self-describing to whoever next touches it. A refresh is +an ordinary PR with a visible diff — which is the point: the diff is the +review. + +**The generator must reject a table it cannot faithfully encode.** Keys +are ASCII today but nothing upstream promises that; a key containing a +character the emitted Lua would have to escape, or a duplicate after +normalization, aborts the regeneration rather than silently emitting a +table that disagrees with its source. Same discipline as Q#LN20's +refusal to hand back a lossy path. + +### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it + +`classify_key` (`src/optimistic.rs:144`) returns `Insert(c)` for `\` and +for every ASCII letter — only the nine built-in pair chars are excluded +(Q#AP1). So on a CRDT frontend the user's `\alpha` arrives as six +**source-peer** optimistic inserts, while the expansion is a single +**daemon-peer** `buf:replace` spanning all six. Undo across that boundary +is not chronologically arbitrated; this is the same defect Q#LN6 already +accepts for `⟨⟩`, `⦃⦄`, `⟮⟯`, one order of magnitude wider. + +Considered and rejected: `pmacs.buffer.set_round_trip_input(buf, true)`, +which exists, is per-buffer, and would fix this exactly. Its six current +callers are all read-only generated buffers — listview, compile, dired, +terminal — and it does considerably more than disable optimistic insert: +per `src/editor_core.rs:505`, `dispatch_idle` reports false, so RET +reaches buffer-local bindings instead of inserting a newline. Turning it +on for every ordinary editable Lean source file would trade a known undo +degradation for an unknown behavior change across the whole editing +surface, and would make Lean the one language whose typing has a +different latency profile. + +Also rejected: adding `\` to the always-round-trip set. It is +frontend-side and language-blind, so this would tax LaTeX, C, shell, and +every string literal in the editor to fix one language. + +Decision: **accept the degradation, name it in the module comment, and +do not paper over it.** The general fix is chronological cross-peer undo +arbitration — already on the standing backlog, and the same fix Q#LN6 +points at. What Stage 4b owes is honesty about scope: this is not "a few +brackets," it is every abbreviation the user types on a CRDT frontend. + +### Q#LN22 — Stage 4b mechanism: lazy abandonment, explicit ordering + +**Ordering.** The abbreviation consumer registers ahead of auto-pairing. +The collision is real: 64 keys contain a `lean4` pair-set character — +`\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`, `\{}` → `{$CURSOR}`. +With pairing first, typing `\[` inserts `[]` with the point between, so +the pending key is corrupted to `\[]` before the second `[` is typed and +`\[[]]` becomes unreachable. + +(Rev 1 justified this with `\<>`, which was wrong: `<` is not in the pair +set per Q#LN6, so that key is safe under either order.) + +**The contract the collision exposes:** the consumer must claim a +self-insert that **extends an open pending abbreviation**, not only one +that completes an expansion. A consumer that claims only completed +expansions hands every intermediate keystroke to auto-pairing, which is +exactly how `\[` gets corrupted. "Claimed" means the chain stops, not +that an edit was made. + +**State machine**, per §2.11's ground truth rather than rev 5's +reconstruction of it: + +- `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, + start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`. +- 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`. +- Expansion resolves through §2.11's three-rule `getReplacementText`, + including the suffix rule (`\alp7` → `α7`). +- `$CURSOR` is stripped from the symbol and its index becomes the point. + +**Abandonment is lazy, because there is no cursor-motion hook** (round-5 +finding 3). Pending state is validated at the next typed edit and +discarded when any of these no longer holds: the record's buffer is the +pending buffer; `rec.effective_start` equals `start_offset + 1 + +#text` (the point is still at the end of the pending span); and the +buffer's `revision()` advanced by exactly the pending edit. `buffer. +after-switch` clears it eagerly since that hook *does* exist. The +practical difference from upstream: a user who clicks away mid-`\alp` +and types elsewhere gets the pending state dropped rather than expanded. +Upstream expands it. **This is a deliberate divergence** — expanding +into a region the user has left is the worse failure, and pmacs cannot +detect the departure at the moment it happens. + +**One `buf:replace`** for the whole expansion — one undo step, one CRDT +op, one effective-edit verification, with the same +rejected/altered-by-intercept reporting as `comment.lua`'s Q#CT5 and +`pair.lua`. A rejection drops the pending state; it does not retry. + +**Gate:** `pmacs.config.define{ name = "lean.abbrev", type = "boolean", +default = true, mutability = "live" }`, read against the **source** +buffer of the typed edit — the `editing.auto-pair` precedent +(`pair.lua:46`), including its round-2 correction to resolve +`rec.buffer` rather than `pmacs.window.buffer()`. + +**Language gate:** the consumer opens no pending abbreviation outside a +`lean4` buffer, resolved from `rec.buffer` for the same reason. `\` in a +Rust buffer is an ordinary character and `\[` there still pairs. ### Q#LN12 — Stage 5 sends `$/lean/plainGoal` through a typed Rust request @@ -1418,13 +1739,14 @@ never lands. | 2 | multi-root server affinity | **`ensure_server`, shared by every language** | — | | 3a | notification/response seams + purge; `pmacs.fs.canonicalize` | **the shared event drain, run by every language** | — | | 3b | `lake serve` + probe/latch, Lake root, `waitForDiagnostics` | none — Lean-only files plus one config entry | 1, 2, 3a | -| 4 | Unicode input method | **refactors `pair.lua`'s provenance read** | 1 | +| 4a | typed-edit consumer chain | **refactors `pair.lua`'s provenance read, shared by every language** | — | +| 4b | Unicode input method | none — Lean-only files plus one chain consumer | 1, 4a | | 5 | goal panel | new typed LSP request; panel adopter | 3a, 3b | | 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3b, 5 | | 7 | module hierarchy | listview adopter + one typed Rust request | 3a, 3b | -Four of the eight carry risk that is *not* about Lean — stages 1, 2, 3a, -and 6 each change something every language touches. That is the +Five of the nine carry risk that is *not* about Lean — stages 1, 2, 3a, +4a, and 6 each change something every language touches. That is the organizing principle of the split: **no PR in this arc mixes a cross-cutting substrate change with Lean feature content.** A reviewer looking at Stage 2 sees only `ensure_server`; a reviewer looking at Stage @@ -1436,6 +1758,16 @@ Lean-only. One generalization shipped as Stage 2; extracting the other as 3a is what makes the claim true again. The rule is only worth writing down if it survives contact with a stage that is inconvenient to split. +Round 5 found the *same* rule broken again, by Stage 4, whose risk column +read "refactors `pair.lua`'s provenance read" — every language's +auto-pairing — for a stage described as the Lean input method. Rev 5 had +noticed the shape and answered it with a commit boundary; a commit +boundary is not a review boundary. Twice in two re-scouts is the +interesting part: **this rule is not self-enforcing, and a stage only +looks Lean-only until someone re-reads its own risk column.** Every +remaining stage should be re-checked against it at scout time, not +assumed. + Ordering notes: - **Stage 2 has no Lean in it and could ship independently of this arc.** @@ -1453,11 +1785,21 @@ Ordering notes: `builtin/runtime/lsp.lua`. Unlike stages 1 and 2, this pair is strictly sequential — recorded here, per the #126/#127 lesson, rather than discovered in a rebase. -- **Stage 4 does not depend on stages 2, 3a, or 3b** and could run in - parallel, but should not: both touch `lsp.lua`/`pair.lua`-adjacent - runtime files, and the #126/#127 lesson is that parallel-safety - requires the file split be agreed *before* either lane starts. - Sequential is cheaper. +- **Stage 4a depends on nothing in this arc** — not even Stage 1. It is + a pure runtime-substrate change whose only content is `pair.lua` and a + new module beside it, and it would be worth landing if the Lean arc + were abandoned tomorrow, because "the typed-edit record has exactly + one consumer forever" is not a property anyone chose. +- **4a and 4b cannot run as sibling worktrees**, for the 3a/3b reason: + 4b's consumer is written against the registration API 4a adds. Strictly + sequential, recorded before either starts. +- **Stage 4b depends on stages 1 and 4a and on nothing else** — not on + 2, 3a, or 3b. The input method is useful with no language server at + all, which is the honest ordering argument for putting it this early: + a user with no Lean toolchain installed still gets a Lean editor that + can type Lean. It could run in parallel with the 5/6/7 lane, but + should not, per the #126/#127 lesson that parallel-safety requires the + file split be agreed *before* either lane starts. - **Stage 6 depends on Stage 5** only for the read-only generated-buffer and panel machinery, which Stage 5 establishes. If Stage 5 slips, Stage 6 can carry that machinery itself at the cost of duplicating it. @@ -1496,7 +1838,22 @@ Stated so they can be scored, per house style. inside `buffer.after-edit` re-enters the hook in a way pairing does not already survive. Confidence: medium — pairing does the same thing, but over a single codepoint rather than a multi-byte span. -6. **These eight stages reach rough VS Code parity for everything except +5a. **Lazy abandonment is good enough without a cursor-motion hook** + (rev 6, Q#LN22). Falsified if a user in normal editing hits a case + where stale pending state produces a *wrong* expansion rather than a + dropped one — the failure mode this design chooses. Confidence: + medium-high, because every path that can invalidate the state either + goes through `buffer.after-edit` (where it is checked) or through + `buffer.after-switch` (where it is cleared), and the residual is a + cursor move with no intervening edit, which the next typed edit + catches by position. If it fails, the fix is a cursor-motion hook — + substrate work with its own framing, not a patch to this stage. +5b. **Stage 4a is behavior-preserving.** Falsified by any change to + `tests/auto_pair_acceptance.rs` being needed to make it pass. + Confidence: high, and cheap to score — it is a diff-level check, not + a judgment call. This bet is stated separately from bet 5 because it + is the one a reviewer can falsify in ten seconds. +6. **These nine stages reach rough VS Code parity for everything except the interactive infoview.** Scored honestly rather than aspirationally. What lands: highlighting, goal view, Unicode input, diagnostics, hover, completion, goto-definition, symbols, semantic tokens, `#eval` @@ -1528,10 +1885,26 @@ What remains deferred: - **GPU goal band** — blocked on bottom-panel Stage 2 (Q#LN14). The panel is grid-only until then. - **A `cursor.after-move` hook** — there is none (Q#LN13), so Stage 5 - polls off `process.after-tick`. A real motion hook would serve the goal - view, `completion.lua`'s cursor-delta heuristic, and the outline/hover - panels alike; it is substrate work that should not be invented inside a - language lane. + polls off `process.after-tick` and Stage 4b abandons pending + abbreviations lazily rather than on departure (Q#LN22, round-5 finding + 3). A real motion hook would serve the goal view, the input method, + `completion.lua`'s cursor-delta heuristic, and the outline/hover panels + alike; it is substrate work that should not be invented inside a + language lane. Two consumers in this arc now want it, which is worth + recording as evidence for whoever frames it. +- **Chronological cross-peer undo arbitration** — the general fix for + Q#LN6's bracket pairs and Q#LN21's abbreviation expansions alike. + Already on the standing backlog; named again here because Stage 4b + widens the exposure from three pair characters to every abbreviation a + user types on a CRDT frontend, which changes how often the existing + defect is met without changing what it is. +- **Per-buffer optimistic-apply policy** — the narrower thing Q#LN21 + actually wanted and did not build. `set_round_trip_input` is the only + existing lever and it is too blunt (it also changes RET dispatch); a + frontend-side, language-aware round-trip character set would fix the + undo degradation for Lean without taxing every other language, and + would retire Q#AP1's limitation too. Frontend + protocol work, so + Q#LN14's no-protocol-change rule keeps it out of this arc entirely. - **LSP server reaping / LRU** — Q#LN15's per-root affinity makes unbounded `lake serve` growth possible. No editor caps this by default and pmacs will not either in this arc, but the policy question is now @@ -1758,12 +2131,44 @@ revision take letter suffixes rather than displacing anything. Round 3's finding 4 was stale cross-references surviving a renumber; not renumbering is the cheaper way to not repeat it. -**Stage 4 — the Unicode input method** +**Stage 4a — the typed-edit consumer chain** -38. `\alpha` + space yields `α`; the whole expansion is a single undo step. +Criterion 46 keeps its number and moves here — it was always the +substrate pin, filed under Stage 4 only because Stage 4 was one stage. +Per the no-renumbering rule above, round 5's additions take letter +suffixes on both sides of the split. + +46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs` + suite passes **unmodified**. A suite edited to accommodate the + refactor proves nothing; the diff for 4a must show zero lines + changed in that file. +46a. The chain reads the record exactly once: with two consumers + registered, a `take_typed_edit()` from inside either observes nil, + and both consumers receive the *same* record fields. Bites against a + chain that re-takes per consumer (which would hand the second one + nil in production and pass a single-consumer test). +46b. Ordering is by declared priority, not registration order: two + consumers registered low-priority-last still run + low-priority-first. Bites against a chain that "works" only because + `include_str!` order happens to agree with intent. +46c. A claiming consumer stops the chain — a later consumer does not + run — and a non-claiming one does not. +46d. A consumer that throws is contained: the fan-out still succeeds, + the other consumers still run, and the failure reports through + `set_status`. Bites against the `all-must-succeed` contract taking + the whole fan-out down with one bad consumer (Q#LN10). +46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server + test — pairing's closer must be in the buffer before `lsp.lua` + flushes `didChange` — still holds with pairing behind the chain. + Falsified by moving the chain's registration after `lsp.lua`'s. + +**Stage 4b — the Unicode input method** + +38. `\alpha` + space yields `α`; the whole expansion is a single undo + step, and one undo restores `\alpha` rather than `\alph`. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. -40. **Pair-collision pin (Q#LN10).** `\[[]]` yields `⟦⟧`: each `[` is +40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is claimed as an extension of the pending abbreviation, so auto-pairing never inserts a closing `]` into the pending key. Bites against an ordering where pairing runs first, and against a consumer that claims @@ -1773,15 +2178,55 @@ renumbering is the cheaper way to not repeat it. 41. `\to` yields `→` eagerly on uniqueness, with no terminator typed. 42. A prefix with no match (`\zzzz` + space) is left as literal text; no edit is made. -43. Moving the cursor out of a pending abbreviation abandons it. +43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion + hook, this asserts what pmacs can actually detect: after `\alp`, an + explicit `goto_byte` elsewhere followed by typing `h` inserts a + plain `h` and leaves the `\alp` text untouched — the pending state + is dropped, not expanded. Plus: `buffer.after-switch` clears pending + state eagerly. **Rev 5's version of this criterion was not + buildable**; recorded so the change is visible rather than silent. 44. `pmacs.config.set("lean.abbrev", false)` disables expansion; the setting is read against the typed edit's **source** buffer. 45. Expansion does not fire in a non-`lean4` buffer — including that a pending abbreviation is never opened there, so `\[` in a Rust buffer still pairs normally. -46. **Provenance-refactor pin:** the full auto-pairing acceptance suite - passes unchanged, and a bite against the pre-refactor `pair.lua` - confirms the shared-consumer commit is behavior-preserving. +45a. **Shortest-key resolution (§2.11).** `\alp` + space yields `α`, and + `\al` + space yields `∀` — from `all`, not `alpha`. The second is + the one that bites: a "longest match" or "unique match only" + implementation passes the first and fails this. +45b. **Suffix rule.** `\alp7` + space yields `α7`. Bites against an + implementation that drops unmatchable trailing characters or + abandons the whole abbreviation. +45c. **There is no terminator list.** `\+` followed by space extends + rather than terminating, because `'+ '` is a key. Bites against any + implementation with a hardcoded space/tab/RET terminator set — which + is what rev 5 specified. +45d. **`\\` yields a single `\`**, by extension-and-eager-match rather + than by treating the second `\` as a terminator. And after a + *non-empty* pending key, a second `\` does terminate and open a new + abbreviation: `\alpha\to` + space yields `α→`. +45e. **No re-arm through inserted text (§2.11).** `\setminus` + space + yields a literal `\`, and typing an ordinary letter after it inserts + that letter — the inserted backslash opens no pending abbreviation, + because the expansion is a programmatic replace that arms no record. + Bites against a future consumer that infers pending state from + buffer text instead of provenance. +45f. **Both producers, and the CI-darkness stated.** The dispatch path + is pinned by the criteria above. The optimistic CRDT producer + (round-5 finding 4) is pinned by a separate criterion driving + `handle_remote_crdt_op`, which is `#[cfg(feature = "crdt")]` and + therefore **dark in CI and dark in the required gate list**, since + that list runs `--features crdt` only for `--lib`. The PR must + either land that coverage as a `--lib` test where the gate reaches + it, or state in its description that the optimistic path was + verified only locally and name the command. Silence here is the + failure mode — a green CI would otherwise read as covering the path + most users take. +45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips: + its entry count matches the header's declared count, and a spot set + of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches + `abbreviations.json` byte-for-byte. Bites against a generator that + silently drops or mangles keys (Q#LN11). **Stage 5 — the goal view** @@ -1847,7 +2292,7 @@ renumbering is the cheaper way to not repeat it. it, with the extra success-gate §2.9 forces. - **#110 (auto-pairing)** — `take_typed_edit()` provenance, the fail-closed discipline on transformed source edits, and Q#AP1's optimistic-classifier - limitation. Stage 4 is built on all three. + limitation. Stage 4a generalizes the first; 4b is built on all three. - **#127 (config registry)** — `pmacs.config.define` and the source-buffer-resolution correction. Q#LN10's gate follows `editing.auto-pair` exactly. @@ -1895,8 +2340,8 @@ alongside sixteen other languages — deliberately *not* the typed registry, because moving one language's entry there while the other sixteen stay put would fragment the surface rather than unify it. Migrating `pmacs.lsp.config` wholesale is a config-arc concern; this lane must not -create a precedent that makes it harder. Stage 4's `lean.abbrev` gate is -where this arc does enter the registry, and Q#LN10 already commits to the +create a precedent that makes it harder. Stage 4b's `lean.abbrev` gate is +where this arc does enter the registry, and Q#LN22 already commits to the `editing.auto-pair` shape. **Background-work attribution (§9).** Three pieces of background work, @@ -1928,3 +2373,59 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from #161 — surfacing the spawn failure itself. Each is a behavior change for languages other than Lean, and §4's rule is what keeps them out of a Lean PR. + +### 9.1 Coherence impact — stages 4a and 4b (rev 6) + +**Sections served.** §6 (interaction islands) primarily, and in the +*preventing* direction rather than the fixing one — see below. §11 +(config registry) secondarily, by adding one option in the established +shape rather than a new switch mechanism. + +**Golden journey (§2).** No step is touched by 4a. 4b improves step 4 +(editing) for Lean specifically and changes nothing for any other +language: the pending-abbreviation state exists only in `lean4` buffers. +Neither stage changes launch, open, or attach. + +**Interaction islands (§6).** **None added, and this is the load-bearing +claim of Stage 4b.** An input method is the archetypal island: a modal +state where ordinary keys mean something else, usually with its own +keymap, its own escape, and its own set of commands that only work +inside it. Stage 4b deliberately has none of those. There is no keymap, +no dispatch shadow, no mode line indicator, no command that only works +mid-abbreviation, and no key that exits. The pending state is invisible +to every other subsystem, is abandoned by ordinary editing, and its +worst failure is that the user's literal text stays literal. The +`lean.abbrev` switch is an ordinary registry boolean, not an island +toggle. + +Stage 4a's chain is the mechanism that makes that possible, and it also +retires a smaller island risk: today the only way for a second feature to +react to a typed character is to compete with `pair.lua` for a one-shot +record, and the natural workaround — inferring from buffer text — is how +input methods grow their own private state and, eventually, their own +modal surface. + +**Config registry (§11).** One option, `lean.abbrev`, in exactly the +`editing.auto-pair` shape (boolean, `mutability = "live"`, resolved +against the typed edit's source buffer). This is the arc entering the +registry as §9's earlier text predicted, and it is a genuine adoption +rather than a new surface. Stage 4a adds none. + +**Background-work attribution (§9).** Neither stage does background work. +Both are synchronous inside an existing hook fan-out; no process is +spawned, no timer armed, no request issued. There is nothing to attribute +and nothing to worsen — recorded explicitly because "none" is an answer +this section should be able to give without ambiguity. + +**Debt this revision retires.** The unowned assumption that +`take_typed_edit()` has exactly one consumer forever. That was never a +decision — it was the shape of the only caller — and every future +typed-character feature would have had to rediscover it. Stage 4a turns +an accident into an API with a stated ordering contract. + +**Debt this revision names rather than pays.** One, and it is real: +Q#LN21's cross-peer undo degradation, now covering every abbreviation +rather than three bracket pairs. The fix is chronological cross-peer undo +arbitration, already on the standing backlog and already blocking Q#LN6. +Stage 4b makes the existing gap more visible without widening the class +of defect — but "more visible" is the honest word, not "unchanged." From c4fad0731ceb726965964c0deb29a8893a87135a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:39:01 -0400 Subject: [PATCH 2/7] =?UTF-8?q?docs(lean4):=20rev=207=20=E2=80=94=20round?= =?UTF-8?q?=206=20review,=20five=20P1s,=20and=20reconcile=20the=20ledgers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The 4a/4b split held; five P1s against rev 6's own content, all real, all reproduced. Four share a root: rev 6 verified its external facts and under-verified its internal ones. 1. Stage 4a's declared footprint excluded the tests its own acceptance required. 46a-46e cannot live in tests/auto_pair_acceptance.rs, which criterion 46 requires byte-identical. Footprint now names tests/typed_edit_chain_acceptance.rs and gates on it. 2. Pending abbreviation state had the wrong owner. pmacs is multi-frontend: EditorCore.views is per-FrontendId with its own active window, take_typed_edit is already frontend-keyed, and buffer.after-switch fires with no arguments — so a buffer-keyed clear-on-switch lets any frontend discard another's pending abbreviation. Now keyed (frontend, buffer) with a window check, frontend-scoped clearing, a frontend.detached purge, and acceptance 45i, which the buffer-keyed design passes every other criterion without. 3. The shortest-match rule was missing its tie-break: upstream keeps declaration order among equal-length shortest keys, and 101 prefixes have equal-shortest candidates resolving to different symbols (f picks f< over f>). A pairs-iterated Lua map cannot express this, so the vendored artifact is now an ordered sequence and resolution sorts by (#key, source rank). Rev 6 missed this because it declared the package ships no README after a 404 on the package root, with the directory listing showing src/README.md already in hand — a 404 on a guessed path is not evidence of absence, and the README states the rule in one sentence. 4. The generator's rejection rule rejected the current table: \ is a key and " begins eleven, while acceptance 45d requires \ to work. Replaced with canonical lossless escaping; aborts only on duplicate keys, invalid UTF-8, and a failed self-round-trip. 45g no longer claims to diff against abbreviations.json, which is not shipped. 5. Durable and volatile state were not reconciled. agent-handoff.md anchored main at d152120 with neither #167 nor #170 and no Lean arc bullet at all; active-work.md kept 407 lines of merged Stage 1/2/3a/3b history against its own instruction to prune merged entries, under a stale snapshot date. Durable facts moved to the handoff; the ledger keeps only the unlanded Stage 4 lane. Also corrected: 119 multi-codepoint symbols (26 with $CURSOR), not 93; three backslash values, not two; Q#LN22 now states the terminating-\ reprocess rule acceptance 45d depended on; acceptance 38 says the terminator is retained, so undo restores "\alpha " with its space; coherence cites golden-journey step 5, not step 4; and the config-registry prior art points at Q#LN22. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 435 +++---------------------------------- docs/agent-handoff.md | 71 +++++- docs/lean4-mode-framing.md | 324 +++++++++++++++++++++++---- 3 files changed, 371 insertions(+), 459 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 52d44ba..47c3677 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -1,6 +1,6 @@ # Active work — cross-machine resume ledger -**Snapshot: 2026-07-25.** This file records volatile work that has not +**Snapshot: 2026-07-26.** This file records volatile work that has not landed on `main`. Read it after `docs/agent-handoff.md`. Remove completed entries when their PR merges; do not let this become a second permanent backlog. @@ -59,421 +59,40 @@ If it does not, stop and repair the remote/fetch configuration. ## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING -- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review - round, all twelve checks green). Branch `githubsucks/lean4-stage1` - retained; it was worked in the shared checkout (no sibling worktree). -- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as - the branch's first commit (`a382965`) after three review rounds. **Seven - stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star: - match or exceed VS Code's Lean support. -- **Stage 1 implemented; no wire change (protocol stays v20), no LSP, no - frontend change.** Four commits: framing, grammar, theme captures, - editing surface + acceptance. - - `Cargo.toml` + `src/syntax.rs`: `arborium-lean` 2.18 and one - `BUILTIN_LANGUAGES` entry named **`lean4`** (Q#LN2 — the name becomes - the `didOpen` language_id), claiming `.lean` only. - - `src/highlight.rs`: four capture entries — `constructor`, `character`, - `keyword.conditional`, `warning`. - - `builtin/runtime/{comment,pair,syntax}.lua`: `--` comments, the - `⟨⟩ ⦃⦄ ⟮⟯` pair set, the `lean` → `lean4` modeline alias. - - `tests/lean4_stage1_acceptance.rs` plus unit tests in `syntax.rs` / - `highlight.rs`: 12 criteria, 17 tests. -- **Q#LN1's open obligation is discharged.** `tree-sitter-lean4` is - unusable (depends on `tree-sitter ^0.25` directly against our 0.26, - exports no `LANGUAGE` const despite its README, packages no queries); - `arborium-lean` rides `tree-sitter-language 0.1` with a pre-generated - ABI-15 parser. `cargo tree -d` shows no duplicate core. The parse smoke - pins the failure mode that matters: `→`/`∀`/`≥` must produce - `(arrow)`/`(forall)`/`(comparison)`, since a mismatched-core build - degrades silently on exactly those characters rather than failing loudly. -- **Q#LN4 is a deliberate retro-paint of seven language entries**, not - four: `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated - base-first into javascriptreact/typescript/typescriptreact. Its shape is - "every capitalized identifier" (`#match? "^[A-Z]"`) plus every Lua table - brace — not "constructors". Pinned in both directions per #146. -- Implementation findings not in the framing: - - `warning` had to move from bold red to bold **bright** red: `number` - is plain `fg(1)`, so `sorry` and an adjacent numeric literal were the - same colour. Found by writing the test. - - `Some(1)` is **not** `@constructor` — in call position a narrower - `@function` pattern wins. Only bare or pattern-position capitalized - identifiers reach it. Pinned so the blast-radius claim stays honest. - - Lean node kinds nest: `module > declaration > def|theorem`. - - `pmacs.parse.injection_aliases` is a documented **write-only** Lua - proxy (canonical map is Rust-side), so fence tests must drive - `_parse_now` and inspect layer languages, never read the table back. -- **Review round 1 addressed.** The finding: acc12's server-list assertion - could not fail for the regression it named — the shared `editor()` - helper wipes `pmacs.lsp.config` before any buffer opens, so - `#pmacs.lsp.list() == 0` holds for every language regardless of what - Stage 1 ships. It now asserts against a **pristine** `EditorState` that - `pmacs.lsp.config.lean4` is nil, with a non-vacuity check that the same - lookup finds `rust`; bite-verified by adding a `lean4` config to - `lsp.lua` and watching it fail. Also fixed a stale column in a - `highlight.rs` comment. -- Verification on this branch: `cargo fmt --check` clean; strict workspace - Clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1 - 9/9; comment toggle 14; auto-pair 45; injection 4; M4 121; required GPU - 152; **isolated-config workspace sweep 3,150 across 90 suites**; - `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` - for the reason recorded in the bottom-panel lane below. -### Stage 2 — multi-root LSP server affinity (Q#LN15) +- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), + #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full + histories were pruned from this ledger in round 6, per this file's own + instruction to remove entries when their PR merges; the durable facts + now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 7 + carries the decisions. -- Portable branch: `githubsucks/lsp-multi-root-affinity`, shared checkout, - based on `githubsucks/main` @ `0827dd1`. Named for the substrate, not - for Lean: **the diff contains no Lean content**, because `ensure_server` - is the one server-affinity function every LSP language shares and a - cross-cutting change to it must not be reviewable only as a Lean - feature. -- Three files, no protocol change: `src/lua_bindings/mod.rs` (the - `lsp.list()` row builder gains `root_uri` + `cwd`), - `builtin/runtime/lsp.lua` (`project_root_for` returns `root, source`; - `ensure_server` hoists it above the reuse loop and matches on it), - `tests/lsp_multi_root_acceptance.rs` (9 tests, acceptance 13–21). -- **The rule that keeps this from regressing every other language: the - affinity key is the root only when a root was actually FOUND.** - `project_root_for` never returns nil for a file with a path — its last - resort is the file's own directory — so a naive `(language_id, root)` - key gives every directory of loose scratch files its own server, for - every language. `source` is `"config" | "detected" | "fallback"` and - only the first two become a key. -- **Wire-identical for the fallback case, and that is provable rather - than hoped.** Matching is on the spawned spec's `root_uri` (nil matching - nil), so the fallback spawn passes `root_uri = nil`; `cwd` still carries - the directory and `build_initialize` derives the identical `rootUri` - from `cwd` when the field is None, using a percent-encoder with the same - allowed set as Lua's `file_uri_for`. `build_initialize` (`src/lsp.rs`) - is the **only** reader of `spec.root_uri` in the tree. -- Deliberate behavior change, asserted not discovered: a server - hand-spawned from `init.lua` with only `cwd` set also reads back nil, so - a root-bearing attach will not adopt it. -- `config[language].root` may now be a `function(path) -> string|nil`, - memoized per directory — needed because the hoist puts root resolution - on every attach rather than every spawn. The memo is keyed **weakly by - the resolver function itself**, so replacing `config[lang].root` cannot - serve a root the previous resolver computed. This is Q#LN8's - generalization landing early; the Lean resolver that uses it is Stage 3. -- Bite-verified three ways: 5/9 fail against the pre-change `lsp.lua`, - 8/9 against the pre-change `mod.rs`, and — the one that matters most — - installing the naive always-key-on-root variant fails acceptance 20 and - 21 exactly as Q#LN15 part 2 predicts. The four that survive the first - bite (13, 15, 16, 19) are the regression pins; passing on both sides is - their job. -- Every fixture sets `pmacs.project.set_search_boundary` at its own - tempdir root. Without it the marker walk climbs to the filesystem root - and a stray `.git` above the temp directory turns the markerless cases - into detected ones — the assertions would still pass while testing - nothing. -- **Found but not fixed here (pre-existing, own lane):** `ensure_server` - never forwards `cfg.restart` to `pmacs.lsp.spawn`, so a - `restart = "never"` in `pmacs.lsp.config[lang]` is silently dropped on - the auto-attach path. At least one existing test sets it believing it - takes effect. Out of scope for a PR whose acceptance 16 pins existing - attach behavior as unchanged. -- **Review round 1 addressed.** The blocker was process, not design: the - test file was committed *before* `cargo fmt` ran, so the fix sat - uncommitted in the working tree and the branch as pushed failed the - first gate. The reported "fmt clean" described the worktree, not the - branch — gate results are only meaningful when run against the pushed - tree. Also added the two pins review asked for (a **string** `config - .root` as an affinity key — acc17 only covered the function form; and - `root = false` reading as unset), each bite-verified against exactly - the mutation it targets and neither against the other. And documented - the canonicalization obligation: the `"detected"` arm is canonicalized - for free, a **configured** root is not, so on macOS a resolver - returning `/var/…` and a detected `/private/var/…` are different keys - for one directory. Stage 3's Lean resolver is the first real consumer, - so the obligation is written at the point of use. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; - multi-root 11/11; M4 121; statusline 7; completion popup 9; auto-pair - 45; required GPU 155; **isolated-config workspace sweep 3,164 across 91 - suites**; `git diff --check` clean. The sweep needs an isolated - `XDG_CONFIG_HOME` and `-- --skip basedpyright`. - -### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`) - -- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @ - `46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first - two commits, then the implementation, then a bite-driven correction. -- **Stage 2 merged as #161** (`main` @ `46a1b8f`, 2026-07-25, two review - rounds). COHERENCE.md §7 records the slice; §1.2 records the dead - `pmacs.error` channel found landing it. -- **Framing rev 5 splits Stage 3 into 3a and 3b** because rev 4 broke its - own §4 rule — the row read "two `lsp.lua` generalizations" under prose - claiming Stage 3 was Lean-only. One generalization shipped as Stage 2; - the other (Q#LN9's seams) is the shared event drain, so it is now its - own substrate stage. 3a and 3b are **strictly sequential** — 3b's - subscriber is written against 3a's seam and both touch `lsp.lua`. -- Ships: `pmacs.lsp.on_notification` / `on_response`, two arms in - `handle_server_requests`, a pending-response purge, and - `pmacs.fs.canonicalize` (Q#LN20). No protocol change, no Lean content. -- **Two framing claims were corrected during implementation**, both - recorded in §0.1 finding 6 and in the round-2 commit: - 1. The reachable leak is **not** a killed buffer. The Rust core fires - exactly five hooks (`buffer.after-edit`, `buffer.after-load`, - `buffer.after-switch`, `frontend.detached`, `process.after-tick`) — - **there is no buffer-kill hook**, so nothing tears an attachment - down and the drain keeps reaching that server. The real path is - `attach_buffer` dropping a dead sid from `attachments` and - rebuilding against a fresh server, which makes `crashed`/`stopped` - the event *least* likely to be drained. Hence the purge polls - `pmacs.lsp.list()` rather than riding the drain. - 2. Acceptance 32 does **not** pin "removed before invocation" — - `pcall` catches the raise either way, so before/after is - unobservable without a re-entrant drain. It pins removal being - **unconditional**; renamed accordingly. -- **`pmacs._fs` is installed from `install_async`, not `install_project`**, - purely for load order: `make_workspace` runs *after* `fs.lua` is - evaluated, so a canonicalizer placed there reads nil. This cost one - failing run to discover and is the kind of thing to check first. -- Bites recorded (all against the committed tree): removal gated on a - clean return → acc32 fails 2 != 1; an event-driven purge → the - no-attachment case fails "never called" while the attached case still - passes; a resolver without `canonicalize` → two servers (34b's own - falsification, which ships as a test). -- **Known unpinned:** the purge's generation (`attempt`) check. Reaching - it needs a crash *and* its restart to fall in a gap with no - `_async.tick`; the backoff is 500ms, so any tick sees `crashed` first - and the absent-or-terminal arm fires. Labelled as defensive in the - code rather than left looking covered. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,826 default + 2,003 CRDT library tests; - dispatch seams 15/15 on Linux (14 on macOS — see below); multi-root - 13/13; M4 121; required GPU 155; **isolated-config workspace sweep - 3,189 across 93 suites, zero failures**; `git diff --check` clean. -- **Two flakes/portability facts from CI round 1, both worth keeping:** - 1. `composition_overhead_under_ten_percent` tripped once in a local - sweep at 18.8% against a 10% budget, then passed 3/3 in isolation - here, passed in isolation on main, and passed a full sweep rerun. - The tell is in its own output: the same run reported realistic-frame - overhead as **-4.6%**, and a negative figure is measurement noise, - not added work. Load-sensitive under a parallel `--workspace` run. - 2. **A non-UTF-8 filename fixture cannot be built on macOS.** APFS - enforces valid UTF-8, so `std::fs::write` fails with EILSEQ - ("Illegal byte sequence") before the code under test is reached. - `#[cfg(unix)]` is NOT sufficient for such a fixture — - `#[cfg(target_os = "linux")]` is. Cost one red CI round to learn. - -### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`) - -- Same worktree `../pmacs-lean-stage3`, **branched off - `lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response - seam and `pmacs.fs.canonicalize`, so it is strictly sequential. - **Retarget PR #170 to `main` BEFORE merging #167, not after** — the - kill-ring lesson exactly. (Round 1 of this ledger entry stated the - reverse in its first sentence and the correct rule in the next; the - review caught it. A safety rule written twice with opposite senses is - worse than not written.) -- Ships `builtin/runtime/lean.lua` (new), one `include_str!` line in - `src/editor.rs`, `pmacs.lsp._attach_buffer` exported from `lsp.lua`, - a `leanprogress` mode plus `waitForDiagnostics` validation on - `pmacs_fake_lsp`, and `tests/lean4_server_acceptance.rs` (40 tests). - No protocol change. -- **Stage 1's acceptance 12 is half superseded and was rewritten, not - deleted.** It asserted `pmacs.lsp.config.lean4 == nil` to catch a - Stage-3 front-run; 3b is that stage. What survives is the restraint - half — constructing an editor spawns nothing though the config now - names `lake`, and opening a Lean buffer with no server configured - spawns nothing — which is what holds Q#LN7's "not at init" promise. -- **The marker test is wrong in two opposite directions if done naively** - and both are pinned: `io.open` SUCCEEDS on a directory (so truthiness - accepts a `lean-toolchain` dir), but requiring a non-nil read rejects - an EMPTY `lean-toolchain` (a legitimate marker — existence semantics, - not content). Discriminator is `read`'s SECOND return; decline only on - a non-nil err. Probed on LuaJIT 2.1. -- **Fifteen bites recorded, each against the committed tree.** R1: bare - `io.open` → 24a fails / 24b passes; require-non-nil → 24b fails / 24a - passes; no canonicalization → symlinked open spawns two servers; no - re-attach after the swap → three latch tests fail; hook keyed on the - attachment → the missing-`lake` case fails; `waitForDiagnostics` - without `version` → acc37 fails with InvalidParams. R2: skip retiring - a terminal server → `attempt` reaches 3; no originating-buffer gate → - the Lean buffer is left on the `lake` stub; retry-forever → the - failing-fallback test fails; version-probe any command → the - working-wrapper test fails; no disabled guard → the unconfigured test - sees "`nil` could not be started". R3: verdict keyed on `watching` → - the late-verdict test finds the buffer still on `lake`; `buf_key` - rewritten per load → the second-buffer test fails; hardcoded - `lake serve` → the wrapper-naming test fails. -- **Round-2 review: three more P1 lifecycle defects, suite 20/20 with - all of them live.** (1) The crashed primary respawned forever — - skipping the retire call avoided corrupting terminal servers but left - `next_restart_at` armed. **`forget` is the call for a TERMINAL server** - (it requires terminal state and removes the client, dropping the - restart timer); `stop` is for a live one and corrupts a terminal one. - (2) Re-attachment targeted whatever buffer was active when the async - verdict landed; an unrelated Rust attachment satisfied "a different - server id". (3) A failing fallback retried every tick forever, silent. - Plus two P2s: the Lake version parser was applied to arbitrary wrapper - output, and an UNCONFIGURED `config.lean4` was reported as failure and - latched, poisoning the session. -- **Round-3 review: two more P1s, both asynchronous correlation, suite - 25/25.** (a) `probe.watching` is cleared when the server initializes, - so a SLOW version verdict arrived with nil and retired nothing — - `_attach_buffer` returned the still-live primary and the retry called - it success, so status and config said "fell back" while the buffer - stayed put. **That is the round-1 silent no-op reached through a third - event ordering.** `probe.primary` is now separate from - `probe.watching` and survives initialization. (b) `buf_key` was - rewritten on every Lean `after-load`, so a second Lean buffer opened - before the verdict became the rebuild target while the latch still - watched the first buffer's server. Target buffer and primary server - are one fact and are now armed together, once. Plus a P2: the failure - message hardcoded `lake serve` after the latch became - command-agnostic, sending wrapper users to debug the wrong binary. -- **Round-4 review: one P1, and it is the same defect a FOURTH time.** - `pmacs.lsp.config.lean4` is a single global entry, so swapping its - command invalidates **every** Lean buffer and **every** Lean server — - Q#LN15 gives one per project root. Rounds 1–3 each fixed the repair - for one buffer and one server; round 4 is "repair the armed target, - strand the rest". The shape that finally holds: retire ALL `lean4` - servers on latch, and repair each buffer **lazily and at most once** - when it becomes active (`buffer.after-switch` + the tick), because - `_attach_buffer` is active-buffer-only and cannot reach the others. - The per-buffer once-only bound is what stops a failing fallback - retrying forever — the round-2 defect a naive global repair loop would - have reintroduced for every buffer instead of one. Plus a P2: the - argument-inclusive attribution was implemented but pinned only by - "contains the command name", so a mutation dropping every argument - still passed. -- **Round-5 review: one P1 plus a frontend scope hole, and four more.** - (1) A fallback that SPAWNS and then dies retried forever: the - once-per-buffer guard bounds `_attach_buffer`, not the server it - produced, and `ensure_server` never forwards `cfg.restart` so the - fallback inherits `OnCrash` — respawned by the manager with no - ceiling, silently, because `latched` had disabled the primary's poll. - The fallback now gets its own one-shot die-before-initialize watch. - (2) **Simultaneous frontends**: both repair triggers read the ambient - `pmacs.window.buffer()`, and the daemon restores `active_frontend` to - the last-dispatched one before `tick_processes`, so a Lean buffer - active in ANOTHER frontend gets no `after-switch` and stays stale. - Fixed at the right seam — **make CONSUMPTION safe**: both - `attached_for_active` and `attachment_for_request` now refuse a record - whose server is dead (the former rebuilds, the latter reports none, - since it must not perturb LSP state). Healing at the point of use is - frontend-agnostic, because whichever frontend runs a command is active - while it runs. (3) The retirement sweep selected on `language_id`, so - it stopped USER-spawned Lean servers too; it now keys on the - `default-lean4` label `ensure_server` stamps, which is the derivation - discriminator. (4) `probe.latched` gated repair even when NO swap - occurred, so an already-fallback config was retried and misreported. - Split out `probe.fallback_installed`. (5) The once-per-buffer - assertion counted TABLE KEYS, which cannot distinguish "once per - buffer" from "every tick for one buffer" — cardinality stays 1 either - way. Now a numeric attempt counter; the bite shows **174 vs 1**. -- **Round-6 review: four P1s and one P2, suite 40/40.** (1) General - point-of-use healing treated a crashed OnCrash server as absent and - spawned beside it while its old id still had `next_restart_at` armed; - `attach_buffer` now forgets a terminal record before replacement. - `attachment_for_request` remains non-attaching and preserves the - record, so a same-id restart can recover instead of being orphaned. - (2) The fallback watch was scalar, while Q#LN15 permits simultaneous - per-root servers and lsp.lua can create them without passing through - Lean's repair function. Watches are now per-SID and discover every - config-driven Lean server from a private origin table. (3) The shipped - `lean.wait-for-diagnostics` command bypassed both safe resolvers and - still consumed a stopped record; it now uses a command-safe resolver, - waits asynchronously for a healed replacement to initialize, and the - test requires the real request to finish. (4) When no config swap - occurred, one failed root still swept a healthy root; that arm now - retires only the SID whose verdict fired. (5) `label` is public and - unreserved, therefore not ownership. lsp.lua records successful - config-driven spawns privately, and every Lean lifecycle decision keys - on that origin fact; the user-server pin deliberately collides on - `default-lean4`. All five bites against `19f48d4` discriminate: the - old files produce 2 same-root servers, a fallback attempt of 4, a - shipped command still targeting `stopped`, retirement of the healthy - root, and retirement of the colliding user server, respectively. -- **DURABLE LESSON — "the test that passes" vs "the test that - discriminates."** Green tests across six rounds repeatedly pinned only - a nearby helper or an absence, and only biting exposed it. **Carry this - to `docs/agent-handoff.md` when the lane lands.** The concrete shapes, - all from this branch: - 1. R1 acceptance 36 asserted "every server is terminal" — pinning the - ABSENCE of the fallback it claimed to test. - 2. "No live non-fallback server" misses a respawn loop: a respawning - server sits in `crashed` most of the time. `attempt` counts - respawns; liveness does not. - 3. Returning to a buffer via `find_or_open` re-fires - `buffer.after-load`, which repairs the attachment regardless of the - code under test. Use `switch_buffer`. - 4. A MISSING executable fails synchronously inside `after-load`, where - the rebuild happens inline — no async race can occur. Only the - probe path exercises asynchronous ordering. - 5. A mutation that RAISES (indexing a nil config) is swallowed by the - hook's pcall, so the bite "passes" for the wrong reason. A bite must - reproduce the original shape, not merely break the code. - 6. A fixture whose `serve` sleeps can never let the primary initialize - first, so it cannot reach the ordering where a late verdict must - retire a LIVE server. - 7. Asserting on a field that no longer exists (`_probe.reattach_from` - after a refactor) reads as nil and passes for nothing. Assert - positive facts — a count, a command string — not absences. - 8. Counting DISTINCT KEYS cannot bound REPEATED WORK: a per-tick retry - on one buffer keeps `#repaired == 1` forever. Count the attempts, - not the things attempted against (bite: 174 vs 1). - 9. A NONEXISTENT executable only exercises synchronous ENOENT. To - reach "spawned, then died", the fixture must actually spawn. - 10. Calling the two SAFE HELPERS directly does not pin a shipped - command that bypasses both. Drive the command registry entry and - require its terminal result — replacing a dead record with a - `starting` server is still not success if the request is issued - before initialize. - Rule: **a test is not evidence until the mutation it targets has been - shown to fail it.** -- **SECOND DURABLE LESSON — a scope error repeats until the scope is - named.** The "fallback silently does not happen" defect came back four - times: no re-attach; re-attach cleared by an unrelated buffer; - re-attach satisfied by the server being replaced; re-attach of one - buffer while the others stay stale. Every fix was locally correct and - none asked *what does this config swap invalidate?* — the answer being - every Lean buffer and every Lean server, because the config entry is - global and servers are per-root. **When a change edits shared state, - enumerate everything derived from it before repairing anything.** -- **SUBSTRATE BUG FOUND, not fixed here (framing §6).** - `LspManager::stop` on an ALREADY-terminal server takes its - not-initialized branch, terminates the dead process and sets - `ShuttingDown { .. None }` on the premise that "the next exit - observation cleans up" — but the exit already happened, which is what - made it `Crashed`. No further event arrives, so the client is stuck in - `ShuttingDown` **forever**: `server_is_live` reads it as LIVE, so - `attach_buffer` never rebuilds, and `forget` refuses it for not being - terminal. **Stopping a dead server is what makes it un-replaceable.** - Lean works around it by dispatching on state: `forget` when - terminal, `stop` when live. Merely SKIPPING the call is not - enough — that leaves `next_restart_at` armed. -- Round-1 review found four P1s, all real: the latch swapped the config - but never spawned or re-attached (and acc36 *asserted every server was - terminal*, pinning the absence of the fallback); a missing `lake` - bypassed probe and latch entirely because the hook keyed on an - attachment that ENOENT prevents; `waitForDiagnostics` omitted the - `version` Lean requires; and the ledger stated the dangerous stacking - order. -- The probe's non-zero exit is deliberately NOT a fallback trigger — - §2.9's elan shim makes `lake --version` fail where `lake serve` still - works. Only a parseable version below 3.1.0 triggers it; the - server-failure latch covers the rest. -- Verification on this branch: `cargo fmt --check` clean; strict - workspace Clippy clean; 1,829 default + 2,003 CRDT library tests; - lean4 server 40/40; lean4 stage 1 9/9; dispatch seams 15/15; - multi-root 13/13; M4 121; required GPU 155; **isolated-config - serial workspace sweep 3,229 across 94 suites, zero failures**; - `git diff --check` clean. (Round 1 of - this entry recorded 17/17 and 3,206 — the PRE-fix counts — after the - fixes were pushed. The ledger's protocol is that verification - describes the pushed tree; recording it late is the #161 fmt-blocker - error in a slower form.) - -### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4 — framing rev 7, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) - Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main that had advanced 50 commits mid-review; the only conflict either time was this ledger's own lane headings, resolved by keeping both sides. - Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. - Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No + Framing-only so far: `docs/lean4-mode-framing.md` **revision 7**. No code. Awaiting user approval before implementation, per the workflow. +- **Round 6 review found five P1s, four of them internal to rev 6** — + facts about pmacs the revision asserted without checking, while its + external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint + omitted the test file its own acceptance requires; pending + abbreviation state was keyed by buffer when pmacs is **multi-frontend** + (`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already + frontend-keyed, and `buffer.after-switch` fires with NO arguments, so + a buffer-keyed clear lets any frontend discard another's pending + state); the shortest-match rule was missing its **tie-break by source + declaration order**, which 101 prefixes depend on and a `pairs`- + iterated Lua map cannot express; and the generator's "abort on keys + needing escaping" rule **rejects the real table** (`\` is a key, `"` + begins eleven). +- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared + the upstream package ships no README after fetching the package root, + with the directory listing showing `src/README.md` already in hand. + The README states the tie rule in one sentence. - **Round 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 diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index b2d0aeb..a176505 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,7 +1,8 @@ # Agent handoff — cross-machine continuity -**Last updated: 2026-07-25, after the inline-math slice (#158) landed — -the first mathematical typesetting in pmacs — following find-file (#162), +**Last updated: 2026-07-26, after Lean 4 stages 3a and 3b (#167, #170) +landed — pmacs' first Lean language server — following the inline-math +slice (#158), the first mathematical typesetting in pmacs, and find-file (#162), the dired arc's Stage 0, and COHERENCE.md (#163), Lean 4 Stage 1 (#160), the minimap blank-slab fix (#159), bottom-panel Stage 1 (#155), the inline-math re-scout (#154), the vterm PTY-flake fix (#153), and the @@ -25,15 +26,15 @@ reads it the way you just did. For volatile branches, checkpoints, verification, and recovery commands, read `docs/active-work.md` immediately after this file. -## 1. Where the project stands (2026-07-25) +## 1. Where the project stands (2026-07-26) -- `main` @ `d152120` (the bottom-panel landed-doc refresh #156 atop the - inline-math slice #158, dired Stage 1 #165, the GPU terminal input fix - #166, Lean 4 Stage 2 #161, the dired framing #164, COHERENCE.md #163, - find-file #162, Lean 4 Stage 1 #160, minimap blank-slab #159, - bottom-panel Stage 1 #155). Protocol unchanged at **v20**. The bullets - below describe the arcs in their own terms; this line is the - head-of-`main` anchor. +- `main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a #167, the + bottom-panel landed-doc refresh #156, the inline-math slice #158, + dired Stage 1 #165, the GPU terminal input fix #166, Lean 4 Stage 2 + #161, the dired framing #164, COHERENCE.md #163, find-file #162, Lean + 4 Stage 1 #160, minimap blank-slab #159, bottom-panel Stage 1 #155). + Protocol unchanged at **v20**. The bullets below describe the arcs in + their own terms; this line is the head-of-`main` anchor. - **`COHERENCE.md` is now required reading and a required framing input — #163.** It carries the product-coherence thesis, an audited scorecard, per-concern gaps, and §20's priority order, and it is the @@ -42,6 +43,56 @@ commands, read `docs/active-work.md` immediately after this file. interaction islands added, config-registry adoption, background-work attribution. Its §2 grades the golden journey **broken at step 3** (`pmacs .` exits 1). +- **Lean 4 arc (Arc 8) — stages 1, 2, 3a, 3b LANDED** + (`docs/lean4-mode-framing.md`; #160, #161, #167, #170; merge + `d400f30`). pmacs edits Lean 4: `arborium-lean` highlighting, a + `lean4` major mode, `⟨⟩ ⦃⦄ ⟮⟯` pairs, and a `lake serve` language + server with a Lake-aware outermost root, a lazy toolchain probe, a + one-shot `lean --server` fallback, and `waitForDiagnostics`. **No + protocol change in any stage** (still v20). + - **Two of the four stages contained no Lean at all**, and that is the + arc's organizing rule: *no PR mixes a cross-cutting substrate change + with Lean feature content.* Stage 2 made LSP server affinity + per-project-root (`ensure_server` had been reusing one server across + roots — a correctness bug for every language, not just Lean). Stage + 3a added notification/response subscription seams to + `handle_server_requests`, the single shared LSP event drain, plus + `pmacs.fs.canonicalize`. + - **Two consecutive re-scouts found that rule broken by the stage + being scouted** — Stage 3 in round 4, Stage 4 in round 5, each time + by a risk column that contradicted its own prose. The rule is not + self-enforcing. Re-check every remaining stage's risk column at + scout time. + - **A configured LSP root must be a canonical absolute path.** It + reaches `file_uri_for` verbatim and that URI is the affinity key, so + one package opened by two spellings spawns two servers. Stage 3a's + `pmacs.fs.canonicalize` is the primitive; it returns nil rather than + a lossy path for non-UTF-8 input. + - **`LspManager::stop` on an already-terminal client strands it in + `ShuttingDown` forever** — `server_is_live` then counts it live so + nothing rebuilds against it, and `forget` refuses it for not being + terminal. *Stopping a dead server is what makes it un-replaceable.* + Stage 3b works around it by dispatching on state (`forget` when + terminal, `stop` when live); merely skipping the call leaves + `next_restart_at` armed. The real fix is unframed substrate work. + - **`elan` shims lie**: `lake --version` and `lean --version` can both + fail ("no default toolchain configured") on a machine where Lean + otherwise works, so `command -v lake` is worthless as a capability + check. Lean acceptance is fake-server; live smokes must be PATH- + **and** success-gated. + - Stage 3b took six review rounds, and **the same defect appeared four + times**: "the fallback silently doesn't happen," as no re-attach, + then re-attach cleared by an unrelated buffer, then satisfied by the + very server being replaced, then repairing one buffer while the rest + stayed stale. Each fix was locally right; none asked what a *global* + config swap invalidates. The durable lesson is to heal at + **consumption** — the point where a stale record is handed out — not + at the moment of the swap. + - Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode + input method) are framed and awaiting approval; stages 5 (goal + panel), 6 (`#eval` output channel), and 7 (module hierarchy) are + framed but not scouted against current `main`. + - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU frontend. **No protocol change (still v20); the whole slice lives in diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index e39eb36..ca50696 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. +Revision 1 — initial. Current revision: **7**. ### Round 1 (rev 1 → rev 2) @@ -288,11 +288,15 @@ landed and its citations are historical record, not navigation. Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main` @ `d400f30` produced **six findings that change the plan** and three -that confirm it. The pmacs-side facts were verified in a worktree at +that confirm it. (Round 6 found five more, four of them internal to this +revision; read that section too before trusting a rev-6 statement.) The pmacs-side facts were verified in a worktree at that commit; the upstream facts were verified by downloading and reading `leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the algorithm, not its documentation, since the `lean4-unicode-input` -package ships no README. +package ships no README. *(Round 6: it does, at `src/README.md` — see +that section. Corrections to round 5's own numbers are marked inline +below rather than rewritten, per the standing rule that revision +entries are record, not navigation.)* 1. **Stage 4 violated this document's own splitting rule — the same way Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting @@ -377,6 +381,14 @@ package ships no README. needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs does not. + *Corrected in round 6.* **119** symbols are multi-codepoint, of which + 26 carry `$CURSOR`; "93" was the non-`$CURSOR` subset stated as a + total. **Three** values contain a backslash — the `\` → `\` identity + entry was missed. And this entry's biggest omission is not a number: + the shortest-key rule needs a **tie-break by source declaration + order**, which the README round 5 said did not exist states outright. + §2.11 and Q#LN11 carry the corrected facts. + Confirmations, recorded because each was load-bearing and unverified: 7. **`take_typed_edit`'s one-shot contract is unchanged** @@ -404,6 +416,70 @@ Citation drift repaired per COHERENCE §25, on the same terms as round and the revision-history entries above, which are historical record rather than navigation. +### Round 6 (rev 6 → rev 7) + +The 4a/4b split held; five P1s against the revision's own content, all +real, all reproduced. Four share a root: **rev 6 verified its external +facts and under-verified its internal ones.** + +1. **Stage 4a's declared footprint excluded the tests its acceptance + required.** Q#LN10 listed three production files while 46a–46e demand + chain-specific tests that cannot live in + `tests/auto_pair_acceptance.rs` — criterion 46 requires that file + byte-identical. Footprint now names + `tests/typed_edit_chain_acceptance.rs` and adds it to the PR's gates. +2. **Pending state had the wrong owner.** §2.11 reasoned "no + multi-cursor, therefore one point" and Q#LN22 keyed pending + abbreviations by buffer. pmacs is multi-frontend: `EditorCore.views` + is per-`FrontendId` with its own active window, `take_typed_edit` is + *already* frontend-keyed, and `pmacs.frontend.id()` exists. Two + frontends on one Lean buffer — the TUI-plus-GPU case this project + ships — would share one slot. Worse, `buffer.after-switch` takes no + arguments, so a buffer-keyed clear-on-switch lets any frontend + discard another's pending abbreviation. Now keyed + `(frontend, buffer)` with a window check, frontend-scoped + after-switch clearing, a `frontend.detached` purge, and acceptance + 45i — which the buffer-keyed design passes every other criterion + without. +3. **The shortest-match rule was missing its tie-break, and rev 6's + research method is why.** Upstream keeps declaration order among + equal-length shortest keys. The README states it in one sentence — + and rev 6 asserted "the package ships no README" after a 404 on the + package root, without checking the directory listing it had already + fetched, which shows `README.md` under `src/`. **A 404 on a guessed + path is not evidence of absence.** The rule is load-bearing: 101 + prefixes have equal-shortest candidates resolving to *different* + symbols (`f` → `f<` not `f>`; `"` picks `"A` from eleven). A `pairs`- + iterated Lua map cannot express it, so Q#LN11 now emits an ordered + sequence and Q#LN22 sorts by `(#key, source rank)`. +4. **The generator's rejection rule rejected the current table.** "Abort + on keys needing Lua escaping" would reject `\` and the eleven `"X` + keys — and acceptance 45d requires `\` to work. Replaced with + canonical lossless escaping; the generator aborts only on duplicate + keys, invalid UTF-8, and a failed self-round-trip. Relatedly, 45g + claimed the suite compares against `abbreviations.json`, which is not + shipped; it now pins self-consistency properties and leaves + source fidelity to the generator, where the source is in hand. +5. **Durable and volatile state were not reconciled** — + `docs/agent-handoff.md` still anchored `main` at `d152120` with + neither #167 nor #170, while `docs/active-work.md` kept full merged + Stage 3a/3b histories against its own instruction to remove merged + entries, under a stale July 25 snapshot date. Round 5 updated the + ledger and skipped the handoff; per CLAUDE.md both are required + reading, and the one that outranks the other was the one left wrong. + +Corrections carried in the same revision, each verified against the +data: the README exists (finding 3); there are **119** multi-codepoint +symbols, of which 26 carry `$CURSOR` — rev 6's "93" was the +non-`$CURSOR` subset reported as a total; **three** values contain a +backslash (`\`, `n`, `setminus`), not two; Q#LN22 now states the rule +acceptance 45d depended on, that an unclaimed terminating `\` is +reprocessed as a new leader; acceptance 38 now says the terminator is +retained, so undo restores `\alpha ` with its space; the coherence +section cites golden-journey **step 5** ("Edit immediately"), not step +4; and §8's config-registry prior art points at Q#LN22, where the gate +now lives. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -828,8 +904,15 @@ them from the store needs a Rust-side policy, not a Lua filter. Q#LN18. Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`, package `lean4-unicode-input`, files `AbbreviationProvider.ts`, `TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`, -`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no -README, so the algorithm below is read off the source. Apache-2.0. +`AbbreviationConfig.ts`, `abbreviations.json`, and — round 6 — the +package README at `lean4-unicode-input/src/README.md`. Apache-2.0. + +**Rev 6 first claimed this package ships no README. It does**, at +`src/README.md` rather than the package root, and the 404 on the root +path was taken as absence without checking the directory listing that +was already in hand. That cost the tie rule below: the README states it +in one sentence, and reading only the code left it as an inference from +`Array.prototype.sort`'s stability rather than a documented contract. **Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key having `p` as a prefix, sorts them by **key length ascending**, and maps @@ -845,6 +928,32 @@ Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`), surprising enough to be worth an acceptance criterion), `alp7` → `α7` via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches). +**The tie rule, and why it is a constraint on the vendored format.** +When several shortest keys have equal length, upstream takes **the one +declared first in `abbreviations.json`**. The README says so outright; +the code achieves it because `Object.keys()` yields JSON insertion order +and `Array.prototype.sort` is stable. Ties are not rare: **101 prefixes +have equal-shortest candidates that resolve to *different* symbols**. +`f` picks `f<` → `‹` over `f>` → `›`; `"` picks `"A` → `Ä` from eleven +equal-length candidates; `(` picks `()` over `(=`, `(b`, `((`, `([`. + +A Lua table iterated with `pairs` has no order at all, so **a generated +`{ [key] = symbol }` map cannot express this contract** — it would +resolve these 101 prefixes nondeterministically, and worse, *stably +wrong* per build. Q#LN11 therefore carries source rank alongside the +symbol. + +**Two things the README explains that the code does not.** `Tab` is the +manual early-replacement trigger upstream binds, which is why +`getReplacementText`'s shortest-prefix rule is user-visible at all +rather than an internal detail. And the `[]_`/`{}_` entries in the table +are not symbols anyone types — they are **decoys**, added so that `\[` +is not uniquely-and-completely matching and therefore does not eagerly +expand before the user can type the second `[`. That is the same +collision Q#LN22 handles from the pairing side, solved upstream by +editing the data. Anyone regenerating the table must not "clean up" +those entries. + **Tracking.** The leader `\` is inserted into the buffer like any other character, and the tracked range starts after it; the replaced range spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the @@ -881,8 +990,10 @@ abbreviation the cursor has left. pmacs has no cursor-motion hook (round-5 finding 3), so this seam does not exist here and Q#LN22 makes abandonment lazy instead. -**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` → -`\n`, so an expansion can insert a backslash; upstream sets +**The re-arm guard pmacs does not need.** Three values contain a +backslash — `\` → `\`, `n` → `\n`, and `setminus` → `\` (rev 6 first +said two, dropping the `\` → `\` identity entry) — so an expansion can +insert a backslash; upstream sets `doNotTrackNewAbbr` across the replace so that backslash does not open a new abbreviation. In pmacs the expansion is a programmatic `buf:replace` that arms no typed-edit record, so the chain sees nothing and cannot @@ -891,9 +1002,25 @@ contract, not by accident — and the acceptance must pin it, because a future consumer that inferred from buffer text rather than provenance would reintroduce the bug. -**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a -`Set` and sorts changes bottom-up for that reason; -pmacs has one point, so one pending abbreviation per buffer. +**What pmacs does not have to carry.** Multi-cursor within a frontend. +Upstream tracks a `Set` and sorts changes bottom-up +for that reason; pmacs has one point per frontend view. + +**What pmacs has instead, and rev 6 got wrong.** Rev 6 read "no +multi-cursor" as "one point" and keyed pending state by buffer alone. +**pmacs is multi-frontend**: `EditorCore.views` is a +`HashMap`, each with its own active window and +cursor; `take_typed_edit` is already keyed by frontend +(`typed_edit_armed: Option<(FrontendId, TypedEditRecord)>`, matched +against `active_frontend`); the record carries `window` as well as +`buffer`; and `pmacs.frontend.id()` is exposed to Lua. Two frontends +editing the same Lean buffer — the ordinary TUI-plus-GPU case, not an +exotic one — would share a single buffer-keyed pending slot, so one +could extend, expand, or silently clear the other's half-typed +abbreviation. `buffer.after-switch` makes it worse: it fires with no +arguments, so a buffer-keyed clear-on-switch would let *any* frontend's +navigation discard a pending abbreviation belonging to another. Q#LN22 +keys the state accordingly. ## 3. Decisions @@ -1340,11 +1467,27 @@ claim a reader must be able to check without reconstructing `src/editor.rs`'s include list. **Stage 4a ships this and nothing else.** Its whole content is: -`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer, -and the `include_str!` line. Round 5's finding 1 is why this is a PR and -not a first commit — `pair.lua` is every language's auto-pairing, and a -reviewer looking at a Lean PR should not have to also review a rewrite -of it. + +| File | Change | +|---|---| +| `builtin/runtime/typed_edit.lua` | new — the chain owner | +| `builtin/runtime/pair.lua` | re-expressed as one registered consumer | +| `src/editor.rs` | one `include_str!` line, before `pair.lua`'s | +| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e | +| `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** | + +Rev 6 listed only the first three and then required criteria 46a–46e, +which no existing suite can host: the auto-pairing suite must stay +untouched (that is the whole point of criterion 46), so the chain's own +behavior — take-once, priority order, claim-stops-chain, throw +containment — has nowhere to live. A declared footprint that excludes +the tests its own acceptance demands is not a footprint. The new suite +joins the required gate list for this PR alongside +`tests/auto_pair_acceptance.rs`. + +Round 5's finding 1 is why this is a PR and not a first commit — +`pair.lua` is every language's auto-pairing, and a reviewer looking at a +Lean PR should not have to also review a rewrite of it. **The no-behavior-change claim must be pinned, not asserted.** The full `tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must @@ -1377,10 +1520,24 @@ file rather than estimated: | 305 keys that are proper prefixes of another | which keys can expand eagerly | | 1,550 keys uniquely-and-completely matching | the eager-expansion set | | 26 values containing `$CURSOR` | point placement | -| 93 multi-codepoint values | the replace is not one-char-for-many | +| 119 multi-codepoint symbols (26 of them `$CURSOR`-bearing) | the replace is not one-char-for-many | +| 101 prefixes with disagreeing equal-shortest ties | why the format carries source rank | + +(Rev 6 gave the multi-codepoint figure as 93, which was the count +*excluding* the `$CURSOR` entries — a subset reported as a total.) vscode-lean4 is Apache-2.0. +**Format: an ordered array, not a map.** §2.11's tie rule makes source +order semantic, and a Lua `{ [key] = symbol }` table iterated with +`pairs` cannot carry it. The generated file emits a **sequence** — +`{ {key, symbol}, ... }` in `abbreviations.json` order — plus a derived +`key → index` lookup built at load time for the exact-match case. +Resolution sorts candidates by `(#key, index)`, so the 101 ties resolve +the way upstream resolves them and the file's own line order is the +audit trail. A map-shaped emit would be nondeterministic across builds +and, once a hash order happened to be stable, *stably wrong*. + Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header recording source repo, commit, license, entry count, and the regeneration command — the `builtin/queries/latex/highlights.scm` @@ -1405,12 +1562,29 @@ so the file is self-describing to whoever next touches it. A refresh is an ordinary PR with a visible diff — which is the point: the diff is the review. -**The generator must reject a table it cannot faithfully encode.** Keys -are ASCII today but nothing upstream promises that; a key containing a -character the emitted Lua would have to escape, or a duplicate after -normalization, aborts the regeneration rather than silently emitting a -table that disagrees with its source. Same discipline as Q#LN20's -refusal to hand back a lossy path. +**Escaping is canonical and lossless, not a rejection trigger.** Rev 6 +said the generator aborts on "a key containing a character the emitted +Lua would have to escape." **That rule rejects the current table**: `\` +is a key, `"` begins eleven keys (`"A` → `Ä` …), and acceptance 45d +requires `\` to work. The generator instead emits every key and symbol +through one canonical Lua string escaper — `\\`, `\"`, `\n`, `\r`, +`\t`, and `\ddd` for any other control byte, everything else literal +UTF-8 — chosen so the emit is byte-deterministic across runs. + +What the generator *does* abort on, because these are real corruption +rather than syntax: + +- a duplicate key after decoding (JSON permits it; the table must not), +- a key or symbol that is not well-formed UTF-8, +- a round-trip mismatch: the generator re-parses its own output and + compares the full ordered sequence against the source, entry for + entry, and fails if they differ anywhere. + +That last check is what makes the artifact trustworthy, and it belongs +in the generator rather than in the acceptance suite — the suite cannot +see `abbreviations.json`, which is not shipped. Same discipline as +Q#LN20's refusal to hand back a lossy path: refuse rather than emit +something plausible. ### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it @@ -1466,23 +1640,54 @@ that an edit was made. reconstruction of it: - `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, - start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`. + window, start_offset, text = "" }`, keyed on **`(frontend, buffer)`** — + see below. - 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`. -- Expansion resolves through §2.11's three-rule `getReplacementText`, - including the suffix rule (`\alp7` → `α7`). +- **A terminating `c` that is itself `\` is then reprocessed as a new + leader**, opening a fresh pending abbreviation at its position. This + is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6 + specified the acceptance without specifying the rule; upstream gets it + from `processChange`, where a `finished` abbreviation reports + `isAffected = false` and so does not suppress the new-leader branch. + Note this is *not* the `\\` case: there the pending text is empty, `\` + extends rather than terminates, and the result is one literal + backslash with no pending state left open. +- Expansion resolves through §2.11's rules — shortest key wins, ties + broken by source rank, unmatchable tail appended (`\alp7` → `α7`). - `$CURSOR` is stripped from the symbol and its index becomes the point. +**Ownership is per frontend, not per buffer** (§2.11). The key is +`(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still +match `rec.window` for the state to be usable — a frontend that moved +the same buffer into a different window is no longer typing where the +pending span is. Two consequences the buffer-only design got wrong: + +- `buffer.after-switch` fires with **no arguments**, so it cannot say + whose switch it was. The subscriber reads `pmacs.frontend.id()` at + callback time — documented as "the frontend that produced the most + recent dispatched input event" — and clears **only that frontend's** + entries. A blanket clear would let one frontend's navigation discard + another's half-typed abbreviation. +- `frontend.detached` fires with the raw frontend id and is the purge + seam, exactly as `killring.lua` uses it (Q#KR11). Without it a + detached frontend's pending state leaks for the life of the session. + +This costs one table level and buys correctness in the ordinary +TUI-plus-GPU configuration, which is not an exotic setup — it is the +one this project ships two frontends for. + **Abandonment is lazy, because there is no cursor-motion hook** (round-5 finding 3). Pending state is validated at the next typed edit and -discarded when any of these no longer holds: the record's buffer is the -pending buffer; `rec.effective_start` equals `start_offset + 1 + -#text` (the point is still at the end of the pending span); and the -buffer's `revision()` advanced by exactly the pending edit. `buffer. -after-switch` clears it eagerly since that hook *does* exist. The +discarded when any of these no longer holds: the record's buffer and +window are the pending ones; `rec.effective_start` equals `start_offset ++ 1 + #text` (the point is still at the end of the pending span); and +the buffer's `revision()` advanced by exactly the pending edit. +`buffer.after-switch` clears the acting frontend's entries eagerly, +since that hook *does* exist. The practical difference from upstream: a user who clicks away mid-`\alp` and types elsewhere gets the pending state dropped rather than expanded. Upstream expands it. **This is a deliberate divergence** — expanding @@ -2138,6 +2343,11 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage. Per the no-renumbering rule above, round 5's additions take letter suffixes on both sides of the split. +46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which +is part of Stage 4a's declared footprint (Q#LN10) and a required gate +for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which +criterion 46 requires to stay byte-identical. + 46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs` suite passes **unmodified**. A suite edited to accommodate the refactor proves nothing; the diff for 4a must show zero lines @@ -2164,8 +2374,12 @@ suffixes on both sides of the split. **Stage 4b — the Unicode input method** -38. `\alpha` + space yields `α`; the whole expansion is a single undo - step, and one undo restores `\alpha` rather than `\alph`. +38. `\alpha` + space yields `α ` — the space lands first and the + expansion runs in the following `buffer.after-edit`, so the + terminator is **retained**, not consumed. The expansion is a single + undo step: one undo restores `\alpha ` (with its space), not + `\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be + true only if the terminator were swallowed. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. 40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is @@ -2211,6 +2425,14 @@ suffixes on both sides of the split. because the expansion is a programmatic replace that arms no record. Bites against a future consumer that infers pending state from buffer text instead of provenance. +45i. **Pending state is per frontend (Q#LN22).** Two frontends attached + to the same `lean4` buffer: A types `\al`, B types `\to` + space in + the same buffer. B's expansion yields `→` and leaves A's `\al` + pending and intact; A then typing `l` + space still yields `∀`. + Plus: B switching buffers does not clear A's pending state, and a + `frontend.detached` for B purges B's entries only. Bites against the + buffer-keyed design rev 6 specified — which passes every + single-frontend criterion above. 45f. **Both producers, and the CI-darkness stated.** The dispatch path is pinned by the criteria above. The optimistic CRDT producer (round-5 finding 4) is pinned by a separate criterion driving @@ -2222,11 +2444,30 @@ suffixes on both sides of the split. verified only locally and name the command. Silence here is the failure mode — a green CI would otherwise read as covering the path most users take. -45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips: - its entry count matches the header's declared count, and a spot set - of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches - `abbreviations.json` byte-for-byte. Bites against a generator that - silently drops or mangles keys (Q#LN11). +45g. **Table integrity — what the suite can actually check.** + `abbreviations.json` is not shipped, so the suite cannot diff + against it and rev 6's "matches byte-for-byte" was unbuildable; a + count plus seven spot entries could not prove 1,855 round-trip + anyway. The full source-fidelity check belongs to the generator + (Q#LN11: re-parse own output, compare the ordered sequence entry for + entry, fail on any difference). What the suite pins instead are + self-consistency properties that a corrupt emit breaks: + - the loaded sequence's length equals the header's declared count, + and equals the declared count for the recorded upstream commit; + - every key is unique, and the derived `key → index` lookup has the + same cardinality as the sequence (a collision would silently drop + entries); + - every key and symbol is well-formed UTF-8, and no symbol contains + `$CURSOR` more than once; + - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`, + `n`, `setminus`, and the tie cases from 45h. +45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` — + `f<` and `f>` are both length 2, and `f<` is declared first. Same + for `\"` + space → `Ä`, first of eleven equal-length candidates. + **This is the criterion that bites a map-shaped vendored table**: + with `pairs` iteration it passes or fails by hash order, so it must + also be run against a deliberately reversed sequence and shown to + fail. 101 prefixes are exposed to this rule. **Stage 5 — the goal view** @@ -2294,7 +2535,7 @@ suffixes on both sides of the split. discipline on transformed source edits, and Q#AP1's optimistic-classifier limitation. Stage 4a generalizes the first; 4b is built on all three. - **#127 (config registry)** — `pmacs.config.define` and the - source-buffer-resolution correction. Q#LN10's gate follows + source-buffer-resolution correction. Q#LN22's gate follows `editing.auto-pair` exactly. - **#129 (mode system)** — mode-scoped keymaps for Stage 5. - **#155 (bottom panel)** — `pmacs.window.display` and the panel adopter @@ -2381,9 +2622,10 @@ PR. (config registry) secondarily, by adding one option in the established shape rather than a new switch mechanism. -**Golden journey (§2).** No step is touched by 4a. 4b improves step 4 -(editing) for Lean specifically and changes nothing for any other -language: the pending-abbreviation state exists only in `lean4` buffers. +**Golden journey (§2).** No step is touched by 4a. 4b improves **step 5 +("Edit immediately")** for Lean specifically and changes nothing for any +other language — rev 6 cited step 4, which is "Understand the visible +interface" and is untouched by both stages: the pending-abbreviation state exists only in `lean4` buffers. Neither stage changes launch, open, or attach. **Interaction islands (§6).** **None added, and this is the load-bearing From 174e36fce384375b94c4c84af5a7a27f41e318da Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 10:49:43 -0400 Subject: [PATCH 3/7] docs(lean4): reconcile peer edits with pending ownership Advance the Stage 4 framing to revision 8. Keep pending abbreviation state frontend-owned while conservatively invalidating it after any intervening shared-buffer edit, make the revision token explicit, and rewrite acceptance 45i around that contract. Correct the active-work multi-codepoint count and the stale coherence revision label. --- docs/active-work.md | 18 ++++++++--- docs/lean4-mode-framing.md | 62 ++++++++++++++++++++++++++++++-------- 2 files changed, 63 insertions(+), 17 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index 47c3677..cf4ea6e 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -64,17 +64,17 @@ If it does not, stop and repair the remote/fetch configuration. 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 7 + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8 carries the decisions. -### Stage 4 — framing rev 7, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) - Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main that had advanced 50 commits mid-review; the only conflict either time was this ledger's own lane headings, resolved by keeping both sides. - Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. - Framing-only so far: `docs/lean4-mode-framing.md` **revision 7**. No + Framing-only so far: `docs/lean4-mode-framing.md` **revision 8**. No code. Awaiting user approval before implementation, per the workflow. - **Round 6 review found five P1s, four of them internal to rev 6** — facts about pmacs the revision asserted without checking, while its @@ -93,6 +93,15 @@ If it does not, stop and repair the remote/fetch configuration. 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 @@ -130,7 +139,8 @@ If it does not, stop and repair the remote/fetch configuration. - 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`, **93** are multi-codepoint. + 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, diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index ca50696..650b2f3 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -46,7 +46,7 @@ during a rebase. ## 0.1 Revision history -Revision 1 — initial. Current revision: **7**. +Revision 1 — initial. Current revision: **8**. ### Round 1 (rev 1 → rev 2) @@ -480,6 +480,29 @@ section cites golden-journey **step 5** ("Edit immediately"), not step 4; and §8's config-registry prior art points at Q#LN22, where the gate now lives. +### Round 7 (rev 7 → rev 8) + +One P1 remained in the new multi-frontend acceptance, plus two +documentation cleanups. + +1. **Acceptance 45i contradicted Q#LN22's conservative abandonment + rule.** It required frontend A's pending abbreviation to survive + frontend B editing the same buffer, but `buffer:revision()` is + buffer-global and advances on every edit. B's first edit therefore + invalidates A's record under the exact-revision guard. The criterion + now separates the two contracts: another frontend cannot consume A's + record, but any intervening edit to their shared buffer invalidates + it lazily; navigation and detachment remain frontend-scoped when no + shared-buffer edit intervenes. The pending record now names its + `expected_revision` explicitly so the validation rule is buildable. + Preserving A's record through peer edits would require translating + and validating its span across arbitrary edits, a substantially + larger substrate change that Stage 4b does not take on. +2. **The volatile ledger retained rev 6's undercount.** Its table facts + now say 119 multi-codepoint symbols — 26 `$CURSOR`-bearing and 93 + others — matching §2.11 and Q#LN11. +3. **§9.1's revision label was stale.** It now names rev 8. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1640,8 +1663,9 @@ that an edit was made. reconstruction of it: - `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer, - window, start_offset, text = "" }`, keyed on **`(frontend, buffer)`** — - see below. + window, start_offset, text = "", expected_revision }`, keyed on + **`(frontend, buffer)`** — see below. `expected_revision` is the + buffer's revision after that leader edit. - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. @@ -1685,7 +1709,14 @@ finding 3). Pending state is validated at the next typed edit and discarded when any of these no longer holds: the record's buffer and window are the pending ones; `rec.effective_start` equals `start_offset + 1 + #text` (the point is still at the end of the pending span); and -the buffer's `revision()` advanced by exactly the pending edit. +the buffer's `revision()` equals `expected_revision + 1`, meaning the +current typed edit is the only edit since this frontend last extended +the pending abbreviation. A claimed extension stores the current +revision as the new `expected_revision`. This is deliberately +conservative across frontends: any intervening edit to the shared +buffer invalidates the pending record even if it occurred elsewhere. +Keeping the record alive would require translating and validating its +span through arbitrary peer edits, substrate Stage 4b does not add. `buffer.after-switch` clears the acting frontend's entries eagerly, since that hook *does* exist. The practical difference from upstream: a user who clicks away mid-`\alp` @@ -2425,14 +2456,19 @@ criterion 46 requires to stay byte-identical. because the expansion is a programmatic replace that arms no record. Bites against a future consumer that infers pending state from buffer text instead of provenance. -45i. **Pending state is per frontend (Q#LN22).** Two frontends attached - to the same `lean4` buffer: A types `\al`, B types `\to` + space in - the same buffer. B's expansion yields `→` and leaves A's `\al` - pending and intact; A then typing `l` + space still yields `∀`. - Plus: B switching buffers does not clear A's pending state, and a - `frontend.detached` for B purges B's entries only. Bites against the - buffer-keyed design rev 6 specified — which passes every - single-frontend criterion above. +45i. **Pending state is per frontend, with conservative shared-buffer + invalidation (Q#LN22).** Two frontends share a `lean4` buffer at + distinct points. A types `\al`; B types `p`. B's `p` lands normally + at B's point rather than extending A's record. Because that edit + advances the shared buffer's revision, A then typing `l` + space + leaves literal `\all ` rather than expanding: A's stale record is + abandoned lazily. In a fresh setup, A types `\al`, B switches + buffers **without editing the shared buffer**, and A typing `l` + + space still yields `∀`; B's switch clears only B's entries. Finally, + `frontend.detached` for B purges B's entries only and does not clear + a still-valid A record. Bites both against the buffer-keyed design + rev 6 specified and against the impossible rev-7 promise that + pending state survives arbitrary peer edits. 45f. **Both producers, and the CI-darkness stated.** The dispatch path is pinned by the criteria above. The optimistic CRDT producer (round-5 finding 4) is pinned by a separate criterion driving @@ -2615,7 +2651,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 6) +### 9.1 Coherence impact — stages 4a and 4b (rev 8) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 From 24ca9062944d639e4aa90c3567a9e67c4497e49b Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:00:03 -0400 Subject: [PATCH 4/7] feat(typed-edit): the typed-edit consumer chain (Arc 8 Stage 4a) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `pmacs.editor.take_typed_edit()` is one-shot and per-frontend (Q#AP9): the first `buffer.after-edit` callback to call it clears the slot, and every later callback in the same fan-out sees nil. That was survivable only because auto-pairing was the sole consumer — never a property anyone chose. A second independent caller would get nil or steal the record from pairing depending on hook registration order, and registration order is not a contract. This makes it one. `builtin/runtime/typed_edit.lua` owns the single after-edit subscriber that reads the record, and offers that one read to consumers registered through `pmacs.typed_edit.add_consumer{ name, priority, fn }`: lowest priority first, ties by registration order, and the first consumer to return truthy claims the edit and stops the chain. `pair.lua` becomes that chain's only consumer, at priority 100. No Lean content. Stage 4b's abbreviation expander is what needs the ordering guarantee (64 of its 1,855 keys contain a `lean4` pair-set character, so pairing running first corrupts them), but the chain is substrate every language runs through, which is why it ships alone — framing Q#LN10, and §4's rule that no PR in this arc mixes a cross-cutting substrate change with Lean feature content. Three design points worth review attention: - Consumers are called even when the record is nil. "This fan-out carried no typed edit" is information a consumer acts on: it is how pairing's test seam observes a non-event, and how Stage 4b will abandon a pending abbreviation an unrelated edit invalidated. Three existing auto-pairing tests fail if the chain skips consumers on nil. - The chain pcalls each consumer. `buffer.after-edit` is all-must-succeed, so a throwing consumer would otherwise fail the fan-out for every other subscriber, including lsp.lua's didChange flush. Behavior-preserving for pairing, which already never throws. - Ordered insertion, not `table.sort`, which is not stable in Lua — "ties by registration order" is a stated contract, not a coincidence. `tests/auto_pair_acceptance.rs` is UNCHANGED — zero lines — and its 45 tests pass. That is criterion 46 and the whole no-behavior-change claim; a suite edited to accommodate the refactor would prove nothing. `tests/typed_edit_chain_acceptance.rs` adds 9 tests for criteria 46a-46e. Every one is bite-verified by mutation: appending instead of ordered insert (5 fail), `>=` for the tiebreak (1), re-taking per consumer (4), ignoring the claim (1), dropping the pcall (1), skipping nil fan-outs (1 here plus 3 in the untouched auto-pair suite), and loading the chain after lsp.lua (the Q#AP7 flush test fails, alongside the two existing pairing ones). Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/pair.lua | 85 +++-- builtin/runtime/typed_edit.lua | 112 ++++++ src/editor.rs | 15 + tests/typed_edit_chain_acceptance.rs | 517 +++++++++++++++++++++++++++ 4 files changed, 699 insertions(+), 30 deletions(-) create mode 100644 builtin/runtime/typed_edit.lua create mode 100644 tests/typed_edit_chain_acceptance.rs diff --git a/builtin/runtime/pair.lua b/builtin/runtime/pair.lua index 9ed9d1f..5869dce 100644 --- a/builtin/runtime/pair.lua +++ b/builtin/runtime/pair.lua @@ -4,20 +4,30 @@ -- next char is already `)` steps over it instead of doubling it. The -- carrier is a `buffer.after-edit` reaction (Q#AP1): the opener stays -- a genuine single-codepoint self-insert — the classification --- signature help depends on — and this hook inserts (or swallows) the --- closer as a second edit. Provenance is the exact one-shot typed-edit --- record (`pmacs.editor.take_typed_edit()`, Q#AP9), not buffer-text --- inference: pastes, programmatic edits, manual hook runs, and a stale --- `this_command` have no record and never pair, and a transformed, --- relocated, or context-switching source self-insert fails closed. +-- signature help depends on — and this reaction inserts (or swallows) +-- the closer as a second edit. Provenance is the exact one-shot +-- typed-edit record (`pmacs.editor.take_typed_edit()`, Q#AP9), not +-- buffer-text inference: pastes, programmatic edits, manual hook runs, +-- and a stale `this_command` have no record and never pair, and a +-- transformed, relocated, or context-switching source self-insert fails +-- closed. -- --- This chunk loads BEFORE lsp.lua (Q#AP7): registration order is hook --- execution order, and lsp.lua's after-edit callback synchronously --- flushes didChange on the signature-trigger path — the closer must --- already be in the buffer when that callback runs. Everything under --- `pmacs.lsp` is therefore looked up lazily at callback time. +-- Since Arc 8 Stage 4a (Q#LN10) pairing no longer subscribes to +-- `buffer.after-edit` itself. It registers on the typed-edit chain +-- (`builtin/runtime/typed_edit.lua`), which owns the single subscriber +-- and the single one-shot read. Everything above still holds — the +-- record is the same record — but the chain, not this file, decides +-- who sees it and in what order. -- --- Framing: docs/auto-pairing-framing.md. +-- This chunk loads AFTER typed_edit.lua (it registers into it) and +-- BEFORE lsp.lua (Q#AP7): registration order is hook execution order, +-- and lsp.lua's after-edit callback synchronously flushes didChange on +-- the signature-trigger path — the closer must already be in the +-- buffer when that callback runs. Everything under `pmacs.lsp` is +-- therefore looked up lazily at callback time. +-- +-- Framing: docs/auto-pairing-framing.md; Stage 4a in +-- docs/lean4-mode-framing.md Q#LN10. pmacs.pair = pmacs.pair or {} @@ -40,7 +50,7 @@ local ed = pmacs.editor -- Per-buffer on/off switch (Q#CR8's flagship adopter). Read against the -- SOURCE buffer of the typed edit, never the currently active one — see --- the hook body below, which resolves it the same way `set_for` resolves +-- the consumer body below, which resolves it the same way `set_for` resolves -- the buffer's pair set (round 2, finding 2): `rec.buffer`, not -- `pmacs.window.buffer()`. pmacs.config.define { @@ -214,28 +224,36 @@ end -- Acceptance tests flip `_capture_records` on; each fan-out then -- publishes the record it observed (or nil) to `_last_record`, which -- is how tests read the exact codepoint / effective triple and prove --- one-shot-ness (this callback registers first and consumes it). +-- one-shot-ness (the chain takes the record before any other +-- `buffer.after-edit` subscriber can, and hands it here). pmacs.pair._capture_records = false -pmacs.hook.add("buffer.after-edit", function() +-- The typed-edit consumer (Arc 8 Stage 4a, Q#LN10). `rec` is the one +-- record `typed_edit.lua` read for this fan-out — possibly nil, which +-- is why the capture seam below is updated before the nil guard. +-- Returns whether pairing CLAIMED the keystroke: true once it has +-- committed to reacting (a skip-over or a closer insert, landed or +-- intercept-rejected), false on every decline. Pairing is last of the +-- builtin consumers, so nothing currently observes that value; it is +-- stated correctly so it stays correct when something does. +local function on_typed_edit(rec) -- One-shot provenance (Q#AP9). Absence — paste, programmatic edit, -- manual hook run, rejected insert, a post-insert mutation by the -- command, stale `this_command` — is a silent non-event; only a -- live record for a pair-set character that then fails a gate -- reports. - local rec = ed.take_typed_edit and ed.take_typed_edit() if pmacs.pair._capture_records then pmacs.pair._last_record = rec end - if not rec then return end - if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return end + if not rec then return false end + if not (ed.this_command and ed.this_command() == "buffer.self-insert") then return false end -- The master switch, per-buffer (Q#CR4): the SOURCE buffer of the -- typed edit, resolved buffer-local -> global -> default(true). A -- second buffer of the same language is untouched by a buffer-local -- override here (acceptance 29). - if not pmacs.config.get("editing.auto-pair", rec.buffer) then return end + if not pmacs.config.get("editing.auto-pair", rec.buffer) then return false end local buf = pmacs.window.buffer() - if not buf then return end + if not buf then return false end -- Relevance first (PR #110 round 1, finding 2): pairing has no -- interest in characters outside the set, so a transformed or @@ -247,14 +265,14 @@ pmacs.hook.add("buffer.after-edit", function() -- Rust. local ch = rec.char local openers, closers = maps_for(set_for(rec.buffer)) - if not (openers[ch] or closers[ch]) then return end + if not (openers[ch] or closers[ch]) then return false end -- Fail closed on a transformed source self-insert (Q#AP3): the -- intercept's positional result stands as produced; pairing on top -- of a relocated or expanded opener would compound it. if not rec.clean then ed.set_status("auto-pair skipped: source self-insert transformed") - return + return false end -- Fail closed when the source edit's context is no longer current: -- an intercept switched window/buffer, or something moved the @@ -268,14 +286,14 @@ pmacs.hook.add("buffer.after-edit", function() or pmacs.window.current() ~= rec.window or ed.cursor() ~= rec.post_cursor then ed.set_status("auto-pair skipped: source context changed") - return + return false end -- Region guard (Q#AP3/Q#AP6): on the dispatch route type-over has -- already consumed and cleared the region. A region surviving the -- edit means the TUI's selection-blind optimistic gate let a custom -- pair char through (named deferral) — reacting would pile a closer -- onto an unconsumed region. - if ed.region() ~= nil then return end + if ed.region() ~= nil then return false end local cursor = rec.post_cursor @@ -294,19 +312,19 @@ pmacs.hook.add("buffer.after-edit", function() if not ok then -- The duplicate stays (e.g. `())`); report, no retry. ed.set_status("auto-pair skip rejected by buffer intercept") - return + return true end if estart ~= cursor or estop ~= cursor + #ch or einserted ~= 0 then ed.set_status("auto-pair skip altered by buffer intercept") repair_cursor(win0, buf, cursor, estart, estop, einserted) end - return + return true end end local closer = openers[ch] - if not closer then return end - if not should_pair(buf, cursor, closers) then return end + if not closer then return false end + if not should_pair(buf, cursor, closers) then return false end local win0 = pmacs.window.current() local ok, estart, estop, einserted = pcall(function() @@ -315,7 +333,7 @@ pmacs.hook.add("buffer.after-edit", function() if not ok then -- Nothing landed; the opener stands alone. ed.set_status("auto-pair closer rejected by buffer intercept") - return + return true end if estart ~= cursor or estop ~= cursor or einserted ~= #closer then ed.set_status("auto-pair closer altered by buffer intercept") @@ -324,4 +342,11 @@ pmacs.hook.add("buffer.after-edit", function() -- Clean path: no cursor motion — the insert landed at the cursor -- and Lua mutators move no cursors, so it already sits between the -- pair; the daemon's per-tick CursorByte re-grounds both frontends. -end) + return true +end + +pmacs.typed_edit.add_consumer { + name = "auto-pair", + priority = 100, + fn = on_typed_edit, +} diff --git a/builtin/runtime/typed_edit.lua b/builtin/runtime/typed_edit.lua new file mode 100644 index 0000000..59f7366 --- /dev/null +++ b/builtin/runtime/typed_edit.lua @@ -0,0 +1,112 @@ +-- typed_edit.lua --- the typed-character consumer chain (Arc 8 Stage 4a). +-- +-- `pmacs.editor.take_typed_edit()` is ONE-SHOT and per-frontend (Q#AP9): +-- the first `buffer.after-edit` callback to call it clears the slot, and +-- every later callback in the same fan-out --- including a nested manual +-- `pmacs.hook.run` --- sees nil. That was survivable only because +-- auto-pairing was the sole consumer, which was never a property anyone +-- chose. A second independent caller gets nil or steals the record from +-- pairing depending on hook registration order, and registration order +-- is not a contract. +-- +-- This module makes it one. It owns the single `buffer.after-edit` +-- subscriber that reads the record, and offers that one read to +-- consumers registered through `pmacs.typed_edit.add_consumer`: +-- +-- pmacs.typed_edit.add_consumer { +-- name = "auto-pair", -- for error reporting; must be unique-ish +-- priority = 100, -- LOWEST runs FIRST +-- fn = function(rec) ... return claimed end, +-- } +-- +-- A consumer returns whether it CLAIMED the edit; the first that claims +-- stops the chain. "Claimed" means the chain stops, not that an edit was +-- made --- Stage 4b's abbreviation expander claims every keystroke that +-- extends a pending abbreviation precisely so that auto-pairing does not +-- also react to it (Q#LN22). +-- +-- Priority is an explicit number rather than load-order-implied, because +-- the ordering is load-bearing (Q#LN22: 64 Lean abbreviation keys +-- contain a character in the `lean4` pair set, and pairing running first +-- corrupts them) and a reader must be able to check it without +-- reconstructing `src/editor.rs`'s include list. +-- +-- ORDERING CONTRACT: this chunk loads BEFORE pair.lua, which registers +-- into it, and therefore before lsp.lua. That preserves Q#AP7 --- see +-- pair.lua's header and the load site in `src/editor.rs`. +-- +-- Framing: docs/lean4-mode-framing.md Q#LN10. + +pmacs.typed_edit = pmacs.typed_edit or {} + +-- Consumers in run order: lowest `priority` first, registration order +-- breaking ties. Maintained by ordered INSERTION rather than +-- `table.sort`, which is not stable in Lua --- equal priorities would +-- otherwise resolve arbitrarily, and "ties broken by registration +-- order" is part of the stated contract, not an incidental property. +local consumers = {} + +-- Register a typed-edit consumer. Argument errors throw: registration +-- happens at chunk-load or config-load time, where a throw is a visible +-- startup failure rather than a silently missing feature. Nothing in +-- the after-edit path throws --- see the fan-out below. +function pmacs.typed_edit.add_consumer(spec) + if type(spec) ~= "table" then + error("pmacs.typed_edit.add_consumer: spec must be a table", 2) + end + local name, priority, fn = spec.name, spec.priority, spec.fn + if type(name) ~= "string" or name == "" then + error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2) + end + if type(priority) ~= "number" then + error("pmacs.typed_edit.add_consumer: " .. name .. + ": priority must be a number", 2) + end + if type(fn) ~= "function" then + error("pmacs.typed_edit.add_consumer: " .. name .. + ": fn must be a function", 2) + end + + -- STRICTLY-greater comparison, so a new consumer lands AFTER every + -- already-registered consumer of equal priority. That is exactly the + -- registration-order tiebreak; `>=` here would silently reverse it. + local at = #consumers + 1 + for i, c in ipairs(consumers) do + if c.priority > priority then + at = i + break + end + end + table.insert(consumers, at, { name = name, priority = priority, fn = fn }) +end + +pmacs.hook.add("buffer.after-edit", function() + local ed = pmacs.editor + -- ONE read for the whole fan-out (Q#AP9). The record may be nil --- + -- paste, programmatic mutation, manual hook run, a replicated CRDT + -- op, a stale `this_command` --- and consumers are called ANYWAY, + -- with nil. That is deliberate: "this fan-out carried no typed edit" + -- is information a consumer acts on. Auto-pairing's test seam + -- observes the non-event through it, and Stage 4b abandons a pending + -- abbreviation that an unrelated edit invalidated. Skipping the + -- fan-out on nil would leave both reading stale state. + local rec = ed.take_typed_edit and ed.take_typed_edit() + + for _, c in ipairs(consumers) do + -- `buffer.after-edit` is all-must-succeed (builtin/hooks/default.lua): + -- a throwing consumer would fail the fan-out for every OTHER + -- subscriber, including lsp.lua's didChange flush. Contain it, + -- report it, and keep going --- a broken consumer must not be able + -- to stop the editor from telling the language server what changed. + -- This matches pair.lua's existing never-throw-from-after-edit + -- discipline; it does not weaken the hook's contract for anyone + -- else, because the chain itself still never fails. + local ok, claimed = pcall(c.fn, rec) + if not ok then + ed.set_status("typed-edit consumer '" .. c.name .. "' failed: " .. + tostring(claimed)) + elseif claimed then + return + end + end +end) diff --git a/src/editor.rs b/src/editor.rs index dcff55a..673ded6 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -415,6 +415,18 @@ impl EditorState { include_str!("../builtin/runtime/listview.lua"), ) .expect("load listview builtin chunk"); + // The typed-edit consumer chain (Arc 8 Stage 4a, Q#LN10) — + // ORDERING CONTRACT: typed_edit.lua must load BEFORE pair.lua, + // which registers a consumer into it, and therefore before + // lsp.lua. It owns the single `buffer.after-edit` subscriber + // that reads the one-shot typed-edit record, so its + // registration position is what preserves Q#AP7 below. + lua_host + .eval( + Some("@pmacs/builtin/runtime/typed_edit.lua"), + include_str!("../builtin/runtime/typed_edit.lua"), + ) + .expect("load typed_edit builtin chunk"); // Auto-pairing (Arc 2, Q#AP7) — ORDERING CONTRACT: pair.lua // must load BEFORE lsp.lua. Hook callbacks run in registration // order, and lsp.lua's `buffer.after-edit` callback flushes @@ -424,6 +436,9 @@ impl EditorState { // the closer stays unsynchronized until the next edit (hook // edits don't re-fire the hook). pair.lua's `pmacs.lsp.*` // lookups are lazy and nil-guarded for the same reason. + // Since Stage 4a the closer is inserted from the chain's + // subscriber rather than pair.lua's own, which is registered + // one chunk earlier — strictly safer for this contract. lua_host .eval( Some("@pmacs/builtin/runtime/pair.lua"), diff --git a/tests/typed_edit_chain_acceptance.rs b/tests/typed_edit_chain_acceptance.rs new file mode 100644 index 0000000..c0170f4 --- /dev/null +++ b/tests/typed_edit_chain_acceptance.rs @@ -0,0 +1,517 @@ +//! Typed-edit consumer chain acceptance (Arc 8 Stage 4a, +//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46e). +//! +//! The chain owns the single `buffer.after-edit` subscriber that reads +//! the one-shot typed-edit record (Q#AP9) and offers it to consumers in +//! priority order. These tests pin the chain's OWN behavior — take-once, +//! priority ordering, claim-stops-chain, throw containment, and the +//! Q#AP7 flush ordering it inherited from `pair.lua`. +//! +//! They deliberately do not re-test auto-pairing: criterion 46 requires +//! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that +//! suite is the no-behavior-change pin. Pairing appears here only as +//! the chain's last consumer, which is how 46c observes that a claim +//! really stopped the chain. +//! +//! Dispatch-driven throughout: `dispatch_key` is the producer that arms +//! the record for a grid frontend. + +use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; +use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; +use pmacs::protocol::FrontendId; +use std::path::PathBuf; +use std::sync::atomic::{AtomicUsize, Ordering}; +use std::time::{Duration, Instant}; + +fn fresh_state_dir() -> PathBuf { + static SEQ: AtomicUsize = AtomicUsize::new(0); + let dir = std::env::temp_dir().join(format!( + "pmacs-typededit-{}-{}", + std::process::id(), + SEQ.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir_all(&dir).unwrap(); + dir +} + +fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent { + KeyEvent { + code, + modifiers: mods, + kind: KeyEventKind::Press, + state: KeyEventState::NONE, + } +} + +fn type_str(s: &mut EditorState, text: &str) { + for ch in text.chars() { + s.dispatch_key( + FrontendId::LOCAL, + key(KeyCode::Char(ch), KeyModifiers::NONE), + ); + } +} + +fn exec(s: &EditorState, src: &str) { + s.lua_host.lua().load(src.to_string()).exec().unwrap(); +} + +fn eval(s: &EditorState, src: &str) -> T { + s.lua_host.lua().load(src.to_string()).eval().unwrap() +} + +fn buffer_text(s: &EditorState) -> String { + let b: mlua::String = eval( + s, + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ); + String::from_utf8_lossy(&b.as_bytes()).into_owned() +} + +fn status(s: &EditorState) -> String { + s.core.borrow().status.clone() +} + +/// Fresh scratch-buffer editor, cursor at 0. Scratch pairing uses the +/// `default` set, so `(` pairs — which is what 46c reads. +fn editor_with(body: &str) -> EditorState { + let s = EditorState::new(); + if !body.is_empty() { + exec(&s, &format!("pmacs.window.buffer():insert(0, {body:?})")); + } + exec(&s, "pmacs.editor.goto_byte(0)"); + s +} + +// --------------------------------------------------------------------------- +// 46a — one read for the whole fan-out +// --------------------------------------------------------------------------- + +#[test] +fn chain_reads_the_record_once_and_hands_the_same_one_to_every_consumer() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.seen = {} + local function spy(tag) + return function(rec) + -- Each consumer independently attempts its own take. Under + -- the pre-chain design this is exactly what a second + -- consumer would have done, and exactly what would have + -- returned nil (or stolen the record from pairing). + local own = pmacs.editor.take_typed_edit() + _G.seen[#_G.seen + 1] = { + tag = tag, + char = rec and rec.char, + post_cursor = rec and rec.post_cursor, + clean = rec and rec.clean, + own_take_was_nil = (own == nil), + } + return false + end + end + pmacs.typed_edit.add_consumer { name = "spy-a", priority = 1, fn = spy("a") } + pmacs.typed_edit.add_consumer { name = "spy-b", priority = 2, fn = spy("b") } + "#, + ); + + type_str(&mut s, "x"); + + let (n, a_char, b_char, a_pc, b_pc, a_clean, b_clean, a_nil, b_nil): ( + i64, + String, + String, + i64, + i64, + bool, + bool, + bool, + bool, + ) = eval( + &s, + " + local a, b = _G.seen[1], _G.seen[2] + return #_G.seen, a.char, b.char, a.post_cursor, b.post_cursor, + a.clean, b.clean, a.own_take_was_nil, b.own_take_was_nil + ", + ); + + assert_eq!(n, 2, "both consumers ran for one typed character"); + // The same record, not two reads of a slot that only one could win. + assert_eq!(a_char, "x"); + assert_eq!(b_char, "x", "the second consumer sees the record too"); + assert_eq!((a_pc, b_pc), (1, 1), "identical post_cursor"); + assert!(a_clean && b_clean, "identical clean verdict"); + // ...and the chain, not the consumers, did the taking. + assert!( + a_nil && b_nil, + "a consumer's own take_typed_edit() observes nil — the chain \ + already consumed the one-shot slot (Q#AP9)" + ); +} + +#[test] +fn consumers_run_when_the_fan_out_carries_no_record() { + // The chain calls consumers with nil rather than skipping them. + // Three tests in the auto-pairing suite depend on this (they assert + // `_last_record == nil` after a record-less fan-out), so it is a + // load-bearing decision and not an implementation detail. + let s = editor_with(""); + exec( + &s, + r#" + _G.calls, _G.nil_calls = 0, 0 + pmacs.typed_edit.add_consumer { + name = "nil-spy", priority = 1, + fn = function(rec) + _G.calls = _G.calls + 1 + if rec == nil then _G.nil_calls = _G.nil_calls + 1 end + return false + end, + } + "#, + ); + + // A manual fan-out arms no record. + exec(&s, "pmacs.hook.run(\"buffer.after-edit\")"); + + let (calls, nil_calls): (i64, i64) = eval(&s, "return _G.calls, _G.nil_calls"); + assert_eq!(calls, 1, "the consumer ran"); + assert_eq!(nil_calls, 1, "and was handed nil, not skipped"); +} + +// --------------------------------------------------------------------------- +// 46b — priority order, not registration order +// --------------------------------------------------------------------------- + +#[test] +fn consumers_run_in_priority_order_not_registration_order() { + let mut s = editor_with(""); + // Registered HIGH priority first. If the chain honored registration + // order (or `include_str!` order, which is the same failure dressed + // differently), the observed order would be the registration order. + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + pmacs.typed_edit.add_consumer { name = "late", priority = 30, fn = mark("late") } + pmacs.typed_edit.add_consumer { name = "early", priority = 10, fn = mark("early") } + pmacs.typed_edit.add_consumer { name = "mid", priority = 20, fn = mark("mid") } + "#, + ); + + type_str(&mut s, "x"); + + let order: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + order, "early,mid,late", + "lowest priority runs first, regardless of when it registered" + ); +} + +#[test] +fn equal_priorities_break_by_registration_order() { + // The stated tiebreak. Lua's `table.sort` is not stable, so this + // bites an implementation that sorts instead of inserting in place. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + pmacs.typed_edit.add_consumer { name = "first", priority = 5, fn = mark("first") } + pmacs.typed_edit.add_consumer { name = "second", priority = 5, fn = mark("second") } + pmacs.typed_edit.add_consumer { name = "third", priority = 5, fn = mark("third") } + "#, + ); + + type_str(&mut s, "x"); + + let order: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!(order, "first,second,third"); +} + +// --------------------------------------------------------------------------- +// 46c — a claim stops the chain +// --------------------------------------------------------------------------- + +#[test] +fn a_claiming_consumer_stops_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "claimer", priority = 1, fn = function() return true end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(!later_ran, "a later consumer must not run after a claim"); + // Pairing is the chain's last consumer at priority 100, so the + // claim is observable in the buffer: no closer was inserted. This + // is the assertion that makes the criterion about behavior rather + // than about a bookkeeping flag. + assert_eq!( + buffer_text(&s), + "(", + "auto-pairing never ran, so the opener stands alone" + ); +} + +#[test] +fn a_non_claiming_consumer_does_not_stop_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "passer", priority = 1, fn = function() return false end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(later_ran, "a declining consumer passes the edit along"); + assert_eq!( + buffer_text(&s), + "()", + "and pairing, still last in the chain, reacted normally" + ); +} + +// --------------------------------------------------------------------------- +// 46d — a throwing consumer is contained +// --------------------------------------------------------------------------- + +#[test] +fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() { + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + pmacs.typed_edit.add_consumer { + name = "boom", priority = 1, + fn = function() error("consumer exploded") end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + // `buffer.after-edit` is all-must-succeed: an uncontained throw + // would fail the fan-out for every other subscriber, including + // lsp.lua's didChange flush. + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!(later_ran, "a throwing consumer must not stop the chain"); + assert_eq!( + buffer_text(&s), + "()", + "and pairing still ran — the fan-out survived the throw" + ); + let st = status(&s); + assert!( + st.contains("boom") && st.contains("consumer exploded"), + "the failure is reported by consumer name and message, got {st:?}" + ); +} + +#[test] +fn add_consumer_rejects_malformed_registrations() { + let s = editor_with(""); + for (src, want) in [ + ( + "pmacs.typed_edit.add_consumer(\"nope\")", + "spec must be a table", + ), + ( + "pmacs.typed_edit.add_consumer{ priority = 1, fn = function() end }", + "name must be a non-empty string", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }", + "priority must be a number", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }", + "fn must be a function", + ), + ] { + let err = s + .lua_host + .lua() + .load(src.to_string()) + .exec() + .expect_err("malformed registration must throw"); + let msg = err.to_string(); + assert!( + msg.contains(want), + "expected {want:?} in the error for {src:?}, got {msg:?}" + ); + } +} + +// --------------------------------------------------------------------------- +// 46e — the Q#AP7 flush ordering the chain inherited +// --------------------------------------------------------------------------- + +fn fake_lsp_path() -> String { + env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned() +} + +fn pump_lua_flag(state: &mut EditorState, flag: &str, secs: u64) -> bool { + let deadline = Instant::now() + Duration::from_secs(secs); + loop { + state.tick_processes(); + state.tick_lsp(); + state.tick_async(); + let done: bool = state + .lua_host + .lua() + .load(format!("return ({flag}) == true")) + .eval() + .unwrap_or(false); + if done { + return true; + } + if Instant::now() >= deadline { + return false; + } + std::thread::sleep(Duration::from_millis(10)); + } +} + +/// The `text` of every `textDocument/didChange` line in the sink, in +/// arrival order. +fn did_change_texts(sink: &std::path::Path) -> Vec { + let Ok(raw) = std::fs::read_to_string(sink) else { + return Vec::new(); + }; + raw.lines() + .filter_map(|l| serde_json::from_str::(l).ok()) + .filter(|v| v.get("method").and_then(|m| m.as_str()) == Some("textDocument/didChange")) + .filter_map(|v| v.get("text").and_then(|t| t.as_str()).map(str::to_owned)) + .collect() +} + +#[test] +fn a_chain_consumers_edit_reaches_the_first_did_change() { + // Q#AP7 generalized from pairing to the chain: lsp.lua's after-edit + // callback flushes didChange SYNCHRONOUSLY on the signature-trigger + // path, so every reaction to a typed character must already be in + // the buffer when it runs. The auto-pairing suite pins this for + // pairing; this pins it for the chain itself, which is what now + // owns the registration position. + // + // Falsified by loading typed_edit.lua after lsp.lua in + // `src/editor.rs`: the consumer's text would then arrive in the + // SECOND didChange, or not at all. + let dir = fresh_state_dir(); + let sink = dir.join("changes.jsonl"); + let sink_disp = sink.display().to_string(); + let fake = fake_lsp_path(); + + let mut s = EditorState::new(); + s.lua_host.lua().remove_app_data::(); + s.lua_host.lua().set_app_data(StateDir(dir.clone())); + exec(&s, "pmacs.lsp.config = {}"); + exec( + &s, + &format!( + "pmacs.lsp.config.rust = {{ + command = '{fake}', + env = {{ + PMACS_FAKE_LSP_MODE = 'sighelp', + PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}', + }}, + }}" + ), + ); + + // A consumer that appends a marker of its own, ahead of pairing. + // It declines the claim so pairing still runs — the assertion is + // about ordering against the flush, not about claiming. + exec( + &s, + r#" + pmacs.typed_edit.add_consumer { + name = "marker", priority = 1, + fn = function(rec) + if not rec then return false end + if rec.char ~= "(" then return false end + local buf = pmacs.window.buffer() + buf:insert(buf:len(), "Z") + return false + end, + } + "#, + ); + + let f = dir.join("a.rs"); + std::fs::write(&f, "\n").unwrap(); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let initialized = "(function() \ + for _,r in ipairs(pmacs.lsp.list()) do \ + if r.state and r.state.kind=='initialized' then return true end \ + end \ + return false \ + end)()"; + assert!(pump_lua_flag(&mut s, initialized, 5), "fake server init"); + + type_str(&mut s, "("); + assert_eq!( + buffer_text(&s), + "()\nZ", + "both the chain consumer's marker and pairing's closer landed" + ); + + let deadline = Instant::now() + Duration::from_secs(5); + let changes = loop { + s.tick_processes(); + s.tick_lsp(); + s.tick_async(); + let c = did_change_texts(&sink); + if !c.is_empty() { + break c; + } + assert!( + Instant::now() < deadline, + "no didChange reached the fake server" + ); + std::thread::sleep(Duration::from_millis(10)); + }; + assert_eq!( + changes[0], "()\nZ", + "the FIRST didChange carries BOTH reactions — the chain ran \ + before lsp.lua's synchronous flush (Q#AP7)" + ); +} From c7072b49e9e7ef427fd449100aa3d3ed5b70f80a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:05:41 -0400 Subject: [PATCH 5/7] docs: record the Stage 4a lane and its bite table Verification describes the pushed tree, per the standing rule. Includes the bite that was worthless as first written: moving only typed_edit.lua past lsp.lua broke the runtime load instead of testing flush ordering. A bite that kills everything has not isolated anything. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/active-work.md | 56 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 53 insertions(+), 3 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index cf4ea6e..bd0c0b1 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -57,7 +57,7 @@ git status --short --branch The `git log` command must expose `d152120` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. -## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING +## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4a IN REVIEW - **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full @@ -146,8 +146,58 @@ If it does not, stop and repair the remote/fetch configuration. `handle_server_requests` 1549→1815, `fs.stat` 93→133, `detect_buffer_language` 452→457, `send_request`/`send_notification` 9342/9361→9507/9527. -- Verification: none yet — the branch carries no code. `git diff --check` - clean. +### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) + +- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` + (new, 112 lines), `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, 9 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`. `buffer.after-edit` is all-must-succeed, so an + uncontained throw fails the fan-out for every other subscriber + including lsp.lua's didChange flush. +- **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) | + + 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 9/9; M4 121; required GPU 202; **isolated-config + workspace sweep 3,328 across 97 suites, zero failures** with + `grep -c basedpyright` = 0; `git diff --check` clean. +- Stage 4b (the input method) is NOT in this PR and not started. ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) From aef4e98c26ecb2c840c564e2a4f721241e229e0a Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:39:33 -0400 Subject: [PATCH 6/7] fix(typed-edit): close round-8 review on the consumer chain MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five defects in the chain itself, plus the stale handoff state. Each consumer now gets its own shallow copy of the typed-edit record. Handing everyone the same table let a DECLINING consumer rewrite provenance for the ones behind it, and pairing decides what to close from `rec.char` — so a forged `char` turned a typed `x` into `x)`. Every field is a scalar or an opaque id, so a shallow copy is complete. The fan-out iterates a snapshot of the consumer list. It was iterating the same array `add_consumer` mutates: a consumer that registered a lower-priority one shifted itself forward under `ipairs` and ran twice, and re-registering made that unbounded. Registrations and removals made during a fan-out now take effect on the next one, stated as a contract and pinned in both directions. `tostring` on the caught error moved inside the containment. A Lua error may be any value, including a table whose `__tostring` throws — rendering it outside the `pcall` reintroduced exactly the escape the containment exists to prevent. Priorities are validated as finite integers in i32 range, matching `pmacs.completion.register`. NaN is a number and every ordered comparison with it is false, so a NaN consumer landed wherever the insertion scan gave up and silently voided the lowest-first ordering that Q#LN22 depends on. `add_consumer` returns a handle and `remove_consumer` unregisters it, reporting whether it was live. Without teardown the chain inherited the `pmacs.hook.add` callback leak COHERENCE.md §13 already records, and spread it to every consumer. Also corrects the rationale the containment was documented with, in the module, the test, and the framing: an uncontained throw does NOT take the fan-out's other subscribers down. `run_all_must_succeed` (src/hook.rs:332) collects errors and continues, so lsp.lua still flushes didChange. The containment is still required — the throw skips every later consumer in the chain — but the reason is narrower than rev 7 claimed. Criteria 46f (record isolation), 46g (snapshot iteration), and 46h (lifecycle and priority validation) added; 46d's rationale corrected. Four new tests, all bite-verified by mutation, each failing only its target: shared record table (1), live-array iteration (1), unprotected tostring (1), bare number check (1), no-op removal (2). The suite also runs green under `--features lua54`. docs/agent-handoff.md said Stage 4a was awaiting approval while this branch had it implemented and in review. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/typed_edit.lua | 113 ++++++++++--- docs/active-work.md | 41 ++++- docs/agent-handoff.md | 24 ++- docs/lean4-mode-framing.md | 42 ++++- tests/typed_edit_chain_acceptance.rs | 232 ++++++++++++++++++++++++++- 5 files changed, 406 insertions(+), 46 deletions(-) diff --git a/builtin/runtime/typed_edit.lua b/builtin/runtime/typed_edit.lua index 59f7366..6baf5f8 100644 --- a/builtin/runtime/typed_edit.lua +++ b/builtin/runtime/typed_edit.lua @@ -13,11 +13,12 @@ -- subscriber that reads the record, and offers that one read to -- consumers registered through `pmacs.typed_edit.add_consumer`: -- --- pmacs.typed_edit.add_consumer { --- name = "auto-pair", -- for error reporting; must be unique-ish +-- local handle = pmacs.typed_edit.add_consumer { +-- name = "auto-pair", -- for error reporting -- priority = 100, -- LOWEST runs FIRST -- fn = function(rec) ... return claimed end, -- } +-- pmacs.typed_edit.remove_consumer(handle) -- -> true if it was live -- -- A consumer returns whether it CLAIMED the edit; the first that claims -- stops the chain. "Claimed" means the chain stops, not that an edit was @@ -46,10 +47,19 @@ pmacs.typed_edit = pmacs.typed_edit or {} -- order" is part of the stated contract, not an incidental property. local consumers = {} --- Register a typed-edit consumer. Argument errors throw: registration --- happens at chunk-load or config-load time, where a throw is a visible --- startup failure rather than a silently missing feature. Nothing in --- the after-edit path throws --- see the fan-out below. +-- Handles are opaque to callers; only identity matters. An integer +-- counter is enough because nothing ever reuses one. +local next_handle = 0 + +-- `math.huge` is the only portable spelling of infinity available in +-- both LuaJIT and 5.4, and NaN is the only value not equal to itself. +local INT32_MIN, INT32_MAX = -2147483648, 2147483647 + +-- Register a typed-edit consumer; returns an opaque handle for +-- `remove_consumer`. Argument errors throw: registration happens at +-- chunk-load or config-load time, where a throw is a visible startup +-- failure rather than a silently missing feature. Nothing in the +-- after-edit path throws --- see the fan-out below. function pmacs.typed_edit.add_consumer(spec) if type(spec) ~= "table" then error("pmacs.typed_edit.add_consumer: spec must be a table", 2) @@ -58,9 +68,18 @@ function pmacs.typed_edit.add_consumer(spec) if type(name) ~= "string" or name == "" then error("pmacs.typed_edit.add_consumer: name must be a non-empty string", 2) end - if type(priority) ~= "number" then + -- A bare `type(priority) == "number"` admits NaN and the infinities, + -- and EVERY ordered comparison against NaN is false --- so a NaN + -- consumer silently lands wherever the insertion scan happens to give + -- up, and the lowest-first contract other consumers depend on stops + -- holding. Bounded integers match `pmacs.completion.register`, whose + -- priority is an i32 on the Rust side. + if type(priority) ~= "number" or priority ~= priority + or priority == math.huge or priority == -math.huge + or priority % 1 ~= 0 + or priority < INT32_MIN or priority > INT32_MAX then error("pmacs.typed_edit.add_consumer: " .. name .. - ": priority must be a number", 2) + ": priority must be a finite integer in [-2147483648, 2147483647]", 2) end if type(fn) ~= "function" then error("pmacs.typed_edit.add_consumer: " .. name .. @@ -77,7 +96,27 @@ function pmacs.typed_edit.add_consumer(spec) break end end - table.insert(consumers, at, { name = name, priority = priority, fn = fn }) + next_handle = next_handle + 1 + local handle = next_handle + table.insert(consumers, at, + { handle = handle, name = name, priority = priority, fn = fn }) + return handle +end + +-- Unregister a consumer by the handle `add_consumer` returned. Returns +-- true if it was registered, false otherwise (so a double-remove is a +-- reportable no-op rather than a throw). Without this, re-evaluating a +-- config or reloading a package accumulates callbacks permanently --- +-- the leak COHERENCE.md §13 already records against `pmacs.hook.add`, +-- which this chain would otherwise inherit and spread. +function pmacs.typed_edit.remove_consumer(handle) + for i, c in ipairs(consumers) do + if c.handle == handle then + table.remove(consumers, i) + return true + end + end + return false end pmacs.hook.add("buffer.after-edit", function() @@ -92,19 +131,51 @@ pmacs.hook.add("buffer.after-edit", function() -- fan-out on nil would leave both reading stale state. local rec = ed.take_typed_edit and ed.take_typed_edit() - for _, c in ipairs(consumers) do - -- `buffer.after-edit` is all-must-succeed (builtin/hooks/default.lua): - -- a throwing consumer would fail the fan-out for every OTHER - -- subscriber, including lsp.lua's didChange flush. Contain it, - -- report it, and keep going --- a broken consumer must not be able - -- to stop the editor from telling the language server what changed. - -- This matches pair.lua's existing never-throw-from-after-edit - -- discipline; it does not weaken the hook's contract for anyone - -- else, because the chain itself still never fails. - local ok, claimed = pcall(c.fn, rec) + -- Iterate a SNAPSHOT. A consumer may register or remove consumers + -- while the chain is running, and `table.insert`/`table.remove` on + -- the live array shifts indices under `ipairs` --- a consumer that + -- registers a lower-priority one shifts itself forward and runs + -- twice, and repeating that is unbounded. Registrations and removals + -- made during a fan-out therefore take effect on the NEXT fan-out. + local snapshot = {} + for i, c in ipairs(consumers) do + snapshot[i] = c + end + + for _, c in ipairs(snapshot) do + -- Each consumer gets its OWN copy of the record. The table handed + -- out is plain Lua data, so a declining consumer could otherwise + -- edit `rec.char` in place and the next consumer would act on the + -- forged value --- auto-pairing reads `rec.char` to decide what to + -- close, so a rewritten `char` makes it insert a pair the user + -- never typed. Every field is a scalar or an opaque id, so a + -- shallow copy is a complete snapshot. + local mine = nil + if rec ~= nil then + mine = {} + for k, v in pairs(rec) do + mine[k] = v + end + end + + -- Contain the consumer. A throw here would skip every LATER + -- consumer in the chain and mark the whole `buffer.after-edit` run + -- failed; the other subscribers still run, because all-must-succeed + -- collects errors and continues (`src/hook.rs`'s + -- `run_all_must_succeed`), but one broken consumer must not be able + -- to silently disable the ones behind it. This matches pair.lua's + -- existing never-throw-from-after-edit discipline. + local ok, claimed = pcall(c.fn, mine) if not ok then - ed.set_status("typed-edit consumer '" .. c.name .. "' failed: " .. - tostring(claimed)) + -- Rendering is itself protected: a Lua error may be any value, + -- including a table whose `__tostring` throws, and an escaping + -- error here would defeat the containment above. + local shown, rendered = pcall(tostring, claimed) + if not shown or type(rendered) ~= "string" then + rendered = "" + end + pcall(ed.set_status, + "typed-edit consumer '" .. c.name .. "' failed: " .. rendered) elseif claimed then return end diff --git a/docs/active-work.md b/docs/active-work.md index bd0c0b1..ba1947a 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -149,9 +149,9 @@ If it does not, stop and repair the remote/fetch configuration. ### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) - Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` - (new, 112 lines), `pair.lua` re-expressed as one consumer, + (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, 9 tests). + `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 @@ -166,9 +166,26 @@ If it does not, stop and repair the remote/fetch configuration. - **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`. `buffer.after-edit` is all-must-succeed, so an - uncontained throw fails the fan-out for every other subscriber - including lsp.lua's didChange flush. + `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: @@ -182,6 +199,11 @@ If it does not, stop and repair the remote/fetch configuration. | 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 @@ -194,9 +216,12 @@ If it does not, stop and repair the remote/fetch configuration. - 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 9/9; M4 121; required GPU 202; **isolated-config - workspace sweep 3,328 across 97 suites, zero failures** with - `grep -c basedpyright` = 0; `git diff --check` clean. + typed-edit chain 13/13 (and 13/13 again under `--no-default-features + --features lua54`, since the fixes touch `math.huge`, `%`, and + `__tostring` behavior that differs between the backends); M4 121; + required GPU 202; **isolated-config workspace sweep 3,332 across 97 + suites, zero failures** with `grep -c basedpyright` = 0; `git diff + --check` clean. - Stage 4b (the input method) is NOT in this PR and not started. ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index a176505..66ccc25 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -88,10 +88,26 @@ 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. - - Remaining: Stage 4a (typed-edit consumer chain) and 4b (the Unicode - input method) are framed and awaiting approval; stages 5 (goal - panel), 6 (`#eval` output channel), and 7 (module hierarchy) are - framed but not scouted against current `main`. + - **Stage 4a (typed-edit consumer chain) is implemented and in review + as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev + 8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the + single `buffer.after-edit` subscriber and the single one-shot read, + `pair.lua` becomes its first registered consumer, and + `tests/auto_pair_acceptance.rs` is unchanged by zero lines + (criterion 46, verified at the diff). No protocol change, no Lean + content. The three decisions that turned out load-bearing rather + than stylistic: consumers are called **even when the record is + nil** (three existing auto-pair tests assert the non-event through + it, and 4b abandons stale pending state on it); each consumer gets + its **own copy** of the record, because pairing reads `rec.char` + and a declining consumer could otherwise forge it; and the fan-out + iterates a **snapshot**, because a consumer that registers a + lower-priority one shifts itself forward under `ipairs` and runs + twice. + - Remaining: Stage 4b (the Unicode input method) is framed and + awaiting approval — not started; stages 5 (goal panel), 6 (`#eval` + output channel), and 7 (module hierarchy) are framed but not + scouted against current `main`. - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 650b2f3..789e419 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1496,7 +1496,7 @@ claim a reader must be able to check without reconstructing | `builtin/runtime/typed_edit.lua` | new — the chain owner | | `builtin/runtime/pair.lua` | re-expressed as one registered consumer | | `src/editor.rs` | one `include_str!` line, before `pair.lua`'s | -| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46e | +| `tests/typed_edit_chain_acceptance.rs` | new — criteria 46a–46h | | `tests/auto_pair_acceptance.rs` | **unchanged, zero lines** | Rev 6 listed only the first three and then required criteria 46a–46e, @@ -2374,7 +2374,7 @@ substrate pin, filed under Stage 4 only because Stage 4 was one stage. Per the no-renumbering rule above, round 5's additions take letter suffixes on both sides of the split. -46a–46e live in a **new `tests/typed_edit_chain_acceptance.rs`**, which +46a–46h live in a **new `tests/typed_edit_chain_acceptance.rs`**, which is part of Stage 4a's declared footprint (Q#LN10) and a required gate for its PR. They cannot live in `tests/auto_pair_acceptance.rs`, which criterion 46 requires to stay byte-identical. @@ -2394,14 +2394,44 @@ criterion 46 requires to stay byte-identical. `include_str!` order happens to agree with intent. 46c. A claiming consumer stops the chain — a later consumer does not run — and a non-claiming one does not. -46d. A consumer that throws is contained: the fan-out still succeeds, - the other consumers still run, and the failure reports through - `set_status`. Bites against the `all-must-succeed` contract taking - the whole fan-out down with one bad consumer (Q#LN10). +46d. A consumer that throws is contained: the later consumers still + run, and the failure reports through `set_status`. Bites against a + chain where one bad consumer silently disables every consumer + behind it. (Round 8 correction: an uncontained throw would *not* + take the fan-out's other subscribers down — `run_all_must_succeed` + in `src/hook.rs` collects errors and continues, so `lsp.lua` still + flushes. Rev 7 claimed otherwise. The containment is still + required; the reason is narrower than stated.) Rendering the error + is itself protected: a Lua error may be any value, including a + table whose `__tostring` throws, and reporting outside the + containment reintroduces the escape it exists to prevent. 46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server test — pairing's closer must be in the buffer before `lsp.lua` flushes `didChange` — still holds with pairing behind the chain. Falsified by moving the chain's registration after `lsp.lua`'s. +46f. **Each consumer's record is its own.** A declining consumer that + mutates the record it was handed cannot change what a later + consumer sees. Bites against handing every consumer the same + mutable table: pairing decides what to close from `rec.char`, so a + forged `char` makes it insert a pair the user never typed. Every + field is a scalar or an opaque id, so a shallow copy is a complete + snapshot. +46g. **The fan-out iterates a snapshot.** A consumer may register or + remove consumers while the chain runs; both take effect on the next + fan-out. Bites against iterating the live array, where a consumer + that registers a lower-priority one shifts itself forward under + `ipairs` and runs twice — unbounded if it re-registers each time. +46h. **The registrar has a lifecycle.** `add_consumer` returns an + opaque handle; `remove_consumer` unregisters it and reports whether + it was live, so a double-remove is a no-op rather than a throw. + Without it, re-evaluating a config or reloading a package + accumulates callbacks permanently — the leak `COHERENCE.md` §13 + already records against `pmacs.hook.add`, which a teardown-less + chain would inherit and spread to every consumer. Priority is + validated as a **finite integer in i32 range**, matching + `pmacs.completion.register`: NaN is a number and every ordered + comparison with it is false, so a bare type check lets it land + wherever the insertion scan gives up and silently voids 46b. **Stage 4b — the Unicode input method** diff --git a/tests/typed_edit_chain_acceptance.rs b/tests/typed_edit_chain_acceptance.rs index c0170f4..8ff9c13 100644 --- a/tests/typed_edit_chain_acceptance.rs +++ b/tests/typed_edit_chain_acceptance.rs @@ -1,11 +1,13 @@ //! Typed-edit consumer chain acceptance (Arc 8 Stage 4a, -//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46e). +//! docs/lean4-mode-framing.md Q#LN10, criteria 46a–46h). //! //! The chain owns the single `buffer.after-edit` subscriber that reads //! the one-shot typed-edit record (Q#AP9) and offers it to consumers in //! priority order. These tests pin the chain's OWN behavior — take-once, -//! priority ordering, claim-stops-chain, throw containment, and the -//! Q#AP7 flush ordering it inherited from `pair.lua`. +//! priority ordering, claim-stops-chain, throw containment, per-consumer +//! record isolation, snapshot iteration under re-entrant registration, +//! the registration lifecycle, and the Q#AP7 flush ordering it inherited +//! from `pair.lua`. //! //! They deliberately do not re-test auto-pairing: criterion 46 requires //! `tests/auto_pair_acceptance.rs` to pass byte-identical, and that @@ -324,9 +326,12 @@ fn a_throwing_consumer_is_contained_reported_and_does_not_stop_the_chain() { "#, ); - // `buffer.after-edit` is all-must-succeed: an uncontained throw - // would fail the fan-out for every other subscriber, including - // lsp.lua's didChange flush. + // An uncontained throw would abandon every LATER consumer in the + // chain and mark the whole `buffer.after-edit` run failed. It would + // NOT stop the hook's other subscribers — all-must-succeed collects + // errors and keeps going (`src/hook.rs`'s `run_all_must_succeed`) — + // so what this pins is that one broken consumer cannot silently + // disable the ones behind it. type_str(&mut s, "("); let later_ran: bool = eval(&s, "return _G.later_ran"); @@ -357,12 +362,43 @@ fn add_consumer_rejects_malformed_registrations() { ), ( "pmacs.typed_edit.add_consumer{ name = \"n\", fn = function() end }", - "priority must be a number", + "priority must be a finite integer", ), ( "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1 }", "fn must be a function", ), + // NaN is a number and every ordered comparison with it is + // false, so a bare type check lets it land wherever the + // insertion scan gives up — and the lowest-first contract the + // Lean expander depends on quietly stops holding. The + // infinities and non-integers go with it: priority matches + // `pmacs.completion.register`'s i32. + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 0/0, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = math.huge, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = -math.huge, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 1.5, \ + fn = function() end }", + "priority must be a finite integer", + ), + ( + "pmacs.typed_edit.add_consumer{ name = \"n\", priority = 4e9, \ + fn = function() end }", + "priority must be a finite integer", + ), ] { let err = s .lua_host @@ -378,6 +414,188 @@ fn add_consumer_rejects_malformed_registrations() { } } +#[test] +fn an_error_whose_rendering_throws_is_still_contained() { + // A Lua error may be any value, including a table whose + // `__tostring` throws. Rendering it outside the containment is a + // second, uncontained throw — the chain would stop at exactly the + // consumer it was trying to report. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.later_ran = false + local hostile = setmetatable({}, { + __tostring = function() error("rendering exploded") end, + }) + pmacs.typed_edit.add_consumer { + name = "boom", priority = 1, fn = function() error(hostile) end, + } + pmacs.typed_edit.add_consumer { + name = "later", priority = 2, + fn = function() _G.later_ran = true; return false end, + } + "#, + ); + + type_str(&mut s, "("); + + let later_ran: bool = eval(&s, "return _G.later_ran"); + assert!( + later_ran, + "an unrenderable error must not escape the containment" + ); + assert_eq!(buffer_text(&s), "()", "and pairing still ran"); + let st = status(&s); + assert!( + st.contains("boom") && st.contains(""), + "the consumer is still named, with a placeholder body, got {st:?}" + ); +} + +// --------------------------------------------------------------------------- +// The record a consumer sees is its own +// --------------------------------------------------------------------------- + +#[test] +fn a_consumers_mutation_of_the_record_cannot_reach_the_next_consumer() { + // The record is plain Lua data. Handing every consumer the same + // table lets a DECLINING consumer rewrite provenance for the ones + // behind it — and pairing decides what to close from `rec.char`, + // so a forged `char` makes it insert a pair the user never typed. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.downstream_char = "unset" + pmacs.typed_edit.add_consumer { + name = "vandal", priority = 1, + fn = function(rec) + if rec then rec.char = "("; rec.codepoint = 40 end + return false + end, + } + pmacs.typed_edit.add_consumer { + name = "witness", priority = 2, + fn = function(rec) + _G.downstream_char = rec and rec.char or "nil" + return false + end, + } + "#, + ); + + type_str(&mut s, "x"); + + let downstream: String = eval(&s, "return _G.downstream_char"); + assert_eq!( + downstream, "x", + "the next consumer sees the real typed character" + ); + assert_eq!( + buffer_text(&s), + "x", + "and pairing, reading the same field, did not close a forged opener" + ); +} + +// --------------------------------------------------------------------------- +// Re-entrant registration, and the consumer lifecycle +// --------------------------------------------------------------------------- + +#[test] +fn registering_or_removing_during_a_fan_out_takes_effect_on_the_next_one() { + // The fan-out iterates a snapshot. Iterating the live array instead + // lets a consumer that registers a LOWER-priority one shift itself + // forward under `ipairs` and run twice in a single fan-out — and + // repeating the registration makes that unbounded. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.order = {} + local function mark(tag) + return function() _G.order[#_G.order + 1] = tag; return false end + end + _G.doomed = pmacs.typed_edit.add_consumer { + name = "doomed", priority = 50, fn = mark("doomed"), + } + _G.did_register = false + pmacs.typed_edit.add_consumer { + name = "a", priority = 10, + fn = function() + _G.order[#_G.order + 1] = "a" + if not _G.did_register then + _G.did_register = true + pmacs.typed_edit.add_consumer { name = "b", priority = 5, fn = mark("b") } + pmacs.typed_edit.remove_consumer(_G.doomed) + end + return false + end, + } + "#, + ); + + type_str(&mut s, "x"); + let first: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + first, "a,doomed", + "`a` runs once even though it registered ahead of itself, and \ + `doomed` still runs in the fan-out it was removed during" + ); + + exec(&s, "_G.order = {}"); + type_str(&mut s, "y"); + let second: String = eval(&s, "return table.concat(_G.order, ',')"); + assert_eq!( + second, "b,a", + "both the registration and the removal land on the next fan-out" + ); +} + +#[test] +fn remove_consumer_unregisters_and_reports_whether_it_was_live() { + // Without removal, re-evaluating a config or reloading a package + // accumulates callbacks permanently — the leak COHERENCE.md §13 + // already records against `pmacs.hook.add`. A chain with no + // teardown would inherit it and spread it to every consumer. + let mut s = editor_with(""); + exec( + &s, + r#" + _G.runs = 0 + _G.h = pmacs.typed_edit.add_consumer { + name = "temporary", priority = 1, + fn = function() _G.runs = _G.runs + 1; return false end, + } + "#, + ); + + type_str(&mut s, "x"); + let runs: i64 = eval(&s, "return _G.runs"); + assert_eq!(runs, 1, "registered consumers run"); + + let first_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)"); + let second_removal: bool = eval(&s, "return pmacs.typed_edit.remove_consumer(_G.h)"); + assert!(first_removal, "removing a live consumer reports true"); + assert!( + !second_removal, + "a double-remove is a reportable no-op, not a throw" + ); + + type_str(&mut s, "y"); + let runs: i64 = eval(&s, "return _G.runs"); + assert_eq!(runs, 1, "the removed consumer no longer runs"); + // Removal is surgical: the chain itself, and pairing on it, survive. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "("); + assert_eq!( + buffer_text(&s), + "xy()", + "the rest of the chain is untouched" + ); +} + // --------------------------------------------------------------------------- // 46e — the Q#AP7 flush ordering the chain inherited // --------------------------------------------------------------------------- From ea9b8c379e97fdfb84e86d37b21a3de8bbb7c1f9 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 13:43:30 -0400 Subject: [PATCH 7/7] docs(lean4): correct Q#LN10's throw-containment rationale MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Q#LN10 still said a throwing consumer "fails the fan-out for everyone." It does not: `run_all_must_succeed` (src/hook.rs:332) collects the error and continues to the hook's remaining subscribers, so `lsp.lua` still flushes didChange. The throw stops every LATER consumer in the chain, which is a narrower consequence and still worth containing — the failure is silent exactly where the abandoned consumers registered. The module comment, criterion 46d, the test, and the ledger were all corrected in the previous commit; Q#LN10 is the decision they descend from, so leaving it stale would have made the disproven claim the authoritative one. Also records the protected-rendering rule there. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- docs/lean4-mode-framing.md | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 789e419..c4a32e5 100644 --- a/docs/lean4-mode-framing.md +++ b/docs/lean4-mode-framing.md @@ -1523,11 +1523,28 @@ sees the exact record via `_capture_records`, and that the Q#AP7 ordering against `lsp.lua`'s `didChange` flush still holds. **What 4a deliberately does not do.** It does not change the `all-must- -succeed` contract, so a consumer that throws still fails the fan-out for -everyone. The chain owner therefore `pcall`s each consumer and reports -through `pmacs.editor.set_status`, matching `pair.lua`'s existing -never-throw-from-after-edit discipline — this is behavior-preserving for -pairing (which already never throws) and is the guardrail 4b needs. +succeed` contract. What that contract actually does on a throw was +stated wrongly through rev 7 and is corrected here, because this +paragraph is the authority the module comment, criterion 46d, the test, +and the ledger all descend from: `run_all_must_succeed` +(`src/hook.rs:332`) **collects** the error and continues to the hook's +remaining subscribers, marking only the run as failed. An uncontained +throw inside the chain therefore does **not** stop `lsp.lua` from +flushing `didChange`. What it does stop is every LATER consumer in the +chain — the chain is one subscriber, and a throw abandons the rest of +its loop. + +That is a narrower consequence than rev 7 claimed and still worth +containing, because the failure is silent in the direction that matters: +a consumer that throws disables the consumers behind it with no signal +at the seam where they were registered. The chain owner therefore +`pcall`s each consumer and reports through `pmacs.editor.set_status`, +matching `pair.lua`'s existing never-throw-from-after-edit discipline — +this is behavior-preserving for pairing (which already never throws) and +is the guardrail 4b needs. The **rendering** of the caught error is +protected the same way: a Lua error may be any value, including a table +whose `__tostring` throws, so `tostring` outside the `pcall` would +reintroduce the escape the containment exists to prevent. ### Q#LN11 — Stage 4b data: vendor the table, generated, attributed