diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua index 4404786..4079de0 100644 --- a/builtin/runtime/lean_input.lua +++ b/builtin/runtime/lean_input.lua @@ -229,7 +229,7 @@ end -- The consumer -- --------------------------------------------------------------------- --- Chain-consumer invocations not yet matched by a `run_deferred`. +-- Chain invocations not yet matched by a `run_deferred`. -- -- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly -- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`, @@ -240,15 +240,29 @@ end -- 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. +-- Counting has to happen INSIDE the chain and BEFORE any consumer that +-- might start a nested fan-out. A subscriber registered alongside +-- `run_deferred` is too late — the whole nested fan-out completes +-- inside the outer chain's subscriber, before either of them runs. And +-- counting in the expander itself is not enough: a lower-priority +-- consumer may CLAIM and stop the chain before the expander is +-- reached, so a nested pass would go uncounted while its +-- `run_deferred` still ran (round 11's fix, round 12's defect). +-- +-- Hence a separate no-op consumer at the minimum priority, which runs +-- first in every chain invocation that reaches any consumer at all. +-- Its guarantee is exactly the ordering contract the chain already +-- rests on, and it degrades safely: the only thing that can skip it is +-- a claim ahead of it, which skips the expander too, so nothing is +-- queued in that fan-out either. local depth = 0 -local function on_typed_edit(rec) +local function count_fan_out() depth = depth + 1 + return false +end + +local function on_typed_edit(rec) local fid = frontend_id() if fid == nil then return false end @@ -426,8 +440,8 @@ 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. + -- keeps this honest if a claim beat the counting consumer, in which + -- case nothing was queued in that fan-out either. local level = depth if depth > 0 then depth = depth - 1 end if level > 1 then return end @@ -487,6 +501,15 @@ pmacs.hook.add("buffer.after-switch", function() if fid ~= nil then pending[fid] = nil end end) +-- Runs first in every chain invocation that reaches a consumer at all, +-- which is what makes the nesting count trustworthy — see `depth`. It +-- declines, always: it observes, it does not participate. +pmacs.typed_edit.add_consumer { + name = "lean-abbrev-fan-out-counter", + priority = -2147483648, + fn = count_fan_out, +} + pmacs.typed_edit.add_consumer { name = "lean-abbrev", priority = 50, diff --git a/docs/active-work.md b/docs/active-work.md index 1a08626..ff1b894 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 11** (rounds 10 and - 11 = review of the implementation). Stage +- Framing `docs/lean4-mode-framing.md` **revision 12** (rounds 10, 11 + and 12 = review of the implementation). Stage 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, the Lean content that registers on it. - Footprint: `scripts/regen-lean-abbrev` (new, the generator), @@ -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, 30 tests), and one + `tests/lean_input_acceptance.rs` (new, 31 tests), and one `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart from the load sites and that one test. @@ -247,6 +247,7 @@ If it does not, stop and repair the remote/fetch configuration. | load lean_input.lua after lsp.lua | 1 | | let a nested fan-out consume the deferred slot | 1 | | stop counting chain invocations | 1 | + | count fan-outs in the expander instead of the sentinel | 1 | Acceptance 45f bit by construction: without a registered window for the source frontend it ran six fan-outs with a nil record and proved @@ -278,6 +279,23 @@ If it does not, stop and repair the remote/fetch configuration. subscriber and the expander's each run exactly once per fan-out, so counting the first and matching it off in the second identifies the nesting level with no new seam in merged Stage 4a substrate. +- **Round 12 found round 11's counter in the wrong place.** It counted + invocations of the EXPANDER, which is optional: a lower-priority + consumer can claim and stop the chain before the expander runs, while + that fan-out's deferred subscriber still runs — so the nested pass + went uncounted, looked outermost, expanded early, and outer pairing + resumed with an invalidated record. The count now comes from a no-op + consumer at the MINIMUM priority, which runs first in every chain + invocation that reaches any consumer, and degrades safely: the only + thing that can skip it is a claim ahead of it, which skips the + expander too. A subscriber registered beside `run_deferred` cannot + serve — the whole nested fan-out completes inside the outer chain's + subscriber, before it would run. +- **Rounds 10–12 share a shape worth naming.** Each fix was correct + about the failure it was shown and wrong about the boundary of the + mechanism it leaned on — first the chain's copy semantics, then its + re-entrancy, then its short-circuit. **A queue that outlives the + thing that filled it has to name that thing, not approximate it.** - Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, named in the module header (Q#LN21): six source-peer optimistic inserts replaced by one daemon-peer op. `set_round_trip_input` would diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index 4f1f467..67e7b43 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -143,7 +143,11 @@ commands, read `docs/active-work.md` immediately after this file. 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: + chain is still mid-list, and the count that recognises this has to + come from a MINIMUM-PRIORITY consumer — the expander is optional + (a claim can stop the chain first) and a subscriber beside the + deferred one is too late (the nested fan-out finishes inside the + outer chain's subscriber). Its other durable facts: the table must stay an ORDERED SEQUENCE (equal-length ties resolve by source declaration order, which a `pairs`-iterated map cannot express); a generator round-trip check must re-read the BYTES ON diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index 3229f35..20c66b4 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: **11**. +Revision 1 — initial. Current revision: **12**. ### Round 1 (rev 1 → rev 2) @@ -587,6 +587,26 @@ One P1 in the round-10 fix, and one stale comment. which round 10 deliberately stopped doing. The behaviour it asserts was correct; only the explanation was stale. +### Round 12 (rev 11 → rev 12) + +One P1: round 11's counter was in the wrong place. + +1. **The nesting count lived in the expander, which is optional.** A + consumer at a lower priority can claim and stop the chain before the + expander runs, while that fan-out's deferred-expansion subscriber + still runs — so the nested pass went uncounted, looked like the + outermost one, expanded early, and outer pairing resumed with an + invalidated record. `\alp(` gave `α(` again. The count now comes + from a no-op consumer at the minimum priority, which runs first in + every chain invocation that reaches any consumer; acceptance 45o + pins the short-circuit path that 45n does not reach. + +The pattern across rounds 10–12 is worth naming: each fix was correct +about the failure it was shown and wrong about the boundary of the +mechanism it relied on — the chain's copy semantics, then its +re-entrancy, then its short-circuit. **A queue that outlives the thing +that filled it needs to name that thing, not approximate it.** + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1815,11 +1835,27 @@ 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. +The nesting level is counted by a **no-op consumer registered at the +minimum priority**, matched off in the expander's subscriber. Only the +outermost pass expands; a nested one leaves the expansion queued. No +new seam in typed_edit.lua, which is merged substrate. + +Where the count lives is the whole difficulty, and two plausible places +are both wrong (round 12): + +- **A subscriber registered beside the expander's is too late.** The + entire nested fan-out completes inside the OUTER chain's subscriber, + before any subscriber registered after it runs. +- **The expander itself is optional.** A lower-priority consumer may + claim and stop the chain before the expander is reached, so a nested + pass would go uncounted while its `run_deferred` still ran — and + would then look like the outermost one. + +A minimum-priority consumer runs first in every chain invocation that +reaches any consumer at all. Its guarantee is exactly the ordering +contract the chain already rests on, and it degrades safely: the only +thing that can skip it is a claim ahead of it, which skips the expander +too, so nothing is queued in that fan-out either. Two guards this exposes, both of which pairing already carries: @@ -2736,6 +2772,14 @@ criterion 46 requires to stay byte-identical. outer chain would then hand pairing a record the replace had invalidated — the round-10 failure again, through the chain's documented re-entrancy seam rather than through claiming. +45o. **A nested fan-out that never reaches the expander must not + expand early either** (round 12). Same shape as 45n, but the nested + pass is short-circuited by a consumer at priority 25 that claims + when the record is nil — so the expander never runs on it. Bites + against counting fan-outs in the expander, which is optional by + construction: the uncounted nested pass looks outermost, expands, + and outer pairing resumes with an invalidated record. 45n passes + against that bug, which is why both are pinned. 45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` — `f<` and `f>` are both length 2, and `f<` is declared first. Same for `\"` + space → `Ä`, first of eleven equal-length candidates. @@ -2890,7 +2934,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from languages other than Lean, and §4's rule is what keeps them out of a Lean PR. -### 9.1 Coherence impact — stages 4a and 4b (rev 11) +### 9.1 Coherence impact — stages 4a and 4b (rev 12) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs index 4cc0613..9b6a3b8 100644 --- a/tests/lean_input_acceptance.rs +++ b/tests/lean_input_acceptance.rs @@ -251,6 +251,65 @@ fn a_nested_fan_out_between_the_expander_and_pairing_does_not_expand_early() { ); } +#[test] +fn a_nested_fan_out_that_never_reaches_the_expander_still_does_not_expand_early() { + // The chain's OTHER exit: a consumer may CLAIM and stop the chain + // before the expander is reached, while the fan-out's + // deferred-expansion subscriber still runs. Counting in the + // expander itself therefore misses that pass — it would look like + // the outermost one and expand early, and outer pairing would + // resume with an invalidated record. + // + // The sequence, exactly: a consumer at 25 declines on the outer + // pass (there is a record) and claims on the nested one (there is + // not); a consumer at 75 runs one nested fan-out from between the + // expander and pairing. + let (mut s, _f) = lean_editor(); + exec( + &s, + r#" + _G.NESTED, _G.CLAIMED = 0, 0 + pmacs.typed_edit.add_consumer { + name = "claims-only-when-recordless", + priority = 25, -- ahead of the expander at 50 + fn = function(rec) + if rec == nil then + _G.CLAIMED = _G.CLAIMED + 1 + return true -- stops the chain: the expander never runs + end + return false + end, + } + 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, claimed): (i64, i64) = eval(&s, "return _G.NESTED, _G.CLAIMED"); + assert_eq!(nested, 1, "the nested fan-out must actually have run"); + assert!( + claimed >= 1, + "the nested pass must actually have been short-circuited before \ + the expander, or this pins the same thing as 45n" + ); + assert_eq!( + text(&s), + "α()", + "the nesting count comes from a point that runs before any \ + consumer can claim, so the nested pass was still recognised" + ); +} + #[test] fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { // The other direction: claiming extensions must not disable pairing