From 0d7ec7e3a6c1384e6d95b68456c8290add4e92fc Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 17:00:58 -0400 Subject: [PATCH] fix(lean4): tie the deferred expansion to the fan-out that queued it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `buffer.after-edit` fan-outs NEST — the typed-edit contract supports a consumer calling `pmacs.hook.run`, and typed_edit.lua's header says so in its second paragraph. A nested run re-enters every subscriber, including the deferred expansion's, while the OUTER chain is still walking its consumer list and pairing has not yet seen the terminator. So a consumer registered at priority 75 — between the expander at 50 and pairing at 100 — that runs one nested fan-out made `\alp(` yield `α(` again: the nested pass consumed the queued expansion and edited, and outer pairing then resumed holding a record the replace had invalidated. That is round 10's failure reached through the chain's documented re-entrancy seam rather than through claiming, which is why deferring alone did not close it. Deferring work past a fan-out means owning WHICH fan-out it belongs to. The chain's subscriber and this module's each run exactly once per fan-out, in that order, so counting invocations of the first and matching them off in the second identifies the nesting level. Only the outermost pass expands; a nested one leaves the expansion queued. No new seam in typed_edit.lua, which is merged Stage 4a substrate. Both halves bite: removing the level check and never counting invocations each fail the new acceptance 45n. Also fixes a test comment that still described the span design round 10 discarded — it claimed the expansion replaces the span "INCLUDING the terminator". The behaviour asserted was right; the explanation was stale. Framing rev 11. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/lean_input.lua | 28 ++++++++++++++++++++ docs/active-work.md | 19 +++++++++++--- docs/agent-handoff.md | 6 ++++- docs/lean4-mode-framing.md | 48 ++++++++++++++++++++++++++++++++-- tests/lean_input_acceptance.rs | 44 ++++++++++++++++++++++++++++++- 5 files changed, 138 insertions(+), 7 deletions(-) diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua index 7b205d2..4404786 100644 --- a/builtin/runtime/lean_input.lua +++ b/builtin/runtime/lean_input.lua @@ -229,7 +229,26 @@ end -- The consumer -- --------------------------------------------------------------------- +-- Chain-consumer invocations not yet matched by a `run_deferred`. +-- +-- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly +-- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`, +-- and a nested run re-enters every subscriber — including this module's +-- deferred-expansion subscriber, while the OUTER chain is still walking +-- its consumer list and pairing has not yet seen the terminator. A +-- nested run that performed the expansion would reproduce exactly the +-- bug deferring exists to fix: pairing resumes afterwards holding a +-- record the replace has invalidated, declines, and the closer is lost. +-- +-- The chain's subscriber and this module's subscriber run exactly once +-- each per fan-out, in that order, so counting invocations of the first +-- and matching them off in the second identifies the nesting level +-- without any new seam in typed_edit.lua. Only the outermost pass +-- performs the expansion; a nested one leaves it queued. +local depth = 0 + local function on_typed_edit(rec) + depth = depth + 1 local fid = frontend_id() if fid == nil then return false end @@ -404,6 +423,15 @@ end -- A claim by ANY chain consumer stops the chain but not this — which -- is the point. Pairing claims the terminator it reacts to. local function run_deferred() + -- Match off this fan-out's chain invocation. `> 1` means the outer + -- chain is still mid-list — pairing has not had the terminator yet — + -- so the queued expansion stays queued for the outer pass. The clamp + -- keeps this honest if a lower-priority consumer claimed before the + -- chain reached ours, in which case there is nothing queued anyway. + local level = depth + if depth > 0 then depth = depth - 1 end + if level > 1 then return end + local fid = frontend_id() if fid == nil then return end local d = deferred[fid] diff --git a/docs/active-work.md b/docs/active-work.md index f931da1..1a08626 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -175,8 +175,8 @@ If it does not, stop and repair the remote/fetch configuration. ### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`) -- Framing `docs/lean4-mode-framing.md` **revision 10** (round 10 = - review of the implementation). Stage +- Framing `docs/lean4-mode-framing.md` **revision 11** (rounds 10 and + 11 = review of the implementation). Stage 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, the Lean content that registers on it. - Footprint: `scripts/regen-lean-abbrev` (new, the generator), @@ -184,7 +184,7 @@ If it does not, stop and repair the remote/fetch configuration. from `leanprover/vscode-lean4@17d1d08`, Apache-2.0), `builtin/runtime/lean_input.lua` (new, the consumer at priority 50), `src/editor.rs` (two `include_str!` blocks), - `tests/lean_input_acceptance.rs` (new, 29 tests), and one + `tests/lean_input_acceptance.rs` (new, 30 tests), and one `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart from the load sites and that one test. @@ -245,6 +245,8 @@ If it does not, stop and repair the remote/fetch configuration. | drop the `cursor() == post_cursor` check | 1 | | place the point without the context guard | 1 | | load lean_input.lua after lsp.lua | 1 | + | let a nested fan-out consume the deferred slot | 1 | + | stop counting chain invocations | 1 | Acceptance 45f bit by construction: without a registered window for the source frontend it ran six fan-outs with a nil record and proved @@ -265,6 +267,17 @@ If it does not, stop and repair the remote/fetch configuration. relevance check needs `cursor() == post_cursor`, as pairing's has since #110), and cursor placement could move a buffer an intercept had switched to. +- **Round 11 found the round-10 fix incomplete in one place: + `buffer.after-edit` fan-outs NEST.** A consumer between the expander + (50) and pairing (100) that calls `pmacs.hook.run("buffer.after-edit")` + re-enters the expander's subscriber while the OUTER chain is still + mid-list; the nested pass expanded and outer pairing then resumed with + an invalidated record — `α(` again, through the chain's documented + re-entrancy seam instead of through claiming. **Deferring work past a + fan-out means owning which fan-out it belongs to.** The chain's + subscriber and the expander's each run exactly once per fan-out, so + counting the first and matching it off in the second identifies the + nesting level with no new seam in merged Stage 4a substrate. - Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, named in the module header (Q#LN21): six source-peer optimistic inserts replaced by one daemon-peer op. `set_round_trip_input` would diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index d1dc46b..4f1f467 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -139,7 +139,11 @@ commands, read `docs/active-work.md` immediately after this file. be used. The expansion therefore runs on a SECOND `buffer.after-edit` subscriber after the chain — which is how a pair character that terminates an abbreviation still pairs - (`\alp(` → `α()`). Its other durable facts: + (`\alp(` → `α()`). And **deferring work past a fan-out means + owning which fan-out it belongs to**: these fan-outs NEST, so a + consumer between the expander and pairing that calls + `pmacs.hook.run` re-enters the deferred subscriber while the outer + chain is still mid-list. Its other durable facts: the table must stay an ORDERED SEQUENCE (equal-length ties resolve by source declaration order, which a `pairs`-iterated map cannot express); a generator round-trip check must re-read the BYTES ON diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 482ad84..3229f35 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: **10**. +Revision 1 — initial. Current revision: **11**. ### Round 1 (rev 1 → rev 2) @@ -567,6 +567,26 @@ Acceptance 45m was added with them: the expansion now runs on its own `buffer.after-edit` subscriber, which is a new instance of Q#AP7 and was unpinned. +### Round 11 (rev 10 → rev 11) + +One P1 in the round-10 fix, and one stale comment. + +1. **The deferred expansion was not tied to the fan-out that queued + it.** `buffer.after-edit` fan-outs nest — the typed-edit contract + supports a consumer calling `pmacs.hook.run` — and a nested run + re-enters the expander's subscriber while the OUTER chain is still + mid-list. A consumer at priority 75 running one nested fan-out made + `\alp(` yield `α(` again: the nested pass expanded, and outer + pairing then resumed with a record the replace had invalidated. + Round 10's own failure mode, reached through re-entrancy instead of + claiming. Q#LN22 now specifies matching chain invocations against + expander invocations so only the outermost pass expands; acceptance + 45n pins it. +2. **A test comment still described the discarded span design** — it + said the expansion replaces the span "INCLUDING the terminator", + which round 10 deliberately stopped doing. The behaviour it asserts + was correct; only the explanation was stale. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1785,6 +1805,22 @@ and the typed text only; whatever pairing did lands after it and survives untouched. One undo restores the same text either way, because the terminator was always its own insert. +**The deferred expansion must belong to its own fan-out** (round 11). +`buffer.after-edit` fan-outs NEST — Q#AP9 and typed_edit.lua's header +both say so explicitly, and a consumer may call `pmacs.hook.run`. A +nested run re-enters every subscriber, including the deferred +expansion's, while the OUTER chain is still walking its consumer list +and pairing has not yet seen the terminator. A nested pass that +performed the expansion would reproduce the exact bug deferring exists +to fix, reached through the chain's documented re-entrancy seam instead +of through claiming. + +The chain's subscriber and the expander's subscriber each run exactly +once per fan-out, in that order, so counting invocations of the first +and matching them off in the second identifies the nesting level — no +new seam in typed_edit.lua, which is merged substrate. Only the +outermost pass expands; a nested one leaves the expansion queued. + Two guards this exposes, both of which pairing already carries: - The relevance check is **three-part**, not two: buffer, window, **and @@ -2692,6 +2728,14 @@ criterion 46 requires to stay byte-identical. unexpanded text. Pinned with the `sighelp` fake server and `(` as the trigger — the flush carrying the terminator carries `α()`. Falsified by loading lean_input.lua after lsp.lua. +45n. **A nested fan-out must not expand early** (round 11). A consumer + registered BETWEEN the expander and pairing that calls + `pmacs.hook.run("buffer.after-edit")` once still yields `α()` for + `\alp(`. Bites against a deferred slot consumed by whichever + fan-out happens to reach it: the nested pass would expand, and the + outer chain would then hand pairing a record the replace had + invalidated — the round-10 failure again, through the chain's + documented re-entrancy seam rather than through claiming. 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. @@ -2846,7 +2890,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 10) +### 9.1 Coherence impact — stages 4a and 4b (rev 11) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs index 9270f1b..4cc0613 100644 --- a/tests/lean_input_acceptance.rs +++ b/tests/lean_input_acceptance.rs @@ -98,7 +98,10 @@ fn lean_editor() -> (EditorState, PathBuf) { fn the_finish_path_retains_the_terminator_in_one_undo_step() { // `alp` is not a key; `alpha` is the shortest key extending it. The // space does not extend anything, so it lands first and the - // expansion replaces the whole span INCLUDING the terminator. + // expansion replaces the leader and the typed text — the span stops + // BEFORE the terminator, so whatever auto-pairing did with it + // survives. One undo restores the same text either way, because the + // terminator was its own insert to begin with. let (mut s, _f) = lean_editor(); type_str(&mut s, "\\alp "); assert_eq!(text(&s), "α ", "terminator retained, not consumed"); @@ -209,6 +212,45 @@ fn a_pair_character_that_terminates_an_abbreviation_still_pairs() { ); } +#[test] +fn a_nested_fan_out_between_the_expander_and_pairing_does_not_expand_early() { + // `buffer.after-edit` fan-outs NEST — the typed-edit contract + // explicitly supports a consumer calling `pmacs.hook.run`, and a + // nested run re-enters every subscriber, including the deferred + // expansion's. If the nested pass performed the expansion, the + // OUTER chain would then resume and hand pairing a record the + // replace had already invalidated: `α(` again, reached through the + // chain's documented re-entrancy seam rather than through claiming. + let (mut s, _f) = lean_editor(); + exec( + &s, + r#" + _G.NESTED = 0 + pmacs.typed_edit.add_consumer { + name = "nested-fan-out", + priority = 75, -- between the expander (50) and pairing (100) + fn = function() + if _G.NESTED == 0 then + _G.NESTED = 1 + pmacs.hook.run("buffer.after-edit") + end + return false + end, + } + "#, + ); + + type_str(&mut s, "\\alp("); + let nested: i64 = eval(&s, "return _G.NESTED"); + assert_eq!(nested, 1, "the nested fan-out must actually have run"); + assert_eq!( + text(&s), + "α()", + "the expansion waited for the OUTERMOST pass, so pairing still \ + held a valid record when the terminator reached it" + ); +} + #[test] fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { // The other direction: claiming extensions must not disable pairing