From a53965474d245d29d9454ec420d199216c2a6cd3 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 16:24:06 -0400 Subject: [PATCH 1/4] feat(lean4): the Unicode input method (Arc 8 Stage 4b) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Typing `\alpha` in a Lean 4 buffer gives `α`; `\<>` gives `⟨⟩` with the point between them. The abbreviation table is vendored from vscode-lean4 and the expander is a typed-edit consumer registered on the Stage 4a chain at priority 50, ahead of auto-pairing. The ordering is load-bearing. 64 abbreviation keys contain a character in the `lean4` pair set, so with pairing first, typing `\[` would insert `[]` and corrupt the pending key to `\[]` before the second `[` arrives — `\[[]]` becomes unreachable. The consumer therefore claims every keystroke that EXTENDS a pending abbreviation, not only one that completes an expansion; claiming only completions would hand each intermediate `[` to pairing by a different route. The vendored table is an ORDERED SEQUENCE, not a map. Upstream breaks equal-length ties by source declaration order — 101 prefixes depend on it, and `\f` resolves through `f<` rather than `f>` — which a `pairs`-iterated Lua table cannot express. `scripts/regen-lean-abbrev` takes a vscode-lean4 commit, emits the file with its provenance header, and aborts on a duplicate key, invalid UTF-8, or a round-trip mismatch. Undo is cross-peer-degraded on CRDT frontends and that is accepted and named, not papered over (Q#LN21): `\alpha` arrives as six source-peer optimistic inserts while the expansion is one daemon-peer replace. `set_round_trip_input` would fix it and also makes `dispatch_idle` report false, so RET would stop inserting a newline. Round 9 corrects three approved acceptance criteria that the real table contradicts, found by simulating the state machine over all 1,855 entries and re-reading upstream at the pinned commit rather than re-reading the prose. `\to` is not eager — `top`, `to0` and `toa` extend it. `\zzzz` expands to `ζzzz ` because `ze`, `zeta` and `zsqrtd` exist; only `$ % , ; @ W` open no key at all. And `\alpha`'s undo does not restore `\alpha ` because `alpha` IS eager, so the terminator is a separate edit. Criteria 38, 41 and 42 now state both paths, and the false halves are asserted too: they read as correct until the table is consulted. Three implementation traps worth the record. The generator's own round-trip check was broken twice and failed closed both times: `str.splitlines()` splits on U+2028, which 53 symbols contain, and escaping through `chr(byte)` produced a latin-1-shaped string that the UTF-8 write re-encoded. The first check compared in-memory strings and agreed with itself; it now stages the file, re-reads the bytes from disk, and renames into place only on a match. And the expansion SHRINKS the buffer, so the point must be placed explicitly — pairing's no-cursor-motion rule holds only for an insert AT the cursor, and without this every self-insert after the first expansion is silently rejected and the editor looks dead. 25 acceptance tests plus one `--lib` test for the optimistic CRDT producer (45f), which is where the gate list's `--features crdt` run reaches it; a crdt-gated integration test would be dark in CI and in the gates both. Fifteen mutations bite, each failing its target. Three of these tests were vacuous when first written and biting is what found them: the abandonment test asserted text a surviving record would also produce, the re-arm test used an example that never reaches the re-arm branch, and both switch tests ran through `find_or_open`'s fresh-load path rather than `buffer.after-switch`. No protocol change (Q#LN14). Also reconciles the handoff and ledger for Stage 4a (#179) and adds `lean.abbrev` to COHERENCE.md's config-registry adoption census, now nine settings. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- COHERENCE.md | 9 +- builtin/runtime/lean_abbrev.lua | 1883 +++++++++++++++++++++++++++++++ builtin/runtime/lean_input.lua | 362 ++++++ docs/active-work.md | 235 ++-- docs/agent-handoff.md | 46 +- docs/lean4-mode-framing.md | 76 +- scripts/regen-lean-abbrev | 254 +++++ src/daemon.rs | 137 +++ src/editor.rs | 21 + tests/lean_input_acceptance.rs | 678 +++++++++++ 10 files changed, 3521 insertions(+), 180 deletions(-) create mode 100644 builtin/runtime/lean_abbrev.lua create mode 100644 builtin/runtime/lean_input.lua create mode 100755 scripts/regen-lean-abbrev create mode 100644 tests/lean_input_acceptance.rs diff --git a/COHERENCE.md b/COHERENCE.md index 4e7361c..f172a21 100644 --- a/COHERENCE.md +++ b/COHERENCE.md @@ -1022,12 +1022,15 @@ layering, provenance, and adoption have not followed.** `ConfigValue`s; `describe-setting`'s "Source:" names where `define()` ran. The inspection view sketched above is currently impossible to render. -- **Adoption is eight settings**: `editing.auto-pair` (pair.lua), +- **Adoption is nine settings**: `editing.auto-pair` (pair.lua), `editing.trim-on-save` (editops.lua), `autosave.interval-ms` (autosave.lua), `window.panel-height` + `window.min-height` - (window.lua), and `terminal.default-profile` + + (window.lua), `terminal.default-profile` + `terminal.scrollback-rows` + `terminal.escape-key` (terminal.lua, - #173). Everything else a user might set — theme, fonts, LSP + #173), and `lean.abbrev` (lean_input.lua, Arc 8 Stage 4b) — a + `live` boolean read against the typed edit's SOURCE buffer, the + `editing.auto-pair` shape including its correction to resolve + `rec.buffer` rather than the active buffer. Everything else a user might set — theme, fonts, LSP server config, killring size, recentf/saveplace/desktop enables, pair sets, comment strings, `pmacs.parse.*` — lives in raw Lua outside the registry and is therefore invisible to `describe-setting` diff --git a/builtin/runtime/lean_abbrev.lua b/builtin/runtime/lean_abbrev.lua new file mode 100644 index 0000000..769c9d4 --- /dev/null +++ b/builtin/runtime/lean_abbrev.lua @@ -0,0 +1,1883 @@ +-- lean_abbrev.lua --- VENDORED DATA. Do not edit by hand. +-- +-- The Lean 4 abbreviation table, generated from: +-- +-- repo: https://github.com/leanprover/vscode-lean4 +-- path: lean4-unicode-input/src/abbreviations.json +-- commit: 17d1d08 +-- license: Apache-2.0 +-- entries: 1855 (26 carry $CURSOR) +-- source: 36861 bytes +-- +-- Regenerate with: +-- +-- scripts/regen-lean-abbrev 17d1d08 +-- +-- An ORDERED SEQUENCE, not a map: upstream resolves equal-length ties +-- by source declaration order (101 prefixes depend on it), and a +-- `pairs`-iterated Lua map cannot express that. The file's own line +-- order is the audit trail. Consumers must not reorder it. +-- +-- Not fetched at runtime and not a package dependency: the input method +-- has to work offline and on first launch. Upkeep is a documented +-- manual process — see docs/lean4-mode-framing.md Q#LN11. + +pmacs = pmacs or {} + +pmacs.lean_abbrev = { + { "{}", "{$CURSOR}" }, + { "{}_", "{$CURSOR}_" }, + { "{{}}", "⦃$CURSOR⦄" }, + { "[]", "[$CURSOR]" }, + { "[]_", "[$CURSOR]_" }, + { "[[]]", "⟦$CURSOR⟧" }, + { "<>", "⟨$CURSOR⟩" }, + { "()", "($CURSOR)" }, + { "()_", "($CURSOR)_" }, + { "^()", "⁽$CURSOR⁾" }, + { "_()", "₍$CURSOR₎" }, + { "([])'", "⟮$CURSOR⟯" }, + { "(())", "⸨$CURSOR⸩" }, + { "f<>", "‹$CURSOR›" }, + { "f<<>>", "«$CURSOR»" }, + { "h<>", "❰$CURSOR❱" }, + { "[--]", "⁅$CURSOR⁆" }, + { "||||", "‖$CURSOR‖" }, + { "nnnorm", "‖$CURSOR‖₊" }, + { "norm", "‖$CURSOR‖" }, + { "floor", "⌊$CURSOR⌋" }, + { "ceil", "⌈$CURSOR⌉" }, + { "nfloor", "⌊$CURSOR⌋₊" }, + { "nceil", "⌈$CURSOR⌉₊" }, + { "s[]", "⦋$CURSOR⦌" }, + { "simplex", "⦋$CURSOR⦌" }, + { "\\", "\\" }, + { "a", "α" }, + { "b", "β" }, + { "c", "χ" }, + { "d", "↓" }, + { "e", "ε" }, + { "g", "γ" }, + { "i", "∩" }, + { "m", "μ" }, + { "n", "\\n" }, + { "o", "∘" }, + { "p", "Π" }, + { "t", "▸" }, + { "r", "→" }, + { "u", "↑" }, + { "v", "∨" }, + { "x", "×" }, + { "-", "⁻¹" }, + { "~", "∼" }, + { ".", "·" }, + { "*", "⋆" }, + { "!", "¬" }, + { "?", "¿" }, + { "1", "₁" }, + { "2", "₂" }, + { "3", "₃" }, + { "4", "₄" }, + { "5", "₅" }, + { "6", "₆" }, + { "7", "₇" }, + { "8", "₈" }, + { "9", "₉" }, + { "0", "₀" }, + { "l", "←" }, + { "<", "⟨" }, + { ">", "⟩" }, + { "O", "Ø" }, + { "&", "⅋" }, + { "A", "𝔸" }, + { "C", "ℂ" }, + { "D", "Δ" }, + { "F", "𝔽" }, + { "G", "Γ" }, + { "H", "ℍ" }, + { "I", "⋂" }, + { "I0", "⋂₀" }, + { "K", "𝕂" }, + { "L", "Λ" }, + { "N", "ℕ" }, + { "P", "Π" }, + { "Q", "ℚ" }, + { "R", "ℝ" }, + { "S", "Σ" }, + { "U", "⋃" }, + { "U0", "⋃₀" }, + { "Z", "ℤ" }, + { "#", "♯" }, + { ":", "∶" }, + { "|", "∣" }, + { "rw", "▸" }, + { "coe", "↑" }, + { "be", "β" }, + { "ga", "γ" }, + { "de", "δ" }, + { "ep", "ε" }, + { "ze", "ζ" }, + { "et", "η" }, + { "th", "θ" }, + { "io", "ι" }, + { "ka", "κ" }, + { "la", "λ" }, + { "mu", "μ" }, + { "nu", "ν" }, + { "xi", "ξ" }, + { "pi", "π" }, + { "rh", "ρ" }, + { "vsi", "ς" }, + { "si", "σ" }, + { "ta", "τ" }, + { "ph", "φ" }, + { "ch", "χ" }, + { "ps", "ψ" }, + { "om", "ω" }, + { "`A", "À" }, + { "'A", "Á" }, + { "^{A}", "Â" }, + { "~A", "Ã" }, + { "\"A", "Ä" }, + { "-{A}", "Ā" }, + { "cC", "Ç" }, + { "`E", "È" }, + { "'E", "É" }, + { "^{E}", "Ê" }, + { "\"E", "Ë" }, + { "-{E}", "Ē" }, + { "`I", "Ì" }, + { "'I", "Í" }, + { "^{I}", "Î" }, + { "\"I", "Ï" }, + { "-{I}", "Ī" }, + { "~N", "Ñ" }, + { "`O", "Ò" }, + { "'O", "Ó" }, + { "^{O}", "Ô" }, + { "~O", "Õ" }, + { "\"O", "Ö" }, + { "/O", "Ø" }, + { "-{O}", "Ō" }, + { "`U", "Ù" }, + { "'U", "Ú" }, + { "^{U}", "Û" }, + { "\"U", "Ü" }, + { "-{U}", "Ū" }, + { "'Y", "Ý" }, + { "`a", "à" }, + { "'a", "á" }, + { "^{a}", "â" }, + { "~a", "ã" }, + { "\"a", "ä" }, + { "-{a}", "ā" }, + { "cc", "ç" }, + { "`e", "è" }, + { "'e", "é" }, + { "^{e}", "ê" }, + { "\"e", "ë" }, + { "-{e}", "ē" }, + { "`i", "ì" }, + { "'i", "í" }, + { "^{i}", "î" }, + { "\"i", "ï" }, + { "-{i}", "ī" }, + { "~{n}", "ñ" }, + { "`o", "ò" }, + { "'o", "ó" }, + { "^{o}", "ô" }, + { "~o", "õ" }, + { "\"o", "ö" }, + { "/o", "ø" }, + { "-{o}", "ō" }, + { "`u", "ù" }, + { "'u", "ú" }, + { "^{u}", "û" }, + { "\"u", "ü" }, + { "-{u}", "ū" }, + { "'y", "ý" }, + { "\"y", "ÿ" }, + { "/L", "Ł" }, + { "note", "♩" }, + { "not", "¬" }, + { "notin", "∉" }, + { "notlt", "≮" }, + { "nomisma", "𐆎" }, + { "nin", "∉" }, + { "nni", "∌" }, + { "ni", "∋" }, + { "nattrans", "⟹" }, + { "nat_trans", "⟹" }, + { "natural", "♮" }, + { "nat", "ℕ" }, + { "naira", "₦" }, + { "nabla", "∇" }, + { "napprox", "≉" }, + { "numero", "№" }, + { "nLeftarrow", "⇍" }, + { "nLeftrightarrow", "⇎" }, + { "nRightarrow", "⇏" }, + { "nVDash", "⊯" }, + { "nVdash", "⊮" }, + { "ncong", "≇" }, + { "nearrow", "↗" }, + { "neg", "¬" }, + { "nequiv", "≢" }, + { "neq", "≠" }, + { "nexists", "∄" }, + { "ne", "≠" }, + { "ngeqq", "≱" }, + { "ngeqslant", "≱" }, + { "ngeq", "≱" }, + { "ngtr", "≯" }, + { "nleftarrow", "↚" }, + { "nleftrightarrow", "↮" }, + { "nleqq", "≰" }, + { "nleqslant", "≰" }, + { "nleq", "≰" }, + { "nless", "≮" }, + { "nmid", "∤" }, + { "nparallel", "∦" }, + { "npreceq", "⋠" }, + { "nprec", "⊀" }, + { "nrightarrow", "↛" }, + { "nshortmid", "∤" }, + { "nsimeq", "≄" }, + { "nsim", "≁" }, + { "nsubseteqq", "⊈" }, + { "nsubseteq", "⊈" }, + { "nsubset", "⊄" }, + { "nsucceq", "⋡" }, + { "nsucc", "⊁" }, + { "nsupseteqq", "⊉" }, + { "nsupseteq", "⊉" }, + { "nsupset", "⊅" }, + { "ntrianglelefteq", "⋬" }, + { "ntriangleleft", "⋪" }, + { "ntrianglerighteq", "⋭" }, + { "ntriangleright", "⋫" }, + { "nvDash", "⊭" }, + { "nvdash", "⊬" }, + { "nwarrow", "↖" }, + { "eqn", "≠" }, + { "equiv", "≃" }, + { "eqcirc", "≖" }, + { "eqcolon", "≕" }, + { "eqslantgtr", "⋝" }, + { "eqslantless", "⋜" }, + { "entails", "⊢" }, + { "en", "–" }, + { "exn", "∄" }, + { "exists", "∃" }, + { "ex", "∃" }, + { "emptyset", "∅" }, + { "empty", "∅" }, + { "em", "—" }, + { "epsilon", "ε" }, + { "eps", "ε" }, + { "euro", "€" }, + { "eta", "η" }, + { "ell", "ℓ" }, + { "iso", "≅" }, + { "in", "∈" }, + { "inn", "∉" }, + { "inter", "∩" }, + { "intercal", "⊺" }, + { "intersection", "∩" }, + { "integral", "∫" }, + { "integral-", "⨍" }, + { "int", "ℤ" }, + { "inv", "⁻¹" }, + { "increment", "∆" }, + { "inf", "⊓" }, + { "infi", "⨅" }, + { "infty", "∞" }, + { "iff", "↔" }, + { "imp", "→" }, + { "imath", "ı" }, + { "iota", "ι" }, + { "=n", "≠" }, + { "==n", "≢" }, + { "===", "≣" }, + { "==>", "⟹" }, + { "==", "≡" }, + { "=:", "≕" }, + { "=o", "≗" }, + { "=>n", "⇏" }, + { "=>", "⇒" }, + { "~n", "≁" }, + { "~~n", "≉" }, + { "~~~", "≋" }, + { "~~-", "≊" }, + { "~~", "≈" }, + { "~-n", "≄" }, + { "~-", "≃" }, + { "~=n", "≇" }, + { "~=", "≅" }, + { "homotopy", "∼" }, + { "hom", "⟶" }, + { "hori", "ϩ" }, + { "hookleftarrow", "↩" }, + { "hookrightarrow", "↪" }, + { "hryvnia", "₴" }, + { "heta", "ͱ" }, + { "heartsuit", "♥" }, + { "hbar", "ℏ" }, + { ":~", "∻" }, + { ":=", "≔" }, + { "::-", "∺" }, + { "::", "∷" }, + { "-~", "≂" }, + { "-|", "⊣" }, + { "-1", "⁻¹" }, + { "^-1", "⁻¹" }, + { "-2", "⁻²" }, + { "-3", "⁻³" }, + { "-:", "∹" }, + { "->n", "↛" }, + { "->", "→" }, + { "-->", "⟶" }, + { "---", "─" }, + { "--=", "═" }, + { "--_", "━" }, + { "--.", "╌" }, + { "-o", "⊸" }, + { ".=.", "≑" }, + { ".=", "≐" }, + { ".+", "∔" }, + { ".-", "∸" }, + { "...", "⋯" }, + { "(=", "≘" }, + { "(b", "⟅" }, + { "and=", "≙" }, + { "and", "∧" }, + { "an", "∧" }, + { "angle", "∠" }, + { "rightangle", "∟" }, + { "angstrom", "Å" }, + { "all", "∀" }, + { "allf", "∀ᶠ" }, + { "all^f", "∀ᶠ" }, + { "allm", "∀ᵐ" }, + { "all^m", "∀ᵐ" }, + { "alpha", "α" }, + { "aleph", "ℵ" }, + { "aleph0", "ℵ₀" }, + { "asterisk", "⁎" }, + { "ast", "∗" }, + { "asymp", "≍" }, + { "apl", "⌶" }, + { "approxeq", "≊" }, + { "approx", "≈" }, + { "aa", "å" }, + { "ae", "æ" }, + { "austral", "₳" }, + { "amalg", "∐" }, + { "average", "⨍" }, + { "-int", "⨍" }, + { "or=", "≚" }, + { "ordfeminine", "ª" }, + { "ordmasculine", "º" }, + { "or", "∨" }, + { "oplus", "⊕" }, + { "od", "ᵒᵈ" }, + { "orderdual", "ᵒᵈ" }, + { "addopposite", "ᵃᵒᵖ" }, + { "aop", "ᵃᵒᵖ" }, + { "mulopposite", "ᵐᵒᵖ" }, + { "mop", "ᵐᵒᵖ" }, + { "opposite", "ᵒᵖ" }, + { "op", "ᵒᵖ" }, + { "o+", "⊕" }, + { "o--", "⊖" }, + { "o-", "⊝" }, + { "ox", "⊗" }, + { "o/", "⊘" }, + { "o.", "⊙" }, + { "oo", "⊚" }, + { "o*", "∘*" }, + { "o=", "⊜" }, + { "oe", "œ" }, + { "octagonal", "🛑" }, + { "ohm", "Ω" }, + { "ounce", "℥" }, + { "omega", "ω" }, + { "omicron", "ο" }, + { "ominus", "⊖" }, + { "odot", "⊙" }, + { "oint", "∮" }, + { "oiint", "∯" }, + { "oslash", "⊘" }, + { "otimes", "⊗" }, + { "tensorproduct", "⊗" }, + { "pitensorproduct", "⨂" }, + { "tensorpower", "⨂" }, + { "pd", "∂" }, + { "*=", "≛" }, + { "t=", "≜" }, + { "tint", "∯" }, + { "transport", "▹" }, + { "trans", "▹" }, + { "triangledown", "▿" }, + { "trianglelefteq", "⊴" }, + { "triangleleft", "◃" }, + { "triangleq", "≜" }, + { "trianglerighteq", "⊵" }, + { "triangleright", "▹" }, + { "triangle", "▵" }, + { "tr", "⬝" }, + { "tb", "◂" }, + { "twoheadleftarrow", "↞" }, + { "twoheadrightarrow", "↠" }, + { "tw", "◃" }, + { "tie", "⁀" }, + { "times", "×" }, + { "theta", "θ" }, + { "therefore", "∴" }, + { "thickapprox", "≈" }, + { "thicksim", "∼" }, + { "telephone", "℡" }, + { "tenge", "₸" }, + { "textmusicalnote", "♪" }, + { "textmu", "µ" }, + { "textfractionsolidus", "⁄" }, + { "textbaht", "฿" }, + { "textdied", "✝" }, + { "textdiscount", "⁒" }, + { "textcolonmonetary", "₡" }, + { "textcircledP", "℗" }, + { "textwon", "₩" }, + { "textnaira", "₦" }, + { "textnumero", "№" }, + { "textpeso", "₱" }, + { "textpertenthousand", "‱" }, + { "textlira", "₤" }, + { "textlquill", "⁅" }, + { "textrecipe", "℞" }, + { "textreferencemark", "※" }, + { "textrquill", "⁆" }, + { "textinterrobang", "‽" }, + { "textestimated", "℮" }, + { "textopenbullet", "◦" }, + { "tugrik", "₮" }, + { "tau", "τ" }, + { "top", "⊤" }, + { "to", "→" }, + { "to0", "→₀" }, + { "r0", "→₀" }, + { "to_0", "→₀" }, + { "r_0", "→₀" }, + { "finsupp", "→₀" }, + { "to1", "→₁" }, + { "r1", "→₁" }, + { "to_1", "→₁" }, + { "r_1", "→₁" }, + { "l1", "→₁" }, + { "to1s", "→₁ₛ" }, + { "r1s", "→₁ₛ" }, + { "to_1s", "→₁ₛ" }, + { "r_1s", "→₁ₛ" }, + { "l1simplefunc", "→₁ₛ" }, + { "toa", "→ₐ" }, + { "ra", "→ₐ" }, + { "to_a", "→ₐ" }, + { "r_a", "→ₐ" }, + { "alghom", "→ₐ" }, + { "tob", "→ᵇ" }, + { "rb", "→ᵇ" }, + { "to^b", "→ᵇ" }, + { "r^b", "→ᵇ" }, + { "boundedcontinuousfunction", "→ᵇ" }, + { "tol", "→ₗ" }, + { "rl", "→ₗ" }, + { "to_l", "→ₗ" }, + { "r_l", "→ₗ" }, + { "linearmap", "→ₗ" }, + { "tosl", "→ₛₗ" }, + { "rsl", "→ₛₗ" }, + { "to_sl", "→ₛₗ" }, + { "r_sl", "→ₛₗ" }, + { "semilinearmap", "→ₛₗ" }, + { "tom", "→ₘ" }, + { "rm", "→ₘ" }, + { "to_m", "→ₘ" }, + { "r_m", "→ₘ" }, + { "aeeqfun", "→ₘ" }, + { "rp", "→ₚ" }, + { "to_p", "→ₚ" }, + { "r_p", "→ₚ" }, + { "dfinsupp", "→ₚ" }, + { "tos", "→ₛ" }, + { "rs", "→ₛ" }, + { "to_s", "→ₛ" }, + { "r_s", "→ₛ" }, + { "simplefunc", "→ₛ" }, + { "heyting", "⇨" }, + { "himp", "⇨" }, + { "hnot", "￢" }, + { "covers", "⋖" }, + { "covby", "⋖" }, + { "wcovby", "⩿" }, + { "wcovers", "⩿" }, + { "def=", "≝" }, + { "defs", "≙" }, + { "degree", "°" }, + { "dei", "ϯ" }, + { "delta", "δ" }, + { "doteqdot", "≑" }, + { "doteq", "≐" }, + { "dotplus", "∔" }, + { "dotsquare", "⊡" }, + { "dot", "·" }, + { "dong", "₫" }, + { "downarrow", "↓" }, + { "downdownarrows", "⇊" }, + { "downleftharpoon", "⇃" }, + { "downrightharpoon", "⇂" }, + { "dr-", "↘" }, + { "dr=", "⇘" }, + { "drachma", "₯" }, + { "dr", "↘" }, + { "dl-", "↙" }, + { "dl=", "⇙" }, + { "dl", "↙" }, + { "d-2", "⇊" }, + { "d-u-", "⇵" }, + { "d-|", "↧" }, + { "d-", "↓" }, + { "d==", "⟱" }, + { "d=", "⇓" }, + { "dd-", "↡" }, + { "ddagger", "‡" }, + { "ddag", "‡" }, + { "ddots", "⋱" }, + { "dz", "↯" }, + { "dib", "◆" }, + { "diw", "◇" }, + { "di.", "◈" }, + { "die", "⚀" }, + { "division", "÷" }, + { "divideontimes", "⋇" }, + { "div", "÷" }, + { "diameter", "⌀" }, + { "diamondsuit", "♢" }, + { "diamond", "⋄" }, + { "digamma", "ϝ" }, + { "di", "◆" }, + { "dagger", "†" }, + { "dag", "†" }, + { "daleth", "ℸ" }, + { "dashv", "⊣" }, + { "dh", "ð" }, + { "dvd", "∣" }, + { "m=", "≞" }, + { "meet", "⊓" }, + { "member", "∈" }, + { "mem", "∈" }, + { "measuredangle", "∡" }, + { "ma", "↦" }, + { "mapsto", "↦" }, + { "male", "♂" }, + { "maltese", "✠" }, + { "manat", "₼" }, + { "mathscr{I}", "ℐ" }, + { "minus", "−" }, + { "mill", "₥" }, + { "micro", "µ" }, + { "mid", "∣" }, + { "multiplication", "×" }, + { "multimap", "⊸" }, + { "mho", "℧" }, + { "models", "⊧" }, + { "mp", "∓" }, + { "?=", "≟" }, + { "??", "⁇" }, + { "?!", "‽" }, + { "prohibited", "🛇" }, + { "prod", "∏" }, + { "propto", "∝" }, + { "precapprox", "≾" }, + { "preceq", "≼" }, + { "precnapprox", "⋨" }, + { "precnsim", "⋨" }, + { "precsim", "≾" }, + { "prec", "≺" }, + { "preim", "⁻¹'" }, + { "preimage", "⁻¹'" }, + { "prime", "′" }, + { "pr", "↣" }, + { "powerset", "𝒫" }, + { "pounds", "£" }, + { "pound", "£" }, + { "pab", "▰" }, + { "paw", "▱" }, + { "partnership", "㉐" }, + { "partial", "∂" }, + { "paragraph", "¶" }, + { "parallel", "∥" }, + { "pa", "▰" }, + { "pm", "±" }, + { "perp", "⟂" }, + { "^perp", "ᗮ" }, + { "permil", "‰" }, + { "per", "⅌" }, + { "peso", "₱" }, + { "peseta", "₧" }, + { "pilcrow", "¶" }, + { "pitchfork", "⋔" }, + { "psi", "ψ" }, + { "phi", "φ" }, + { "leqn", "≰" }, + { "leqq", "≦" }, + { "leqslant", "≤" }, + { "leq", "≤" }, + { "len", "≰" }, + { "leadsto", "↝" }, + { "leftarrowtail", "↢" }, + { "leftarrow", "←" }, + { "leftharpoondown", "↽" }, + { "leftharpoonup", "↼" }, + { "leftleftarrows", "⇇" }, + { "leftrightarrows", "⇆" }, + { "leftrightarrow", "↔" }, + { "leftrightharpoons", "⇋" }, + { "leftrightsquigarrow", "↭" }, + { "leftthreetimes", "⋋" }, + { "lessapprox", "≲" }, + { "lessdot", "⋖" }, + { "lesseqgtr", "⋚" }, + { "lesseqqgtr", "⋚" }, + { "lessgtr", "≶" }, + { "lesssim", "≲" }, + { "le", "≤" }, + { "lub", "⊔" }, + { "lr--", "⟷" }, + { "lr-n", "↮" }, + { "lr-", "↔" }, + { "lr=n", "⇎" }, + { "lr=", "⇔" }, + { "lr~", "↭" }, + { "lrcorner", "⌟" }, + { "lr", "↔" }, + { "l-2", "⇇" }, + { "l-r-", "⇆" }, + { "l--", "⟵" }, + { "l-n", "↚" }, + { "l-|", "↤" }, + { "l->", "↢" }, + { "l-", "←" }, + { "l==", "⇚" }, + { "l=n", "⇍" }, + { "l=", "⇐" }, + { "l~", "↜" }, + { "ll-", "↞" }, + { "llcorner", "⌞" }, + { "llbracket", "〚" }, + { "ll", "≪" }, + { "lbag", "⟅" }, + { "lambda", "λ" }, + { "lamda", "λ" }, + { "lam", "λ" }, + { "lari", "₾" }, + { "langle", "⟨" }, + { "lira", "₤" }, + { "lceil", "⌈" }, + { "ldots", "…" }, + { "ldq", "“" }, + { "ldata", "《" }, + { "lfloor", "⌊" }, + { "lf", "⧏" }, + { "<|", "⧏" }, + { "lhd", "◁" }, + { "lnapprox", "⋦" }, + { "lneqq", "≨" }, + { "lneq", "≨" }, + { "lnsim", "⋦" }, + { "lnot", "¬" }, + { "longleftarrow", "⟵" }, + { "longleftrightarrow", "⟷" }, + { "longrightarrow", "⟶" }, + { "looparrowleft", "↫" }, + { "looparrowright", "↬" }, + { "lozenge", "✧" }, + { "lq", "‘" }, + { "ltimes", "⋉" }, + { "lvertneqq", "≨" }, + { "geqn", "≱" }, + { "geqq", "≧" }, + { "geqslant", "≥" }, + { "geq", "≥" }, + { "gen", "≱" }, + { "gets", "←" }, + { "ge", "≥" }, + { "glb", "⊓" }, + { "glqq", "„" }, + { "glq", "‚" }, + { "guarani", "₲" }, + { "gangia", "ϫ" }, + { "gamma", "γ" }, + { "ggg", "⋙" }, + { "gg", "≫" }, + { "gimel", "ℷ" }, + { "gnapprox", "⋧" }, + { "gneqq", "≩" }, + { "gneq", "≩" }, + { "gnsim", "⋧" }, + { "gtrapprox", "≳" }, + { "gtrdot", "⋗" }, + { "gtreqless", "⋛" }, + { "gtreqqless", "⋛" }, + { "gtrless", "≷" }, + { "gtrsim", "≳" }, + { "gvertneqq", "≩" }, + { "grqq", "“" }, + { "grq", "‘" }, + { "<=n", "≰" }, + { "<=>n", "⇎" }, + { "<=>", "⇔" }, + { "<=", "≤" }, + { "<~nn", "≴" }, + { "<~n", "⋦" }, + { "<~", "≲" }, + { "<:", "⋖" }, + { ":>", "⋗" }, + { "<->n", "↮" }, + { "<->", "↔" }, + { "<-->", "⟷" }, + { "<--", "⟵" }, + { "<-n", "↚" }, + { "<-", "←" }, + { "<<", "⟪" }, + { ">=n", "≱" }, + { ">=", "≥" }, + { ">n", "≯" }, + { ">~nn", "≵" }, + { ">~n", "⋧" }, + { ">~", "≳" }, + { ">>", "⟫" }, + { "root", "√" }, + { "scissor", "✂" }, + { "ssubn", "⊄" }, + { "ssub", "⊂" }, + { "ssupn", "⊅" }, + { "ssup", "⊃" }, + { "ssqub", "⊏" }, + { "ssqup", "⊐" }, + { "ss", "⊆" }, + { "subn", "⊈" }, + { "subseteqq", "⊆" }, + { "subseteq", "⊆" }, + { "subsetneqq", "⊊" }, + { "subsetneq", "⊊" }, + { "subset", "⊆" }, + { "ssubset", "⊂" }, + { "sub", "⊆" }, + { "supn", "⊉" }, + { "supseteqq", "⊇" }, + { "supseteq", "⊇" }, + { "supsetneqq", "⊋" }, + { "supsetneq", "⊋" }, + { "supset", "⊇" }, + { "ssupset", "⊃" }, + { "sUnion", "⋃₀" }, + { "sInter", "⋂₀" }, + { "sup", "⊔" }, + { "supr", "⨆" }, + { "surd3", "∛" }, + { "surd4", "∜" }, + { "surd", "√" }, + { "succapprox", "≿" }, + { "succcurlyeq", "≽" }, + { "succeq", "≽" }, + { "succnapprox", "⋩" }, + { "succnsim", "⋩" }, + { "succsim", "≿" }, + { "succ", "≻" }, + { "sum", "∑" }, + { "specializes", "⤳" }, + { "~>", "⤳" }, + { "squbn", "⋢" }, + { "squb", "⊑" }, + { "squpn", "⋣" }, + { "squp", "⊒" }, + { "square", "□" }, + { "squigarrowright", "⇝" }, + { "sqb", "■" }, + { "sqw", "□" }, + { "sq.", "▣" }, + { "sqo", "▢" }, + { "sqcap", "⊓" }, + { "sqcup", "⊔" }, + { "sqrt", "√" }, + { "sqsubseteq", "⊑" }, + { "sqsubset", "⊏" }, + { "sqsupseteq", "⊒" }, + { "sqsupset", "⊐" }, + { "sq", "◾" }, + { "sy", "⁻¹" }, + { "symmdiff", "∆" }, + { "st4", "✦" }, + { "st6", "✶" }, + { "st8", "✴" }, + { "st12", "✹" }, + { "stigma", "ϛ" }, + { "star", "⋆" }, + { "straightphi", "φ" }, + { "st", "⋆" }, + { "spesmilo", "₷" }, + { "span", "∙" }, + { "spadesuit", "♠" }, + { "sphericalangle", "∢" }, + { "section", "§" }, + { "searrow", "↘" }, + { "setminus", "\\" }, + { "san", "ϻ" }, + { "sampi", "ϡ" }, + { "shortmid", "∣" }, + { "sho", "ϸ" }, + { "shima", "ϭ" }, + { "shei", "ϣ" }, + { "sharp", "♯" }, + { "sigma", "σ" }, + { "simeq", "≃" }, + { "sim", "∼" }, + { "sbs", "﹨" }, + { "smallamalg", "∐" }, + { "smallsetminus", "∖" }, + { "smallsmile", "⌣" }, + { "smile", "⌣" }, + { "smul", "•" }, + { "swarrow", "↙" }, + { "Tr", "◀" }, + { "Tb", "◀" }, + { "Tw", "◁" }, + { "Tau", "Τ" }, + { "Theta", "Θ" }, + { "TH", "Þ" }, + { "union", "∪" }, + { "undertie", "‿" }, + { "uncertainty", "⯑" }, + { "un", "∪" }, + { "u+", "⊎" }, + { "u.", "⊍" }, + { "ud-|", "↨" }, + { "ud-", "↕" }, + { "ud=", "⇕" }, + { "ud", "↕" }, + { "ul-", "↖" }, + { "ul=", "⇖" }, + { "ulcorner", "⌜" }, + { "ul", "↖" }, + { "ur-", "↗" }, + { "ur=", "⇗" }, + { "urcorner", "⌝" }, + { "ur", "↗" }, + { "u-2", "⇈" }, + { "u-d-", "⇅" }, + { "u-|", "↥" }, + { "u-", "↑" }, + { "u==", "⟰" }, + { "u=", "⇑" }, + { "uu-", "↟" }, + { "upsilon", "υ" }, + { "uparrow", "↑" }, + { "updownarrow", "↕" }, + { "upleftharpoon", "↿" }, + { "uplus", "⊎" }, + { "uprightharpoon", "↾" }, + { "upuparrows", "⇈" }, + { "And", "⋀" }, + { "AA", "Å" }, + { "AE", "Æ" }, + { "Alpha", "Α" }, + { "Or", "⋁" }, + { "O+", "⨁" }, + { "directsum", "⨁" }, + { "Ox", "⨂" }, + { "O.", "⨀" }, + { "O*", "⍟" }, + { "OE", "Œ" }, + { "Omega", "Ω" }, + { "Omicron", "Ο" }, + { "Int", "ℤ" }, + { "Inter", "⋂" }, + { "bInter", "⋂" }, + { "Iota", "Ι" }, + { "Im", "ℑ" }, + { "Un", "⋃" }, + { "Union", "⋃" }, + { "bUnion", "⋃" }, + { "U+", "⨄" }, + { "U.", "⨃" }, + { "Upsilon", "Υ" }, + { "Uparrow", "⇑" }, + { "Updownarrow", "⇕" }, + { "Gl-", "ƛ" }, + { "Gl", "λ" }, + { "Gangia", "Ϫ" }, + { "Gamma", "Γ" }, + { "Glb", "⨅" }, + { "Ga", "α" }, + { "GA", "Α" }, + { "Gb", "β" }, + { "GB", "Β" }, + { "Gg", "γ" }, + { "GG", "Γ" }, + { "Gd", "δ" }, + { "GD", "Δ" }, + { "Ge", "ε" }, + { "GE", "Ε" }, + { "Gz", "ζ" }, + { "GZ", "Ζ" }, + { "Gth", "θ" }, + { "Gt", "τ" }, + { "GTH", "Θ" }, + { "GT", "Τ" }, + { "Gi", "ι" }, + { "GI", "Ι" }, + { "Gk", "κ" }, + { "GK", "Κ" }, + { "GL", "Λ" }, + { "Gm", "μ" }, + { "GM", "Μ" }, + { "Gn", "ν" }, + { "GN", "Ν" }, + { "Gx", "ξ" }, + { "GX", "Ξ" }, + { "Gr", "ρ" }, + { "GR", "Ρ" }, + { "Gs", "σ" }, + { "GS", "Σ" }, + { "Gu", "υ" }, + { "GU", "Υ" }, + { "Gf", "φ" }, + { "GF", "Φ" }, + { "Gc", "χ" }, + { "GC", "Χ" }, + { "Gp", "ψ" }, + { "GP", "Ψ" }, + { "Go", "ω" }, + { "GO", "Ω" }, + { "Inf", "⨅" }, + { "Join", "⨆" }, + { "Lub", "⨆" }, + { "Lambda", "Λ" }, + { "Lamda", "Λ" }, + { "Leftarrow", "⇐" }, + { "Leftrightarrow", "⇔" }, + { "Letter", "✉" }, + { "Lleftarrow", "⇚" }, + { "Ll", "⋘" }, + { "Longleftarrow", "⇐" }, + { "Longleftrightarrow", "⇔" }, + { "Longrightarrow", "⇒" }, + { "Meet", "⨅" }, + { "Sup", "⨆" }, + { "Sqcap", "⨅" }, + { "Sqcup", "⨆" }, + { "Lsh", "↰" }, + { "|-n", "⊬" }, + { "|-", "⊢" }, + { "|=n", "⊭" }, + { "|=", "⊨" }, + { "|->", "↦" }, + { "|=>", "⇰" }, + { "||-n", "⊮" }, + { "||-", "⊩" }, + { "||=n", "⊯" }, + { "||=", "⊫" }, + { "|||-", "⊪" }, + { "||", "‖" }, + { "fuzzy", "‖" }, + { "|n", "∤" }, + { "Com", "ℂ" }, + { "Chi", "Χ" }, + { "Cap", "⋒" }, + { "Cup", "⋓" }, + { "cul", "⌜" }, + { "cuL", "⌈" }, + { "currency", "¤" }, + { "curlyeqprec", "⋞" }, + { "curlyeqsucc", "⋟" }, + { "curlypreceq", "≼" }, + { "curlyvee", "⋎" }, + { "curlywedge", "⋏" }, + { "curvearrowleft", "↶" }, + { "curvearrowright", "↷" }, + { "cur", "⌝" }, + { "cuR", "⌉" }, + { "cup", "∪" }, + { "cu", "⌜" }, + { "cll", "⌞" }, + { "clL", "⌊" }, + { "clr", "⌟" }, + { "clR", "⌋" }, + { "clubsuit", "♣" }, + { "cl", "⌞" }, + { "construction", "🚧" }, + { "cong", "≅" }, + { "con", "⬝" }, + { "compl", "ᶜ" }, + { "complement", "ᶜ" }, + { "complementprefix", "∁" }, + { "Complement", "∁" }, + { "comp", "∘" }, + { "com", "ℂ" }, + { "coloneq", "≔" }, + { "colon", "₡" }, + { "copyright", "©" }, + { "cdots", "⋯" }, + { "cdot", "·" }, + { "cib", "●" }, + { "ciw", "○" }, + { "ci..", "◌" }, + { "ci.", "◎" }, + { "ciO", "◯" }, + { "circeq", "≗" }, + { "circlearrowleft", "↺" }, + { "circlearrowright", "↻" }, + { "circledR", "®" }, + { "circledS", "Ⓢ" }, + { "circledast", "⊛" }, + { "circledcirc", "⊚" }, + { "circleddash", "⊝" }, + { "circ", "∘" }, + { "ci", "●" }, + { "centerdot", "·" }, + { "cent", "¢" }, + { "cedi", "₵" }, + { "celsius", "℃" }, + { "ce", "ȩ" }, + { "checkmark", "✓" }, + { "chi", "χ" }, + { "cruzeiro", "₢" }, + { "caution", "☡" }, + { "cap", "∩" }, + { "qed", "∎" }, + { "quot", "⧸" }, + { "bigsolidus", "⧸" }, + { "/", "⧸" }, + { "+ ", "⊹" }, + { "b+", "⊞" }, + { "b-", "⊟" }, + { "bx", "⊠" }, + { "b.", "⊡" }, + { "bn", "ℕ" }, + { "bz", "ℤ" }, + { "bq", "ℚ" }, + { "brokenbar", "¦" }, + { "br", "ℝ" }, + { "bc", "ℂ" }, + { "bp", "ℙ" }, + { "bb", "𝔹" }, + { "bsum", "⅀" }, + { "b0", "𝟘" }, + { "b1", "𝟙" }, + { "b2", "𝟚" }, + { "b3", "𝟛" }, + { "b4", "𝟜" }, + { "b5", "𝟝" }, + { "b6", "𝟞" }, + { "b7", "𝟟" }, + { "b8", "𝟠" }, + { "b9", "𝟡" }, + { "sb0", "𝟬" }, + { "sb1", "𝟭" }, + { "sb2", "𝟮" }, + { "sb3", "𝟯" }, + { "sb4", "𝟰" }, + { "sb5", "𝟱" }, + { "sb6", "𝟲" }, + { "sb7", "𝟳" }, + { "sb8", "𝟴" }, + { "sb9", "𝟵" }, + { "bub", "•" }, + { "buw", "◦" }, + { "but", "‣" }, + { "bumpeq", "≏" }, + { "bu", "•" }, + { "biohazard", "☣" }, + { "bihimp", "⇔" }, + { "bigcap", "⋂" }, + { "bigcirc", "◯" }, + { "bigcoprod", "∐" }, + { "bigcup", "⋃" }, + { "bigglb", "⨅" }, + { "biginf", "⨅" }, + { "bigjoin", "⨆" }, + { "biglub", "⨆" }, + { "bigmeet", "⨅" }, + { "bigsqcap", "⨅" }, + { "bigsqcup", "⨆" }, + { "bigstar", "★" }, + { "bigsup", "⨆" }, + { "bigtriangledown", "▽" }, + { "bigtriangleup", "△" }, + { "bigvee", "⋁" }, + { "bigwedge", "⋀" }, + { "beta", "β" }, + { "beth", "ℶ" }, + { "between", "≬" }, + { "because", "∵" }, + { "backcong", "≌" }, + { "backepsilon", "∍" }, + { "backprime", "‵" }, + { "backsimeq", "⋍" }, + { "backsim", "∽" }, + { "barwedge", "⊼" }, + { "blacklozenge", "✦" }, + { "blacksquare", "▪" }, + { "blacksmiley", "☻" }, + { "blacktriangledown", "▾" }, + { "blacktriangleleft", "◂" }, + { "blacktriangleright", "▸" }, + { "blacktriangle", "▴" }, + { "bot", "⊥" }, + { "^bot", "ᗮ" }, + { "bowtie", "⋈" }, + { "boxminus", "⊟" }, + { "boxmid", "◫" }, + { "hcomp", "◫" }, + { "boxplus", "⊞" }, + { "boxtimes", "⊠" }, + { "join", "⊔" }, + { "r-2", "⇉" }, + { "r-3", "⇶" }, + { "r-l-", "⇄" }, + { "r--", "⟶" }, + { "r-n", "↛" }, + { "r-|", "↦" }, + { "r->", "↣" }, + { "r-o", "⊸" }, + { "r-", "→" }, + { "r==", "⇛" }, + { "r=n", "⇏" }, + { "r=", "⇒" }, + { "r~", "↝" }, + { "rr-", "↠" }, + { "reb", "▬" }, + { "rew", "▭" }, + { "real", "ℝ" }, + { "registered", "®" }, + { "re", "▬" }, + { "rbag", "⟆" }, + { "rat", "ℚ" }, + { "radioactive", "☢" }, + { "rrbracket", "〛" }, + { "rangle", "⟩" }, + { "rq", "’" }, + { "rightarrowtail", "↣" }, + { "rightarrow", "→" }, + { "rightharpoondown", "⇁" }, + { "rightharpoonup", "⇀" }, + { "rightleftarrows", "⇄" }, + { "rightleftharpoons", "⇌" }, + { "rightrightarrows", "⇉" }, + { "rightthreetimes", "⋌" }, + { "risingdotseq", "≓" }, + { "ruble", "₽" }, + { "rupee", "₨" }, + { "rho", "ρ" }, + { "rhd", "▷" }, + { "rceil", "⌉" }, + { "rfloor", "⌋" }, + { "rtimes", "⋊" }, + { "rdq", "”" }, + { "rdata", "》" }, + { "functor", "⥤" }, + { "fun", "λ" }, + { "f<<", "«" }, + { "f>>", "»" }, + { "f<", "‹" }, + { "f>", "›" }, + { "h<", "❰" }, + { "h>", "❱" }, + { "finprod", "∏ᶠ" }, + { "finsum", "∑ᶠ" }, + { "frac12", "½" }, + { "frac13", "⅓" }, + { "frac14", "¼" }, + { "frac15", "⅕" }, + { "frac16", "⅙" }, + { "frac18", "⅛" }, + { "frac1", "⅟" }, + { "frac23", "⅔" }, + { "frac25", "⅖" }, + { "frac34", "¾" }, + { "frac35", "⅗" }, + { "frac38", "⅜" }, + { "frac45", "⅘" }, + { "frac56", "⅚" }, + { "frac58", "⅝" }, + { "frac78", "⅞" }, + { "frac", "¼" }, + { "frown", "⌢" }, + { "frqq", "»" }, + { "frq", "›" }, + { "female", "♀" }, + { "fei", "ϥ" }, + { "facsimile", "℻" }, + { "fallingdotseq", "≒" }, + { "flat", "♭" }, + { "flqq", "«" }, + { "flq", "‹" }, + { "forall", "∀" }, + { ")b", "⟆" }, + { "[[", "⟦" }, + { "]]", "⟧" }, + { "{{", "⦃" }, + { "}}", "⦄" }, + { "((", "⸨" }, + { "))", "⸩" }, + { "([", "⟮" }, + { "])", "⟯" }, + { "Xi", "Ξ" }, + { "Nat", "ℕ" }, + { "Nu", "Ν" }, + { "Zeta", "Ζ" }, + { "Rat", "ℚ" }, + { "Real", "ℝ" }, + { "Re", "ℜ" }, + { "Rho", "Ρ" }, + { "Rightarrow", "⇒" }, + { "Rrightarrow", "⇛" }, + { "Rsh", "↱" }, + { "Fei", "Ϥ" }, + { "Frowny", "☹" }, + { "Hori", "Ϩ" }, + { "Heta", "Ͱ" }, + { "Khei", "Ϧ" }, + { "Koppa", "Ϟ" }, + { "Kappa", "Κ" }, + { "^a", "ᵃ" }, + { "^b", "ᵇ" }, + { "^c", "ᶜ" }, + { "^d", "ᵈ" }, + { "^e", "ᵉ" }, + { "^f", "ᶠ" }, + { "^g", "ᵍ" }, + { "^h", "ʰ" }, + { "^i", "ⁱ" }, + { "^j", "ʲ" }, + { "^k", "ᵏ" }, + { "^l", "ˡ" }, + { "^m", "ᵐ" }, + { "^n", "ⁿ" }, + { "^o", "ᵒ" }, + { "^p", "ᵖ" }, + { "^r", "ʳ" }, + { "^s", "ˢ" }, + { "^t", "ᵗ" }, + { "^u", "ᵘ" }, + { "^v", "ᵛ" }, + { "^w", "ʷ" }, + { "^x", "ˣ" }, + { "^y", "ʸ" }, + { "^z", "ᶻ" }, + { "^A", "ᴬ" }, + { "^B", "ᴮ" }, + { "^D", "ᴰ" }, + { "^E", "ᴱ" }, + { "^G", "ᴳ" }, + { "^H", "ᴴ" }, + { "^I", "ᴵ" }, + { "^J", "ᴶ" }, + { "^K", "ᴷ" }, + { "^L", "ᴸ" }, + { "^M", "ᴹ" }, + { "^N", "ᴺ" }, + { "^O", "ᴼ" }, + { "^P", "ᴾ" }, + { "^R", "ᴿ" }, + { "^T", "ᵀ" }, + { "^U", "ᵁ" }, + { "^V", "ⱽ" }, + { "^W", "ᵂ" }, + { "^0", "⁰" }, + { "^1", "¹" }, + { "^2", "²" }, + { "^3", "³" }, + { "^4", "⁴" }, + { "^5", "⁵" }, + { "^6", "⁶" }, + { "^7", "⁷" }, + { "^8", "⁸" }, + { "^9", "⁹" }, + { "^)", "⁾" }, + { "^(", "⁽" }, + { "^=", "⁼" }, + { "^+", "⁺" }, + { "^o_", "º" }, + { "^-", "⁻" }, + { "^a_", "ª" }, + { "^uhook", "ꭟ" }, + { "^ubar", "ᶶ" }, + { "^upsilon", "ᶷ" }, + { "^ltilde", "ꭞ" }, + { "^ls", "ꭝ" }, + { "^lhook", "ᶪ" }, + { "^lretroflexhook", "ᶩ" }, + { "^oe", "ꟹ" }, + { "^heng", "ꭜ" }, + { "^hhook", "ʱ" }, + { "^hwithhook", "ʱ" }, + { "^Hstroke", "ꟸ" }, + { "^theta", "ᶿ" }, + { "^turnedv", "ᶺ" }, + { "^turnedmleg", "ᶭ" }, + { "^turnedm", "ᵚ" }, + { "^turnedh", "ᶣ" }, + { "^turnedalpha", "ᶛ" }, + { "^turnedae", "ᵆ" }, + { "^turneda", "ᵄ" }, + { "^turnedi", "ᵎ" }, + { "^turnede", "ᵌ" }, + { "^turnedrhook", "ʵ" }, + { "^turnedrwithhook", "ʵ" }, + { "^turnedr", "ʴ" }, + { "^twithpalatalhook", "ᶵ" }, + { "^otop", "ᵔ" }, + { "^ezh", "ᶾ" }, + { "^esh", "ᶴ" }, + { "^eth", "ᶞ" }, + { "^eng", "ᵑ" }, + { "^zcurl", "ᶽ" }, + { "^zretroflexhook", "ᶼ" }, + { "^vhook", "ᶹ" }, + { "^Ismall", "ᶦ" }, + { "^Lsmall", "ᶫ" }, + { "^Nsmall", "ᶰ" }, + { "^Usmall", "ᶸ" }, + { "^Istroke", "ᶧ" }, + { "^Rinverted", "ʶ" }, + { "^ccurl", "ᶝ" }, + { "^chi", "ᵡ" }, + { "^shook", "ᶳ" }, + { "^gscript", "ᶢ" }, + { "^schwa", "ᵊ" }, + { "^usideways", "ᵙ" }, + { "^phi", "ᶲ" }, + { "^obarred", "ᶱ" }, + { "^beta", "ᵝ" }, + { "^obottom", "ᵕ" }, + { "^nretroflexhook", "ᶯ" }, + { "^nlefthook", "ᶮ" }, + { "^mhook", "ᶬ" }, + { "^jtail", "ᶨ" }, + { "^iota", "ᶥ" }, + { "^istroke", "ᶤ" }, + { "^ereversedopen", "ᶟ" }, + { "^stop", "ˤ" }, + { "^varphi", "ᵠ" }, + { "^vargamma", "ᵞ" }, + { "^gamma", "ˠ" }, + { "^ain", "ᵜ" }, + { "^alpha", "ᵅ" }, + { "^oopen", "ᵓ" }, + { "^eopen", "ᵋ" }, + { "^Ou", "ᴽ" }, + { "^Nreversed", "ᴻ" }, + { "^Ereversed", "ᴲ" }, + { "^Bbarred", "ᴯ" }, + { "^Ae", "ᴭ" }, + { "^SM", "℠" }, + { "^TEL", "℡" }, + { "^TM", "™" }, + { "_a", "ₐ" }, + { "_e", "ₑ" }, + { "_h", "ₕ" }, + { "_i", "ᵢ" }, + { "_j", "ⱼ" }, + { "_k", "ₖ" }, + { "_l", "ₗ" }, + { "_m", "ₘ" }, + { "_n", "ₙ" }, + { "_o", "ₒ" }, + { "_p", "ₚ" }, + { "_r", "ᵣ" }, + { "_s", "ₛ" }, + { "_t", "ₜ" }, + { "_u", "ᵤ" }, + { "_v", "ᵥ" }, + { "_x", "ₓ" }, + { "_0", "₀" }, + { "_1", "₁" }, + { "_2", "₂" }, + { "_3", "₃" }, + { "_4", "₄" }, + { "_5", "₅" }, + { "_6", "₆" }, + { "_7", "₇" }, + { "_8", "₈" }, + { "_9", "₉" }, + { "_)", "₎" }, + { "_(", "₍" }, + { "_=", "₌" }, + { "_+", "₊" }, + { "_-", "₋" }, + { "!!", "‼" }, + { "!?", "⁉" }, + { "San", "Ϻ" }, + { "Sampi", "Ϡ" }, + { "Sho", "Ϸ" }, + { "Shima", "Ϭ" }, + { "Shei", "Ϣ" }, + { "Stigma", "Ϛ" }, + { "Sigma", "Σ" }, + { "Subset", "⋐" }, + { "Supset", "⋑" }, + { "Smiley", "☺" }, + { "Psi", "Ψ" }, + { "Phi", "Φ" }, + { "Pi", "Π" }, + { "Pi0", "Π₀" }, + { "P0", "Π₀" }, + { "Pi_0", "Π₀" }, + { "P_0", "Π₀" }, + { "bfA", "𝐀" }, + { "bfB", "𝐁" }, + { "bfC", "𝐂" }, + { "bfD", "𝐃" }, + { "bfE", "𝐄" }, + { "bfF", "𝐅" }, + { "bfG", "𝐆" }, + { "bfH", "𝐇" }, + { "bfI", "𝐈" }, + { "bfJ", "𝐉" }, + { "bfK", "𝐊" }, + { "bfL", "𝐋" }, + { "bfM", "𝐌" }, + { "bfN", "𝐍" }, + { "bfO", "𝐎" }, + { "bfP", "𝐏" }, + { "bfQ", "𝐐" }, + { "bfR", "𝐑" }, + { "bfS", "𝐒" }, + { "bfT", "𝐓" }, + { "bfU", "𝐔" }, + { "bfV", "𝐕" }, + { "bfW", "𝐖" }, + { "bfX", "𝐗" }, + { "bfY", "𝐘" }, + { "bfZ", "𝐙" }, + { "bfa", "𝐚" }, + { "bfb", "𝐛" }, + { "bfc", "𝐜" }, + { "bfd", "𝐝" }, + { "bfe", "𝐞" }, + { "bff", "𝐟" }, + { "bfg", "𝐠" }, + { "bfh", "𝐡" }, + { "bfi", "𝐢" }, + { "bfj", "𝐣" }, + { "bfk", "𝐤" }, + { "bfl", "𝐥" }, + { "bfm", "𝐦" }, + { "bfn", "𝐧" }, + { "bfo", "𝐨" }, + { "bfp", "𝐩" }, + { "bfq", "𝐪" }, + { "bfr", "𝐫" }, + { "bfs", "𝐬" }, + { "bft", "𝐭" }, + { "bfu", "𝐮" }, + { "bfv", "𝐯" }, + { "bfw", "𝐰" }, + { "bfx", "𝐱" }, + { "bfy", "𝐲" }, + { "bfz", "𝐳" }, + { "MiA", "𝐴" }, + { "MiB", "𝐵" }, + { "MiC", "𝐶" }, + { "MiD", "𝐷" }, + { "MiE", "𝐸" }, + { "MiF", "𝐹" }, + { "MiG", "𝐺" }, + { "MiH", "𝐻" }, + { "MiI", "𝐼" }, + { "MiJ", "𝐽" }, + { "MiK", "𝐾" }, + { "MiL", "𝐿" }, + { "MiM", "𝑀" }, + { "MiN", "𝑁" }, + { "MiO", "𝑂" }, + { "MiP", "𝑃" }, + { "MiQ", "𝑄" }, + { "MiR", "𝑅" }, + { "MiS", "𝑆" }, + { "MiT", "𝑇" }, + { "MiU", "𝑈" }, + { "MiV", "𝑉" }, + { "MiW", "𝑊" }, + { "MiX", "𝑋" }, + { "MiY", "𝑌" }, + { "MiZ", "𝑍" }, + { "Mia", "𝑎" }, + { "Mib", "𝑏" }, + { "Mic", "𝑐" }, + { "Mid", "𝑑" }, + { "Mie", "𝑒" }, + { "Mif", "𝑓" }, + { "Mig", "𝑔" }, + { "Mii", "𝑖" }, + { "Mij", "𝑗" }, + { "Mik", "𝑘" }, + { "Mil", "𝑙" }, + { "Mim", "𝑚" }, + { "Min", "𝑛" }, + { "Mio", "𝑜" }, + { "Mip", "𝑝" }, + { "Miq", "𝑞" }, + { "Mir", "𝑟" }, + { "Mis", "𝑠" }, + { "Mit", "𝑡" }, + { "Miu", "𝑢" }, + { "Miv", "𝑣" }, + { "Miw", "𝑤" }, + { "Mix", "𝑥" }, + { "Miy", "𝑦" }, + { "Miz", "𝑧" }, + { "MIA", "𝑨" }, + { "MIB", "𝑩" }, + { "MIC", "𝑪" }, + { "MID", "𝑫" }, + { "MIE", "𝑬" }, + { "MIF", "𝑭" }, + { "MIG", "𝑮" }, + { "MIH", "𝑯" }, + { "MII", "𝑰" }, + { "MIJ", "𝑱" }, + { "MIK", "𝑲" }, + { "MIL", "𝑳" }, + { "MIM", "𝑴" }, + { "MIN", "𝑵" }, + { "MIO", "𝑶" }, + { "MIP", "𝑷" }, + { "MIQ", "𝑸" }, + { "MIR", "𝑹" }, + { "MIS", "𝑺" }, + { "MIT", "𝑻" }, + { "MIU", "𝑼" }, + { "MIV", "𝑽" }, + { "MIW", "𝑾" }, + { "MIX", "𝑿" }, + { "MIY", "𝒀" }, + { "MIZ", "𝒁" }, + { "MIa", "𝒂" }, + { "MIb", "𝒃" }, + { "MIc", "𝒄" }, + { "MId", "𝒅" }, + { "MIe", "𝒆" }, + { "MIf", "𝒇" }, + { "MIg", "𝒈" }, + { "MIh", "𝒉" }, + { "MIi", "𝒊" }, + { "MIj", "𝒋" }, + { "MIk", "𝒌" }, + { "MIl", "𝒍" }, + { "MIm", "𝒎" }, + { "MIn", "𝒏" }, + { "MIo", "𝒐" }, + { "MIp", "𝒑" }, + { "MIq", "𝒒" }, + { "MIr", "𝒓" }, + { "MIs", "𝒔" }, + { "MIt", "𝒕" }, + { "MIu", "𝒖" }, + { "MIv", "𝒗" }, + { "MIw", "𝒘" }, + { "MIx", "𝒙" }, + { "MIy", "𝒚" }, + { "MIz", "𝒛" }, + { "McA", "𝒜" }, + { "McB", "ℬ" }, + { "McC", "𝒞" }, + { "McD", "𝒟" }, + { "McE", "ℰ" }, + { "McF", "ℱ" }, + { "McG", "𝒢" }, + { "McH", "ℋ" }, + { "McI", "ℐ" }, + { "McJ", "𝒥" }, + { "McK", "𝒦" }, + { "McL", "ℒ" }, + { "McM", "ℳ" }, + { "McN", "𝒩" }, + { "McO", "𝒪" }, + { "McP", "𝒫" }, + { "McQ", "𝒬" }, + { "McR", "ℛ" }, + { "McS", "𝒮" }, + { "McT", "𝒯" }, + { "McU", "𝒰" }, + { "McV", "𝒱" }, + { "McW", "𝒲" }, + { "McX", "𝒳" }, + { "McY", "𝒴" }, + { "McZ", "𝒵" }, + { "Mca", "𝒶" }, + { "Mcb", "𝒷" }, + { "Mcc", "𝒸" }, + { "Mcd", "𝒹" }, + { "Mce", "ℯ" }, + { "Mcf", "𝒻" }, + { "Mcg", "ℊ" }, + { "Mch", "𝒽" }, + { "Mci", "𝒾" }, + { "Mcj", "𝒿" }, + { "Mck", "𝓀" }, + { "Mcl", "𝓁" }, + { "Mcm", "𝓂" }, + { "Mcn", "𝓃" }, + { "Mco", "ℴ" }, + { "Mcp", "𝓅" }, + { "Mcq", "𝓆" }, + { "Mcr", "𝓇" }, + { "Mcs", "𝓈" }, + { "Mct", "𝓉" }, + { "Mcu", "𝓊" }, + { "Mcv", "𝓋" }, + { "Mcw", "𝓌" }, + { "Mcx", "𝓍" }, + { "Mcy", "𝓎" }, + { "Mcz", "𝓏" }, + { "MCA", "𝓐" }, + { "MCB", "𝓑" }, + { "MCC", "𝓒" }, + { "MCD", "𝓓" }, + { "MCE", "𝓔" }, + { "MCF", "𝓕" }, + { "MCG", "𝓖" }, + { "MCH", "𝓗" }, + { "MCI", "𝓘" }, + { "MCJ", "𝓙" }, + { "MCK", "𝓚" }, + { "MCL", "𝓛" }, + { "MCM", "𝓜" }, + { "MCN", "𝓝" }, + { "MCO", "𝓞" }, + { "MCP", "𝓟" }, + { "MCQ", "𝓠" }, + { "MCR", "𝓡" }, + { "MCS", "𝓢" }, + { "MCT", "𝓣" }, + { "MCU", "𝓤" }, + { "MCV", "𝓥" }, + { "MCW", "𝓦" }, + { "MCX", "𝓧" }, + { "MCY", "𝓨" }, + { "MCZ", "𝓩" }, + { "MCa", "𝓪" }, + { "MCb", "𝓫" }, + { "MCc", "𝓬" }, + { "MCd", "𝓭" }, + { "MCe", "𝓮" }, + { "MCf", "𝓯" }, + { "MCg", "𝓰" }, + { "MCh", "𝓱" }, + { "MCi", "𝓲" }, + { "MCj", "𝓳" }, + { "MCk", "𝓴" }, + { "MCl", "𝓵" }, + { "MCm", "𝓶" }, + { "MCn", "𝓷" }, + { "MCo", "𝓸" }, + { "MCp", "𝓹" }, + { "MCq", "𝓺" }, + { "MCr", "𝓻" }, + { "MCs", "𝓼" }, + { "MCt", "𝓽" }, + { "MCu", "𝓾" }, + { "MCv", "𝓿" }, + { "MCw", "𝔀" }, + { "MCx", "𝔁" }, + { "MCy", "𝔂" }, + { "MCz", "𝔃" }, + { "MfA", "𝔄" }, + { "MfB", "𝔅" }, + { "MfC", "ℭ" }, + { "MfD", "𝔇" }, + { "MfE", "𝔈" }, + { "MfF", "𝔉" }, + { "MfG", "𝔊" }, + { "MfH", "ℌ" }, + { "MfI", "ℑ" }, + { "MfJ", "𝔍" }, + { "MfK", "𝔎" }, + { "MfL", "𝔏" }, + { "MfM", "𝔐" }, + { "MfN", "𝔑" }, + { "MfO", "𝔒" }, + { "MfP", "𝔓" }, + { "MfQ", "𝔔" }, + { "MfR", "ℜ" }, + { "MfS", "𝔖" }, + { "MfT", "𝔗" }, + { "MfU", "𝔘" }, + { "MfV", "𝔙" }, + { "MfW", "𝔚" }, + { "MfX", "𝔛" }, + { "MfY", "𝔜" }, + { "MfZ", "ℨ" }, + { "Mfa", "𝔞" }, + { "Mfb", "𝔟" }, + { "Mfc", "𝔠" }, + { "Mfd", "𝔡" }, + { "Mfe", "𝔢" }, + { "Mff", "𝔣" }, + { "Mfg", "𝔤" }, + { "Mfh", "𝔥" }, + { "Mfi", "𝔦" }, + { "Mfj", "𝔧" }, + { "Mfk", "𝔨" }, + { "Mfl", "𝔩" }, + { "Mfm", "𝔪" }, + { "Mfn", "𝔫" }, + { "Mfo", "𝔬" }, + { "Mfp", "𝔭" }, + { "Mfq", "𝔮" }, + { "Mfr", "𝔯" }, + { "Mfs", "𝔰" }, + { "Mft", "𝔱" }, + { "Mfu", "𝔲" }, + { "Mfv", "𝔳" }, + { "Mfw", "𝔴" }, + { "Mfx", "𝔵" }, + { "Mfy", "𝔶" }, + { "Mfz", "𝔷" }, + { "yen", "¥" }, + { "varrho", "ϱ" }, + { "varkappa", "ϰ" }, + { "varkai", "ϗ" }, + { "varnothing", "∅" }, + { "varpi", "ϖ" }, + { "varphi", "ϕ" }, + { "varprime", "′" }, + { "varpropto", "∝" }, + { "vartheta", "ϑ" }, + { "vartriangleleft", "⊲" }, + { "vartriangleright", "⊳" }, + { "varbeta", "ϐ" }, + { "varsigma", "ς" }, + { "veebar", "⊻" }, + { "vee", "∨" }, + { "ve", "ě" }, + { "vE", "Ě" }, + { "vdash", "⊢" }, + { "vdots", "⋮" }, + { "vd", "ď" }, + { "vDash", "⊨" }, + { "vD", "Ď" }, + { "vc", "č" }, + { "vC", "Č" }, + { "koppa", "ϟ" }, + { "kip", "₭" }, + { "ki", "į" }, + { "kI", "Į" }, + { "kelvin", "K" }, + { "kappa", "κ" }, + { "khei", "ϧ" }, + { "warning", "⚠" }, + { "won", "₩" }, + { "wedge", "∧" }, + { "wp", "℘" }, + { "wr", "≀" }, + { "Dei", "Ϯ" }, + { "Delta", "Δ" }, + { "Digamma", "Ϝ" }, + { "Diamond", "◇" }, + { "Downarrow", "⇓" }, + { "DH", "Ð" }, + { "zeta", "ζ" }, + { "Eta", "Η" }, + { "Epsilon", "Ε" }, + { "Beta", "Β" }, + { "Box", "□" }, + { "Bumpeq", "≎" }, + { "bbA", "𝔸" }, + { "bbB", "𝔹" }, + { "bbC", "ℂ" }, + { "bbD", "𝔻" }, + { "bbE", "𝔼" }, + { "bbF", "𝔽" }, + { "bbG", "𝔾" }, + { "bbH", "ℍ" }, + { "bbI", "𝕀" }, + { "bbJ", "𝕁" }, + { "bbK", "𝕂" }, + { "bbL", "𝕃" }, + { "bbM", "𝕄" }, + { "bbN", "ℕ" }, + { "bbO", "𝕆" }, + { "bbP", "ℙ" }, + { "bbQ", "ℚ" }, + { "bbR", "ℝ" }, + { "bbS", "𝕊" }, + { "bbT", "𝕋" }, + { "bbU", "𝕌" }, + { "bbV", "𝕍" }, + { "bbW", "𝕎" }, + { "bbX", "𝕏" }, + { "bbY", "𝕐" }, + { "bbZ", "ℤ" }, + { "bba", "𝕒" }, + { "bbb", "𝕓" }, + { "bbc", "𝕔" }, + { "bbd", "𝕕" }, + { "bbe", "𝕖" }, + { "bbf", "𝕗" }, + { "bbg", "𝕘" }, + { "bbh", "𝕙" }, + { "bbi", "𝕚" }, + { "bbj", "𝕛" }, + { "bbk", "𝕜" }, + { "bbl", "𝕝" }, + { "bbm", "𝕞" }, + { "bbn", "𝕟" }, + { "bbo", "𝕠" }, + { "bbp", "𝕡" }, + { "bbq", "𝕢" }, + { "bbr", "𝕣" }, + { "bbs", "𝕤" }, + { "bbt", "𝕥" }, + { "bbu", "𝕦" }, + { "bbv", "𝕧" }, + { "bbw", "𝕨" }, + { "bbx", "𝕩" }, + { "bby", "𝕪" }, + { "bbz", "𝕫" }, + { "Rge0", "ℝ≥0" }, + { "R>=0", "ℝ≥0" }, + { "nnreal", "ℝ≥0" }, + { "ennreal", "ℝ≥0∞" }, + { "enat", "ℕ∞" }, + { "Zsqrt", "ℤ√" }, + { "zsqrtd", "ℤ√" }, + { "liel", "⁅" }, + { "bracketl", "⁅" }, + { "lier", "⁆" }, + { "[-", "⁅" }, + { "-]", "⁆" }, + { "lsimplex", "⦋" }, + { "rsimplex", "⦌" }, + { "bracketr", "⁆" }, + { "nhds", "𝓝" }, + { "nbhds", "𝓝" }, + { "X", "⨯" }, + { "vectorproduct", "⨯" }, + { "crossproduct", "⨯" }, + { "xs", "×ˢ" }, + { "coprod", "⨿" }, + { "sigmaobj", "∐" }, + { "xf", "×ᶠ" }, + { "exf", "∃ᶠ" }, + { "Yot", "Ϳ" }, + { "goal", "⊢" }, + { "Vdash", "⊩" }, + { "Vert", "‖" }, + { "Vvdash", "⊪" }, + { "tiny", "⧾" }, + { "miny", "⧿" }, + { "heq", "≍" }, + { "r!", "¡" }, +} diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua new file mode 100644 index 0000000..da24378 --- /dev/null +++ b/builtin/runtime/lean_input.lua @@ -0,0 +1,362 @@ +-- lean_input.lua --- the Lean 4 Unicode input method (Arc 8 Stage 4b). +-- +-- Typing `\alpha` gives `α`; `\<>` gives `⟨⟩` with the point between. +-- The table is vendored in lean_abbrev.lua, generated from +-- vscode-lean4 — see that file's header and Q#LN11. +-- +-- This is a typed-edit consumer (Stage 4a, Q#LN10) registered AHEAD of +-- auto-pairing at priority 50. The ordering is load-bearing, not +-- cosmetic: 64 abbreviation keys contain a character in the `lean4` +-- pair set (`\[[]]` → `⟦⟧`, `\{{}}` → `⦃⦄`), so with pairing first, +-- typing `\[` would insert `[]` with the point between and corrupt the +-- pending key to `\[]` before the second `[` arrives — `\[[]]` becomes +-- unreachable. Priority, not load order, is what decides this; that is +-- the whole reason Stage 4a exists. +-- +-- The consumer therefore claims every keystroke that EXTENDS an open +-- pending abbreviation, not merely one that completes an expansion. A +-- consumer that claimed only completed expansions would hand each +-- intermediate `[` to pairing, which is the same corruption by a +-- different route. "Claimed" means the chain stops, not that an edit +-- was made (Q#LN22). +-- +-- UNDO IS CROSS-PEER-DEGRADED, and this is accepted rather than papered +-- over (Q#LN21). `classify_key` (src/optimistic.rs) returns `Insert(c)` +-- for `\` and for every ASCII letter — only the nine built-in pair +-- chars are excluded — so on a CRDT frontend `\alpha` arrives as six +-- SOURCE-peer optimistic inserts while the expansion is a single +-- DAEMON-peer replace spanning all six. Undo across that boundary is +-- not chronologically arbitrated. This is the same defect Q#LN6 already +-- accepts for `⟨⟩`, one order of magnitude wider: it is every +-- abbreviation the user types, not a few brackets. The general fix is +-- chronological cross-peer undo arbitration, named substrate work. +-- `set_round_trip_input` would fix it and is rejected — it also makes +-- `dispatch_idle` report false, so RET would stop inserting a newline. +-- +-- Framing: docs/lean4-mode-framing.md Q#LN11, Q#LN21, Q#LN22. + +pmacs.lean_input = pmacs.lean_input or {} + +local ed = pmacs.editor + +local LEADER = "\\" +local CURSOR = "$CURSOR" + +pmacs.config.define { + name = "lean.abbrev", + description = "Expand \\-prefixed abbreviations into Unicode symbols in Lean 4 buffers.", + type = "boolean", + default = true, + mutability = "live", +} + +-- --------------------------------------------------------------------- +-- The table, and the two indexes derived from it at load time +-- --------------------------------------------------------------------- + +-- `best[p]` is the symbol for the shortest key having `p` as a prefix, +-- ties broken by the key's position in the vendored sequence. Both +-- halves matter: 101 prefixes have equal-shortest candidates that +-- resolve to DIFFERENT symbols (`f` → `‹` from `f<`, not `›` from +-- `f>`), and the sequence's order is the only place that tie is +-- recorded. `pairs` over a map-shaped table could not express it. +-- +-- `eager[k]` marks the 1,550 keys that are complete and have no longer +-- key extending them — the ones that expand the moment they are typed, +-- with no terminator. `to` is NOT one of them (`top`, `to0`, `toa`), +-- which is exactly the case that reads as eager until the table is +-- consulted. +local best, eager = {}, {} + +do + local seq = pmacs.lean_abbrev + if type(seq) ~= "table" then seq = {} end + local extended = {} + for i = 1, #seq do + local entry = seq[i] + local key, symbol = entry[1], entry[2] + -- Walk every prefix of the key, including the key itself. Iterating + -- the sequence in order and only overwriting on a STRICTLY shorter + -- key is what makes the source-order tiebreak fall out: an equal + -- length arriving later loses to the one already recorded. + for n = 1, #key do + local p = key:sub(1, n) + local cur = best[p] + if cur == nil or #key < cur.len then + best[p] = { symbol = symbol, len = #key } + end + if n < #key then extended[p] = true end + end + end + for i = 1, #seq do + local key = seq[i][1] + if not extended[key] then eager[key] = true end + end +end + +-- Test seam (leading underscore = not stable API). Acceptance 45g reads +-- these to pin self-consistency properties a corrupt emit would break — +-- it cannot diff against `abbreviations.json`, which is not shipped. +function pmacs.lean_input._resolve(text) + local hit = best[text] + return hit and hit.symbol or nil +end + +function pmacs.lean_input._is_eager(key) + return eager[key] == true +end + +-- --------------------------------------------------------------------- +-- Pending state: one record per FRONTEND (Q#LN22) +-- --------------------------------------------------------------------- + +-- Keyed by frontend id, with the buffer stored inside and compared by +-- value. Q#LN22 specifies the key as `(frontend, buffer)`; a per- +-- frontend slot is equivalent here and avoids inventing a scalar +-- buffer key (`BufferId`'s inner value is deliberately private, R22). +-- The generality a two-level map would add is unreachable: a frontend +-- has one point, and `buffer.after-switch` clears that frontend's slot, +-- so no frontend can hold pending state in a buffer it is not in. +-- +-- Per-frontend rather than per-buffer is NOT a refinement — a buffer- +-- keyed table lets either frontend consume or discard the other's +-- half-typed abbreviation in a shared buffer, which is the ordinary +-- TUI-plus-GPU configuration this project ships. +local pending = {} + +local function frontend_id() + local ok, id = pcall(function() return pmacs.frontend.id() end) + if ok then return id end + return nil +end + +-- Is `rec` a typed edit that continues `p` exactly? Conservative by +-- construction (Q#LN22): abandonment is LAZY because pmacs has no +-- cursor-motion hook, so every guard that would have been checked at +-- the moment the user left is checked here instead, at the next typed +-- edit. +local function still_valid(p, rec, buf) + if p.buffer ~= rec.buffer or p.window ~= rec.window then return false end + -- The point must still be at the end of the pending span: the leader, + -- plus what has been typed into it, plus the character that just + -- landed. + if rec.effective_start ~= p.start_offset + 1 + #p.text then return false end + -- Exactly one edit since this frontend last extended the pending + -- abbreviation — the one being processed now. Deliberately strict + -- across frontends: `revision()` is BUFFER-GLOBAL, so a peer editing + -- the shared buffer invalidates this record even though it edited + -- elsewhere. Keeping it alive would mean translating and validating + -- the span through arbitrary peer edits, substrate Stage 4b does not + -- add. + local ok, rev = pcall(function() return buf:revision() end) + if not ok or rev ~= p.expected_revision + 1 then return false end + return true +end + +-- --------------------------------------------------------------------- +-- Expansion +-- --------------------------------------------------------------------- + +-- Replace the pending span with `symbol`, placing the point at +-- `$CURSOR` if the symbol carries one. Returns the byte offset just +-- past the replacement, or nil when the edit was rejected or altered. +-- +-- ONE `buf:replace` for the whole expansion: one undo step, one CRDT +-- op, one effective-edit verification. A rejection drops the pending +-- state and does not retry, the same discipline as comment.lua's Q#CT5 +-- and pair.lua. +local function expand(buf, p, symbol, span_end) + local cursor_at = symbol:find(CURSOR, 1, true) + local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol + + local start = p.start_offset + local ok, estart, estop, einserted = pcall(function() + return buf:replace(start, span_end, text) + end) + if not ok then + ed.set_status("lean abbreviation rejected by buffer intercept") + return nil + end + if estart ~= start or estop ~= span_end or einserted ~= #text then + ed.set_status("lean abbreviation altered by buffer intercept") + return nil + end + + -- The point MUST be placed explicitly. Unlike pairing's at-cursor + -- insert, this replace SHRINKS the buffer — `\alpha` (6 bytes) + -- becomes `α` (2) — and a point left at the pre-edit offset is past + -- the new end. Every later self-insert is then silently rejected and + -- the editor looks dead. There is no daemon re-grounding that covers + -- this; that only holds for an edit that lands at the cursor. + ed.goto_byte(cursor_at and (start + cursor_at - 1) or (start + #text)) + return start + #text +end + +-- --------------------------------------------------------------------- +-- The consumer +-- --------------------------------------------------------------------- + +local function on_typed_edit(rec) + local fid = frontend_id() + if fid == nil then return false end + + -- A fan-out carrying no record is still information: a paste, + -- programmatic edit or replicated op landed, so whatever this + -- frontend had pending no longer describes the buffer. Drop it and + -- decline — this is why the chain calls consumers with nil rather + -- than skipping them (Q#LN10). + if not rec then + pending[fid] = nil + return false + end + if not (ed.this_command and ed.this_command() == "buffer.self-insert") then + pending[fid] = nil + return false + end + + -- Both gates resolve against the SOURCE buffer of the typed edit, not + -- the active one — a context-switching command may have replaced it + -- by callback time (pair.lua round 2, finding 2). + if not pmacs.config.get("lean.abbrev", rec.buffer) then + pending[fid] = nil + return false + end + local lang + if pmacs.lsp and pmacs.lsp.buffer_language then + local ok, l = pcall(pmacs.lsp.buffer_language, rec.buffer) + if ok then lang = l end + end + if lang ~= "lean4" then + -- No pending abbreviation is ever OPENED outside a `lean4` buffer: + -- `\` in Rust is an ordinary character and `\[` there still pairs. + pending[fid] = nil + return false + end + + local buf = pmacs.window.buffer() + if not buf or buf ~= rec.buffer or pmacs.window.current() ~= rec.window then + pending[fid] = nil + return false + end + -- Fail closed on a transformed source self-insert, as pairing does: + -- expanding on top of a relocated or rewritten character compounds + -- the intercept's result. + if not rec.clean then + pending[fid] = nil + return false + end + + local revision + do + local ok, rev = pcall(function() return buf:revision() end) + if not ok then + pending[fid] = nil + return false + end + revision = rev + end + + local p = pending[fid] + if p and not still_valid(p, rec, buf) then + p = nil + pending[fid] = nil + end + + local ch = rec.char + + -- No pending abbreviation: only the leader opens one. + if not p then + if ch == LEADER then + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = rec.effective_start, + text = "", + expected_revision = revision, + } + -- Claimed: the leader belongs to the abbreviation, and pairing + -- has no interest in it either way. + return true + end + return false + end + + -- Pending: does any key still have `text .. ch` as a prefix? + local extended = p.text .. ch + if best[extended] then + p.text = extended + p.expected_revision = revision + if eager[extended] then + local span_end = p.start_offset + 1 + #extended + pending[fid] = nil + expand(buf, p, best[extended].symbol, span_end) + end + -- Claimed either way: an extension that has not yet completed must + -- NOT reach auto-pairing (`\[` in `\[[]]`). + return true + end + + -- `ch` does not extend the abbreviation. Expand what is pending + -- FIRST, then let `ch` stand as ordinary text — the terminator is + -- retained, not consumed, and it sits inside the replaced span so the + -- whole thing is one undo step. + pending[fid] = nil + local hit = best[p.text] + local after + if hit and #p.text > 0 then + -- `span_end` covers the terminator: the leader, the pending text, + -- and `ch`, which has already landed. What replaces it is the + -- symbol followed by `ch` itself. + local span_end = p.start_offset + 1 + #p.text + #ch + after = expand(buf, p, hit.symbol .. ch, span_end) + end + + -- A terminating `\` re-arms as a NEW leader at its own position + -- (`\alpha\to` → `α→`). Upstream gets this from `processChange`, + -- where a finished abbreviation reports `isAffected = false` and so + -- does not suppress the new-leader branch. This is not the `\\` case: + -- there the pending text is empty, `\` EXTENDS, and the result is one + -- literal backslash with no pending state left open. + if ch == LEADER then + local start = after and (after - #ch) or rec.effective_start + local ok, rev = pcall(function() return buf:revision() end) + if ok then + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = start, + text = "", + expected_revision = rev, + } + end + return true + end + + -- Claimed only if an expansion actually happened. Otherwise `ch` is + -- an ordinary character in a Lean buffer and auto-pairing should see + -- it — `\zz` leaves `z` free to pair if it ever were a pair char. + return after ~= nil +end + +-- Q#KR11's seam: a detached frontend's pending state must not outlive +-- it. Ids are monotonic, so this table would otherwise grow for the +-- life of the session. +pmacs.hook.add("frontend.detached", function(fid) + pending[fid] = nil +end) + +-- `buffer.after-switch` fires with NO arguments, so it cannot say whose +-- switch it was. The acting frontend is the one that produced the most +-- recent dispatched input event, which is what `pmacs.frontend.id()` +-- reports at callback time. Clearing every entry instead would let one +-- frontend's navigation discard another's half-typed abbreviation. +pmacs.hook.add("buffer.after-switch", function() + local fid = frontend_id() + if fid ~= nil then pending[fid] = nil end +end) + +pmacs.typed_edit.add_consumer { + name = "lean-abbrev", + priority = 50, + fn = on_typed_edit, +} diff --git a/docs/active-work.md b/docs/active-work.md index 9a847b1..7bb63ff 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -14,8 +14,8 @@ 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` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a - #167, the bottom-panel landed-doc refresh #156, the inline-math slice + `githubsucks/main` @ `a27f646` (Lean 4 Stage 4a #179 atop Stage 3b + #170, 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; @@ -57,172 +57,93 @@ 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 4a IN REVIEW +## Lean 4 lane (Arc 8) — Stages 1–4a MERGED; Stage 4b IN REVIEW -- **Stages 1, 2, 3a and 3b are MERGED** — #160 (`main` @ `0827dd1`), - #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`). Their full +- **Stages 1, 2, 3a, 3b and 4a are MERGED** — #160 (`main` @ `0827dd1`), + #161 (`46a1b8f`), #167 (`6f348c9`), #170 (`d400f30`), #179 + (`a27f646`). Their full histories were pruned from this ledger in round 6, per this file's own instruction to remove entries when their PR merges; the durable facts now live in `docs/agent-handoff.md` §1's Lean 4 bullet, which is where - a fresh machine should read them. `docs/lean4-mode-framing.md` rev 8 + a fresh machine should read them. `docs/lean4-mode-framing.md` rev 9 carries the decisions. -### Stage 4 — framing rev 8, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`) +### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`) -- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170** - (`main` @ `d400f30`), 2026-07-26. Both were integrated against a main - that had advanced 50 commits mid-review; the only conflict either time - was this ledger's own lane headings, resolved by keeping both sides. -- Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`. - 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 - external (upstream) facts held. Fixed in rev 7: Stage 4a's footprint - omitted the test file its own acceptance requires; pending - abbreviation state was keyed by buffer when pmacs is **multi-frontend** - (`EditorCore.views` is per-`FrontendId`, `take_typed_edit` is already - frontend-keyed, and `buffer.after-switch` fires with NO arguments, so - a buffer-keyed clear lets any frontend discard another's pending - state); the shortest-match rule was missing its **tie-break by source - declaration order**, which 101 prefixes depend on and a `pairs`- - iterated Lua map cannot express; and the generator's "abort on keys - needing escaping" rule **rejects the real table** (`\` is a key, `"` - begins eleven). -- **A 404 on a guessed path is not evidence of absence.** Rev 6 declared - the upstream package ships no README after fetching the package root, - with the directory listing showing `src/README.md` already in hand. - The README states the tie rule in one sentence. -- **Round 7 review found one remaining P1 in acceptance 45i.** Rev 7 - required A's pending abbreviation to survive B editing the same - buffer, while Q#LN22 also required an exact buffer-revision advance. - Those cannot both hold: revisions are buffer-global and every edit - bumps them. Rev 8 keeps the conservative guard and separates - ownership from survival — B cannot consume A's record, but B editing - the shared buffer invalidates A lazily; B switching buffers or - detaching remains frontend-scoped when no shared-buffer edit - intervenes. -- **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).** - 4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua` - plus `pair.lua` re-expressed as one registered consumer, no behavior - change. 4b is the input method. The split is forced by §4's own rule, - which Stage 4's risk column ("refactors `pair.lua`'s provenance read") - broke while the prose called the stage Lean-only. -- **This is the SECOND consecutive re-scout to find that rule broken** - (round 4 found it for Stage 3). Rev 5 had even noticed the shape and - answered it with a commit boundary. **A commit boundary is not a review - boundary.** Re-check every remaining stage against §4 at scout time; - the rule is not self-enforcing. -- **Rev 5's expansion semantics were wrong in three ways**, found by - reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring - from behavior. Resolution is *shortest key having the input as a - prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no - terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'` - is a key, so `\\` → `\`); and an unmatchable tail is **appended**, - not dropped (`\alp7` → `α7`). -- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving - the cursor out abandons it") was not buildable. Abandonment is lazy — - validated at the next typed edit — and the criterion now asserts what - pmacs can actually detect. Upstream drives this off `changeSelections`; - that seam does not exist here. -- **`dispatch_key` is only half the production path for 4b.** The - auto-pair suite gets away with dispatch-only because Q#AP1 removed the - pair chars from the optimistic classifiers; `\` and the letters are - NOT excluded, so on a CRDT frontend the optimistic producer is the real - path. That producer is `#[cfg(feature = "crdt")]` and CI never enables - `crdt`, and the gate list runs `--features crdt` only for `--lib` — a - crdt-gated integration test is **dark twice over**. -- The whole expansion has cross-peer-degraded undo (Q#LN21): six - source-peer optimistic inserts replaced by one daemon-peer op. - `set_round_trip_input` would fix it and is rejected — it also disables - `dispatch_idle`, so RET stops inserting a newline. -- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all - keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are - proper prefixes of another (so 1,550 expand eagerly), **26** values - carry `$CURSOR`, and **119** are multi-codepoint — the 26 - `$CURSOR`-bearing values plus 93 others. -- Citation sweep per COHERENCE §25: five live citations moved in the 50 - commits since rev 5 — `take_typed_edit` 12827→12990, - `handle_server_requests` 1549→1815, `fs.stat` 93→133, - `detect_buffer_language` 452→457, `send_request`/`send_notification` - 9342/9361→9507/9527. -### Stage 4a — the typed-edit consumer chain (IMPLEMENTED, same branch) - -- Footprint exactly as Q#LN10 declares it: `builtin/runtime/typed_edit.lua` - (new), `pair.lua` re-expressed as one consumer, - `src/editor.rs` +15 (the `include_str!` and its ordering comment), and - `tests/typed_edit_chain_acceptance.rs` (new, 13 tests). - **`tests/auto_pair_acceptance.rs` is UNCHANGED — `git diff --stat - main...HEAD -- tests/auto_pair_acceptance.rs` is empty.** That is - criterion 46 checked at the diff, which is the only way it means - anything. -- **The chain calls consumers even when the record is nil.** This is a - decision, not an implementation detail: three existing auto-pairing - tests assert `pmacs.pair._last_record == nil` after a record-less - fan-out (paste, programmatic insert, nested manual `hook.run`), so - skipping consumers on nil fails them. Stage 4b needs the same - delivery to abandon a pending abbreviation an unrelated edit - invalidated. -- **Ordered insertion, not `table.sort`** — Lua's sort is not stable, and - "ties broken by registration order" is a stated contract. -- **The chain `pcall`s each consumer** and reports through - `set_status`. Rev 7 justified this by claiming an uncontained throw - would fail the fan-out for every other subscriber including lsp.lua's - didChange flush; **that is wrong** — `run_all_must_succeed` - (`src/hook.rs:332`) collects errors and continues, so the other - subscribers still run. The real consequence is narrower and still - worth containing: the throw skips every LATER consumer in the chain. - The rendering is protected too, because a Lua error may be a table - whose `__tostring` throws. -- **Round 8 (review) findings, all fixed on this branch:** each consumer - now gets its **own shallow copy** of the record (the same table let a - declining consumer rewrite `rec.char`, which pairing reads — typing - `x` could produce `x)`); the fan-out iterates a **snapshot** (a - consumer registering a lower-priority one shifted itself forward under - `ipairs` and ran twice, unbounded if repeated); `tostring` moved - inside the containment; **non-finite and non-integer priorities are - rejected** (NaN is a number and every ordered comparison with it is - false, so it landed wherever the insertion scan gave up and silently - voided the ordering contract); and `add_consumer` now returns a handle - with `remove_consumer` beside it, so re-evaluating a config no longer - leaks callbacks the way `pmacs.hook.add` does (COHERENCE §13). -- **Every acceptance test is bite-verified by mutation**, per the - standing rule that a test is not evidence until the mutation it - targets has been shown to fail it: +- Framing `docs/lean4-mode-framing.md` **revision 9**, approved. Stage + 4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b, + the Lean content that registers on it. +- Footprint: `scripts/regen-lean-abbrev` (new, the generator), + `builtin/runtime/lean_abbrev.lua` (new, VENDORED DATA — 1,855 entries + from `leanprover/vscode-lean4@17d1d08`, Apache-2.0), + `builtin/runtime/lean_input.lua` (new, the consumer at priority 50), + `src/editor.rs` (two `include_str!` blocks), + `tests/lean_input_acceptance.rs` (new, 25 tests), and one + `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs` + (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart + from the load sites and that one test. +- **Round 9 corrected three acceptance criteria that the real table + contradicts** — found by simulating the state machine over all 1,855 + entries and re-reading upstream at the pinned commit, not by reading + the prose again. `\to` is NOT eager (`top`, `to0`, `toa` extend it); + `\zzzz` expands to `ζzzz ` because `ze`/`zeta`/`zsqrtd` exist, and + only `$ % , ; @ W` open no key at all; and `\alpha`'s undo does not + restore `\alpha ` because `alpha` IS eager, so the terminator is a + separate edit. Criteria 38, 41 and 42 now state both paths. +- **Two generator bugs, both caught by its own round-trip check + failing closed:** `str.splitlines()` also splits on U+2028/U+2029, + and 53 symbols contain one literally, so the check reported a count + mismatch that was its own bug; then escaping via `chr(byte)` produced + a latin-1-shaped string that `write_text(encoding="utf-8")` + re-encoded, and every non-ASCII symbol landed double-encoded. The + first version of the check compared IN-MEMORY strings and agreed with + itself. **It now stages the file, re-reads the bytes from disk, and + renames into place only on a match.** +- **The point must be placed explicitly after the replace.** The + expansion SHRINKS the buffer (`\alpha` 6 bytes → `α` 2), so a point + left at the pre-edit offset is past the new end and every later + self-insert is silently rejected — the editor looks dead after the + first expansion. Pairing's "no cursor motion on the clean path" does + not generalize: that holds only for an insert AT the cursor. +- **Three tests were vacuous when first written and were found by + biting, not by review:** the abandonment test asserted text that a + wrongly-surviving record would also produce (claiming makes no edit — + it needed the follow-up keystroke that completes an eager key); the + re-arm test used the framing's own `\alpha\to`, which never reaches + the re-arm branch because `alpha` is eager and closes the record + first (`\al\to` does); and both buffer-switch tests passed through + `find_or_open`'s fresh-load path, which fires `buffer.after-load` and + a record-less edit rather than `buffer.after-switch` — deleting the + subscriber left them green. All three now bite. +- **Bite table** (each mutation, and the tests it fails): | Mutation | Tests it fails | |---|---| - | append instead of ordered insert | 5 chain | - | `>=` instead of `>` in the insert scan | 1 chain (tiebreak) | - | re-take the record per consumer | 4 chain | - | ignore the claim return value | 1 chain | - | drop the `pcall` | 1 chain | - | skip consumers when `rec == nil` | 1 chain + **3 auto-pair** | - | load `typed_edit.lua` after `lsp.lua` | 1 chain + **2 auto-pair** (Q#AP7) | - | hand every consumer the same record table | 1 chain (46f) | - | iterate the live array instead of a snapshot | 1 chain (46g) | - | render the error outside the `pcall` | 1 chain (46d) | - | accept any Lua number as a priority | 1 chain (46h) | - | make `remove_consumer` a no-op | 2 chain (46g, 46h) | + | register at priority 150 (after pairing) | 2 | + | claim only completed expansions | 2 | + | longest match instead of shortest | 9 | + | equal-length tie keeps the LATER key | 3 | + | remove the eager branch | 8 | + | expand without the terminator in the span | 2 | + | remove the re-arm branch | 1 | + | remove the point-still-at-span-end check | 1 | + | remove the exact-revision check | 1 | + | leave the point where the replace found it | 5 | + | remove the `lean4` language gate | 1 | + | remove the `lean.abbrev` gate | 2 | + | `buffer.after-switch` clears every frontend | 1 | + | delete the `buffer.after-switch` subscriber | 1 | + | `frontend.detached` purges every frontend | 1 | - The first attempt at the last bite was WORTHLESS as written: moving - only `typed_edit.lua` past `lsp.lua` left `pair.lua` calling a nil - `add_consumer`, so the runtime failed to load and all 9 tests died — - loud, but not a test of the flush-ordering property. Moving - `typed_edit.lua` AND `pair.lua` past `lsp.lua` is the faithful - falsification: registration succeeds, the hook lands late, and exactly - the three ordering tests fail. **A bite that kills everything has not - isolated anything.** -- Verification on this branch (commit-then-gate, so this describes the - pushed tree): `cargo fmt --check` clean; strict workspace Clippy - clean; 1,832 default + 2,009 CRDT library tests; auto-pair 45/45; - typed-edit chain 13/13 (and 13/13 again under `--no-default-features - --features lua54`, since the fixes touch `math.huge`, `%`, and - `__tostring` behavior that differs between the backends); M4 121; - required GPU 202; **isolated-config workspace sweep 3,332 across 97 - suites, zero failures** with `grep -c basedpyright` = 0; `git diff - --check` clean. -- Stage 4b (the input method) is NOT in this PR and not started. + Acceptance 45f bit by construction: without a registered window for + the source frontend it ran six fan-outs with a nil record and proved + nothing, because `handle_remote_crdt_op` arms nothing unless the + source's active window displays the buffer. +- Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED, + named in the module header (Q#LN21): six source-peer optimistic + inserts replaced by one daemon-peer op. `set_round_trip_input` would + fix it and also disables `dispatch_idle`, so RET would stop inserting + a newline. ## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165) diff --git a/docs/agent-handoff.md b/docs/agent-handoff.md index 66ccc25..23108f4 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -1,7 +1,9 @@ # Agent handoff — cross-machine continuity -**Last updated: 2026-07-26, after Lean 4 stages 3a and 3b (#167, #170) -landed — pmacs' first Lean language server — following the inline-math +**Last updated: 2026-07-26, after Lean 4 Stage 4a (#179) landed — the +typed-edit consumer chain, the substrate the Unicode input method +registers on — atop stages 3a and 3b (#167, #170), pmacs' first Lean +language server, and 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 @@ -88,9 +90,9 @@ commands, read `docs/active-work.md` immediately after this file. config swap invalidates. The durable lesson is to heal at **consumption** — the point where a stale record is handed out — not at the moment of the swap. - - **Stage 4a (typed-edit consumer chain) is implemented and in review - as PR #179** (branch `lean4-stage4a-typed-edit-chain`, framing rev - 8). It is substrate only: `builtin/runtime/typed_edit.lua` owns the + - **Stage 4a (typed-edit consumer chain) MERGED as #179** (`main` @ + `a27f646`, two review rounds). It is substrate only: + `builtin/runtime/typed_edit.lua` owns the single `buffer.after-edit` subscriber and the single one-shot read, `pair.lua` becomes its first registered consumer, and `tests/auto_pair_acceptance.rs` is unchanged by zero lines @@ -104,10 +106,36 @@ commands, read `docs/active-work.md` immediately after this file. iterates a **snapshot**, because a consumer that registers a lower-priority one shifts itself forward under `ipairs` and runs twice. - - Remaining: Stage 4b (the Unicode input method) is framed and - awaiting approval — not started; stages 5 (goal panel), 6 (`#eval` - output channel), and 7 (module hierarchy) are framed but not - scouted against current `main`. + - **Round 8's durable lesson: `run_all_must_succeed` does NOT abort + the fan-out.** `src/hook.rs:332` collects each callback's error and + continues to the remaining subscribers, marking only the run + failed — so an uncontained throw inside a hook subscriber does not + stop `lsp.lua` from flushing didChange. Two framing revisions + asserted the opposite to justify a `pcall`. The guard was right and + the reason was wrong, and by the time review caught it the wrong + reason had been copied into a module comment, an acceptance + criterion, a test comment, and the ledger. **Correct the source a + rationale derives from, not only the sites that quote it.** + - **Stage 4b (the Unicode input method) is implemented and in review** + (branch `lean4-stage4b-input-method`, framing rev 9): a vendored + 1,855-entry table generated from `leanprover/vscode-lean4@17d1d08` + by `scripts/regen-lean-abbrev`, plus a consumer registered on the + Stage 4a chain at priority 50, ahead of pairing. Its durable facts: + the table must stay an ORDERED SEQUENCE (equal-length ties resolve + by source declaration order, which a `pairs`-iterated map cannot + express); a generator round-trip check must re-read the BYTES ON + DISK, because comparing in-memory strings cannot see an encoding + applied by the write itself; and an expansion that SHRINKS the + buffer must place the point explicitly, or every later self-insert + is silently rejected and the editor looks dead. + - **Round 9 corrected three approved acceptance criteria** by + simulating the state machine over all 1,855 entries rather than + re-reading the prose. Four review rounds over the text had not + found them, because each named an example that reads as obviously + right and is wrong only against the data. + - Remaining: stages 5 (goal panel), 6 (`#eval` output channel), and 7 + (module hierarchy) are framed but not scouted against current + `main`. - **Inline math LANDED — #158** (`docs/inline-math-slice-framing.md` rev 3; merge `5aa9044`). pmacs renders `$…$` as typeset mathematics in the GPU diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md index c4a32e5..72a83fd 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: **8**. +Revision 1 — initial. Current revision: **9**. ### Round 1 (rev 1 → rev 2) @@ -503,6 +503,38 @@ documentation cleanups. others — matching §2.11 and Q#LN11. 3. **§9.1's revision label was stale.** It now names rev 8. +### Round 9 (rev 8 → rev 9) + +Found during Stage 4b implementation, by simulating Q#LN22's state +machine over all 1,855 vendored entries and re-reading upstream's +`TrackedAbbreviation.ts` and `AbbreviationProvider.ts` at `17d1d08`. +**Three acceptance criteria named examples that the real table +contradicts** — every one of them written from what the abbreviation +*looks* like rather than from whether the table makes it eager. + +1. **Acceptance 41 was false.** `\to` does not expand eagerly: `to` is a + proper prefix of `top`, `to0`, `toa` and others, so upstream's + `isAbbreviationUniqueAndComplete` is false and `to` is not among the + 1,550 eager keys. The criterion now uses `\alpha`, which has no + extension, and additionally pins that `\to` alone does **not** + expand — the false half is worth an assertion because it reads as + correct until the table is consulted. +2. **Acceptance 42 was false.** `\zzzz` + space yields `ζzzz `, not + literal text: `z` opens a pending abbreviation (`ze`, `zeta`, + `zsqrtd`) and the second `z` finishes it. Exactly six printable + characters open no key — `$ % , ; @ W` — and the criterion now uses + `\WWWW`. +3. **Acceptance 38's undo claim was false for its own example.** + `alpha` is eager, so `\alpha` expands before the space is typed and + the space is a separate edit; one undo removes the space rather than + restoring `\alpha `. The criterion now states the finish path and the + eager path separately, since "one expansion is one undo step" is true + of both while the text an undo restores is not. + +The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were +errors in the examples chosen to pin it, which is why a simulation over +the real data found them and four review rounds over the prose did not. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -2452,12 +2484,22 @@ criterion 46 requires to stay byte-identical. **Stage 4b — the Unicode input method** -38. `\alpha` + space yields `α ` — the space lands first and the - expansion runs in the following `buffer.after-edit`, so the - terminator is **retained**, not consumed. The expansion is a single - undo step: one undo restores `\alpha ` (with its space), not - `\alph`. Rev 6 wrote the post-undo text as `\alpha`, which would be - true only if the terminator were swallowed. +38. **Terminators are retained, and one expansion is one undo step — + but which text an undo restores depends on the path.** Rev 8 stated + a single rule here and it is wrong against the real table, because + it assumed `\alpha` takes the finish path when `alpha` is in the + 1,550-key eager set (round 9; see 41). + - *Finish path.* `\alp` + space yields `α `: the space lands first + and the expansion runs in the following `buffer.after-edit`, so + the terminator is **retained**, not consumed, and it is inside the + replaced span. One undo restores `\alp ` — with its space, not + `\al`. Rev 6 wrote the post-undo text without the terminator, + which would be true only if the terminator were swallowed. + - *Eager path.* `\alpha` yields `α` with no terminator typed, and a + following space is a **separate** edit. One undo removes the + space; a second restores `\alpha`. Asserting the finish-path undo + text here would fail, which is the trap this split exists to + record. 39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` placeholder. 40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is @@ -2467,9 +2509,21 @@ criterion 46 requires to stay byte-identical. only completed expansions rather than pending extensions — **both failure modes must be shown**, since they are distinct bugs with the same symptom. -41. `\to` yields `→` eagerly on uniqueness, with no terminator typed. -42. A prefix with no match (`\zzzz` + space) is left as literal text; no - edit is made. +41. **Eager expansion on uniqueness**, with no terminator typed: + `\alpha` yields `α` the moment the final `a` lands. Rev 8 used `\to` + here and that is false against the real table (round 9): `to` is a + proper prefix of `top`, `to0`, `toa` and others, so + `isAbbreviationUniqueAndComplete` is false and `to` is **not** in + the 1,550-key eager set. `\to` alone stays `\to`; `\to` + space + yields `→ ` by the finish path. Both are asserted, because the + wrong one reads as correct until the table is consulted. +42. A prefix that opens no key at all — `\WWWW` + space — is left as + literal text and **no edit is made**. Rev 8 used `\zzzz`, which + expands (round 9): `z` opens a pending abbreviation because `ze`, + `zeta` and `zsqrtd` exist, and the second `z` finishes it, giving + `ζzzz `. Exactly six printable characters open no key: `$ % , ; @ + W`. Bites against an implementation that treats "no complete match" + as "no pending state". 43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion hook, this asserts what pmacs can actually detect: after `\alp`, an explicit `goto_byte` elsewhere followed by typing `h` inserts a @@ -2698,7 +2752,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from languages other than Lean, and §4's rule is what keeps them out of a Lean PR. -### 9.1 Coherence impact — stages 4a and 4b (rev 8) +### 9.1 Coherence impact — stages 4a and 4b (rev 9) **Sections served.** §6 (interaction islands) primarily, and in the *preventing* direction rather than the fixing one — see below. §11 diff --git a/scripts/regen-lean-abbrev b/scripts/regen-lean-abbrev new file mode 100755 index 0000000..14091aa --- /dev/null +++ b/scripts/regen-lean-abbrev @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""Regenerate builtin/runtime/lean_abbrev.lua from vscode-lean4. + +Usage: scripts/regen-lean-abbrev + +Fetches `lean4-unicode-input/src/abbreviations.json` at the given commit +and rewrites the vendored Lua table, including the provenance header, so +the artifact is self-describing to whoever next touches it. A refresh is +an ordinary PR with a visible diff — the diff is the review. + +There is no automatic sync and none is wanted: an editor that silently +re-downloads its input method has a supply-chain problem, not a feature +(docs/lean4-mode-framing.md Q#LN11). + +The emit is an ORDERED SEQUENCE, not a map. Upstream resolves +equal-length abbreviation ties by source declaration order — 101 +prefixes depend on it — and a Lua `{ [key] = symbol }` table iterated +with `pairs` cannot carry that. A map-shaped emit would also be +nondeterministic across builds and, once a hash order happened to be +stable, stably wrong. + +This script ABORTS rather than emitting something plausible when the +source is corrupt: a duplicate key after decoding (JSON permits them, +the table must not), a key or symbol that is not well-formed UTF-8, or a +round-trip mismatch. That last check re-parses the script's own output +with an independent unescaper and compares the full ordered sequence to +the source, entry for entry. It is what makes the vendored file +trustworthy, and it belongs here rather than in the acceptance suite: +the suite cannot see `abbreviations.json`, which is not shipped. +""" + +import json +import pathlib +import sys +import urllib.request + +REPO = "leanprover/vscode-lean4" +PATH = "lean4-unicode-input/src/abbreviations.json" +LICENSE = "Apache-2.0" +OUT = pathlib.Path(__file__).resolve().parent.parent / "builtin/runtime/lean_abbrev.lua" + +# Canonical, lossless, byte-deterministic. Rev 6 of the framing said the +# generator should abort on "a key containing a character the emitted Lua +# would have to escape"; that rule rejects the real table, where `\` is a +# key and `"` begins eleven of them. +SHORT = {"\\": "\\\\", '"': '\\"', "\n": "\\n", "\r": "\\r", "\t": "\\t"} + + +def die(msg): + print(f"regen-lean-abbrev: {msg}", file=sys.stderr) + raise SystemExit(1) + + +def lua_escape(s): + """Escape one string for a Lua double-quoted literal. + + Operates on CHARACTERS, not bytes. Decomposing to UTF-8 bytes and + emitting each as `chr(byte)` produces a latin-1-shaped string that + `write_text(..., encoding="utf-8")` then re-encodes — every + non-ASCII symbol lands in the file double-encoded, and a round-trip + check that compares in-memory strings agrees with itself and misses + it entirely. Only control bytes, which are single-byte by + definition, become `\\ddd`. + """ + out = [] + for ch in s: + if ch in SHORT: + out.append(SHORT[ch]) + elif ord(ch) < 0x20 or ord(ch) == 0x7F: + out.append(f"\\{ord(ch):03d}") + else: + out.append(ch) + return "".join(out) + + +def lua_unescape(s): + """Independent reader for the round-trip check. + + Deliberately not the inverse of `lua_escape` sharing its table: a + check that reuses the encoder's own assumptions cannot detect that + those assumptions are wrong. + """ + out = bytearray() + i = 0 + raw = s.encode("utf-8") + while i < len(raw): + b = raw[i] + if b != ord("\\"): + out.append(b) + i += 1 + continue + i += 1 + if i >= len(raw): + die("round-trip: trailing backslash in emitted string") + nxt = chr(raw[i]) + if nxt in ("\\", '"'): + out.append(ord(nxt)) + i += 1 + elif nxt in ("n", "r", "t"): + out.append({"n": 10, "r": 13, "t": 9}[nxt]) + i += 1 + elif nxt.isdigit(): + digits = "" + while i < len(raw) and chr(raw[i]).isdigit() and len(digits) < 3: + digits += chr(raw[i]) + i += 1 + out.append(int(digits)) + else: + die(f"round-trip: unknown escape \\{nxt} in emitted string") + return out.decode("utf-8") + + +def main(): + if len(sys.argv) != 2: + die(f"usage: {sys.argv[0]} ") + commit = sys.argv[1] + url = f"https://raw.githubusercontent.com/{REPO}/{commit}/{PATH}" + + with urllib.request.urlopen(url, timeout=60) as resp: + raw = resp.read() + + try: + raw.decode("utf-8") + except UnicodeDecodeError as e: + die(f"source is not well-formed UTF-8: {e}") + + # `object_pairs_hook` keeps declaration order AND exposes duplicate + # keys, which a plain dict would silently collapse. + pairs = json.loads(raw, object_pairs_hook=lambda kv: kv) + + seen = {} + for i, (key, symbol) in enumerate(pairs): + if key in seen: + die(f"duplicate key {key!r} at entries {seen[key]} and {i}") + seen[key] = i + for label, s in (("key", key), ("symbol", symbol)): + if not isinstance(s, str): + die(f"{label} at entry {i} is not a string: {s!r}") + try: + s.encode("utf-8") + except UnicodeEncodeError as e: + die(f"{label} at entry {i} is not well-formed UTF-8: {e}") + + cursor = sum(1 for _, v in pairs if "$CURSOR" in v) + for i, (key, symbol) in enumerate(pairs): + if symbol.count("$CURSOR") > 1: + die(f"symbol for {key!r} at entry {i} has more than one $CURSOR") + + body = "".join( + f' {{ "{lua_escape(k)}", "{lua_escape(v)}" }},\n' for k, v in pairs + ) + text = HEADER.format( + repo=REPO, + path=PATH, + commit=commit, + license=LICENSE, + count=len(pairs), + cursor=cursor, + bytes=len(raw), + script=pathlib.Path(sys.argv[0]).name, + ) + "pmacs.lean_abbrev = {\n" + body + "}\n" + + # Round-trip against the BYTES ON DISK, not the string in memory. + # The file is staged beside its destination, re-read, parsed, and + # only renamed into place once it compares equal entry for entry. A + # check that compares in-memory strings cannot see an encoding + # applied by the write itself, which is exactly how a + # double-encoding bug survived the first version of this script. + staged = OUT.with_suffix(".lua.staged") + staged.write_text(text, encoding="utf-8") + on_disk = staged.read_bytes().decode("utf-8") + + got = [] + # `str.splitlines()` is WRONG here: it also splits on U+2028, U+2029, + # U+0085 and the vertical-tab family, and 53 symbols in the real + # table contain one of those literally. It silently loses entries and + # the round-trip then reports a count mismatch that is the checker's + # bug, not the emit's. The emitted file's line structure is defined + # by the LF we write, and nothing else. + for line in on_disk.split("\n"): + line = line.strip() + if not line.startswith('{ "') or not line.endswith("},"): + continue + inner = line[1:-2].strip() + if not (inner.startswith('"') and inner.endswith('"')): + die(f"round-trip: unparsable emitted line: {line!r}") + fields, buf, esc, depth = [], [], False, 0 + for ch in inner: + if esc: + buf.append(ch) + esc = False + elif ch == "\\": + buf.append(ch) + esc = True + elif ch == '"': + depth += 1 + if depth % 2 == 0: + fields.append("".join(buf)) + buf = [] + elif depth % 2 == 1: + buf.append(ch) + if len(fields) != 2: + die(f"round-trip: expected 2 fields, got {len(fields)}: {line!r}") + got.append((lua_unescape(fields[0]), lua_unescape(fields[1]))) + + def fail(msg): + staged.unlink(missing_ok=True) + die(msg) + + if len(got) != len(pairs): + fail(f"round-trip: emitted {len(got)} entries, source has {len(pairs)}") + for i, (want, have) in enumerate(zip(pairs, got)): + if tuple(want) != have: + fail(f"round-trip: entry {i} differs: source {want!r} vs emitted {have!r}") + + staged.replace(OUT) + print( + f"wrote {OUT} — {len(pairs)} entries from {REPO}@{commit} " + f"({len(raw)} source bytes, {OUT.stat().st_size} emitted bytes), " + "round-trip verified against the bytes on disk" + ) + + +HEADER = """\ +-- lean_abbrev.lua --- VENDORED DATA. Do not edit by hand. +-- +-- The Lean 4 abbreviation table, generated from: +-- +-- repo: https://github.com/{repo} +-- path: {path} +-- commit: {commit} +-- license: {license} +-- entries: {count} ({cursor} carry $CURSOR) +-- source: {bytes} bytes +-- +-- Regenerate with: +-- +-- scripts/{script} {commit} +-- +-- An ORDERED SEQUENCE, not a map: upstream resolves equal-length ties +-- by source declaration order (101 prefixes depend on it), and a +-- `pairs`-iterated Lua map cannot express that. The file's own line +-- order is the audit trail. Consumers must not reorder it. +-- +-- Not fetched at runtime and not a package dependency: the input method +-- has to work offline and on first launch. Upkeep is a documented +-- manual process — see docs/lean4-mode-framing.md Q#LN11. + +pmacs = pmacs or {{}} + +""" + +if __name__ == "__main__": + main() diff --git a/src/daemon.rs b/src/daemon.rs index 84716eb..e34a6d6 100644 --- a/src/daemon.rs +++ b/src/daemon.rs @@ -3964,6 +3964,143 @@ mod tests { ); } + /// Arc 8 Stage 4b acceptance 45f: the Lean abbreviation expander + /// works on the OPTIMISTIC producer, not only on `dispatch_key`. + /// + /// This is the path most users take and the one no other Stage 4b + /// test covers. `classify_key` (`src/optimistic.rs`) returns + /// `Insert(c)` for `\` and for every ASCII letter — only the nine + /// built-in pair chars are excluded (Q#AP1) — so on a CRDT frontend + /// `\alpha` arrives here as six source-peer optimistic inserts, + /// while the expansion is a single daemon-peer replace spanning all + /// six. That asymmetry is the accepted undo degradation of Q#LN21; + /// what this pins is that the expansion happens at all. + /// + /// It lives in `--lib` deliberately: the gate list runs + /// `--features crdt` only for `cargo test --lib`, so a crdt-gated + /// INTEGRATION test would be dark in CI and dark in the gates both. + /// + /// The source frontend needs a REGISTERED WINDOW on the edited + /// buffer or nothing is armed at all — `handle_remote_crdt_op` + /// arms the record only when the source's active window displays + /// the buffer, so a source with no view fails closed and silently. + /// A version of this test without the view below passed six + /// fan-outs with a nil record and proved nothing. + #[cfg(feature = "crdt")] + #[test] + fn the_optimistic_producer_also_expands_a_lean_abbreviation() { + use crate::editor::EditorState; + use crate::protocol::FrontendId; + use crate::window::{FrontendView, Layout, Window, WindowId}; + + let dir = std::env::temp_dir().join(format!("pmacs-lean-opt-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("create temp dir"); + let path = dir.join("a.lean"); + std::fs::write(&path, "").expect("write fixture"); + + let source = FrontendId(77); + let mut editor = EditorState::new(); + editor + .lua_host + .eval(Some("test"), "pmacs.lsp.config = {}") + .expect("clear lsp config"); + editor + .lua_host + .eval( + Some("test-open"), + &format!( + "pmacs.buffer.find_or_open({:?}); pmacs.editor.goto_byte(0)", + path.display().to_string() + ), + ) + .expect("open the lean fixture"); + + let buffer_id = editor.core.borrow().active_window().buffer_id; + { + let mut core = editor.core.borrow_mut(); + let mut reg = core.registry.borrow_mut(); + reg.get_mut(buffer_id) + .expect("active buffer") + .upgrade_to_crdt(2) + .expect("upgrade to crdt"); + drop(reg); + + // The replica's own window on the shared buffer. + let text_view = { + let registry = core.registry.clone(); + let reg = registry.borrow(); + crate::text_view::TextView::new(reg.get(buffer_id).expect("buffer")) + }; + let win_id = WindowId::next(); + core.windows + .insert(win_id, Window::new(win_id, buffer_id, text_view)); + core.register_frontend_view( + source, + FrontendView { + layout: Layout::single(win_id), + active: win_id, + fold_projection: true, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + } + + let snapshot_bytes = { + let core = editor.core.borrow(); + let reg = core.registry.borrow(); + reg.get(buffer_id) + .expect("buffer") + .crdt_state() + .expect("crdt-backed") + .export_snapshot() + .expect("export snapshot") + }; + let peer = loro::LoroDoc::new(); + peer.set_peer_id(77).expect("set peer id"); + peer.import(&snapshot_bytes).expect("import snapshot"); + + // One op per keystroke, exactly as the attach loop's + // optimistic-apply branch produces them. + for (i, ch) in "\\alpha".chars().enumerate() { + let v_before = peer.oplog_vv(); + peer.get_text("body") + .insert(i, &ch.to_string()) + .expect("peer insert"); + let op_bytes = peer + .export(loro::ExportMode::updates(&v_before)) + .expect("export op"); + super::handle_remote_crdt_op( + &mut editor, + source, + buffer_id, + crate::rope::CrdtOp { + peer_id: 77, + bytes: op_bytes, + }, + ); + } + + let text = match editor + .lua_host + .eval( + Some("test-readback"), + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ) + .expect("read buffer text") + { + mlua::Value::String(s) => String::from_utf8_lossy(&s.as_bytes()).into_owned(), + other => panic!("expected buffer text, got {other:?}"), + }; + assert_eq!( + text, "α", + "the abbreviation expanded on the optimistic path — the \ + record the expander reads is armed by handle_remote_crdt_op, \ + not only by dispatch_key" + ); + } + /// Q#AI9 (PR #109 round 1): the optimistic-apply arm clears an /// EMPTY anchor on the source window — the GPU always takes this /// path, and the TUI attach mirror tracks no selection state, so diff --git a/src/editor.rs b/src/editor.rs index a19971e..3b3b274 100644 --- a/src/editor.rs +++ b/src/editor.rs @@ -445,6 +445,27 @@ impl EditorState { include_str!("../builtin/runtime/pair.lua"), ) .expect("load pair builtin chunk"); + // Arc 8 Stage 4b: the Lean 4 Unicode input method. The vendored + // abbreviation table first — lean_input.lua reads it at chunk + // load to build its prefix and eager-key indexes. Both load + // after typed_edit.lua, which they register into. + // + // Load order does NOT decide whether abbreviation expansion or + // auto-pairing sees a keystroke first — the chain's priority + // does (50 vs 100), which is why Stage 4a exists. It matters + // only that the chain itself is already there. + lua_host + .eval( + Some("@pmacs/builtin/runtime/lean_abbrev.lua"), + include_str!("../builtin/runtime/lean_abbrev.lua"), + ) + .expect("load lean_abbrev builtin chunk"); + lua_host + .eval( + Some("@pmacs/builtin/runtime/lean_input.lua"), + include_str!("../builtin/runtime/lean_input.lua"), + ) + .expect("load lean_input builtin chunk"); lua_host .eval( Some("@pmacs/builtin/runtime/lsp.lua"), diff --git a/tests/lean_input_acceptance.rs b/tests/lean_input_acceptance.rs new file mode 100644 index 0000000..01ee89e --- /dev/null +++ b/tests/lean_input_acceptance.rs @@ -0,0 +1,678 @@ +//! Lean 4 Unicode input method acceptance (Arc 8 Stage 4b, +//! docs/lean4-mode-framing.md Q#LN11/Q#LN21/Q#LN22, criteria 38–45i). +//! +//! Dispatch-driven throughout: `dispatch_key` is the producer that arms +//! the typed-edit record for a grid frontend. The optimistic CRDT +//! producer is criterion 45f and lives in a `--lib` test, where the gate +//! list's `--features crdt` run reaches it. + +use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; +use pmacs::editor::EditorState; +use pmacs::protocol::FrontendId; +use pmacs::window::{FrontendView, Layout, Window, WindowId}; +use std::path::PathBuf; +use std::sync::atomic::{AtomicUsize, Ordering}; + +fn fresh_dir() -> PathBuf { + static SEQ: AtomicUsize = AtomicUsize::new(0); + let dir = std::env::temp_dir().join(format!( + "pmacs-leaninput-{}-{}", + std::process::id(), + SEQ.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir_all(&dir).unwrap(); + dir +} + +fn key(code: KeyCode) -> KeyEvent { + KeyEvent { + code, + modifiers: KeyModifiers::NONE, + kind: KeyEventKind::Press, + state: KeyEventState::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 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 type_as(s: &mut EditorState, fid: FrontendId, chars: &str) { + for ch in chars.chars() { + s.dispatch_key(fid, key(KeyCode::Char(ch))); + } +} + +fn type_str(s: &mut EditorState, chars: &str) { + type_as(s, FrontendId::LOCAL, chars); +} + +/// An editor with an empty `.lean` file open and the point at 0. +/// `pmacs.lsp.config = {}` keeps the real user config from spawning a +/// server; the language still resolves from the extension. +fn lean_editor() -> (EditorState, PathBuf) { + let dir = fresh_dir(); + let f = dir.join("a.lean"); + std::fs::write(&f, "").unwrap(); + let s = EditorState::new(); + exec(&s, "pmacs.lsp.config = {}"); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + assert_eq!( + eval::>( + &s, + "return pmacs.lsp.buffer_language(pmacs.window.buffer())" + ) + .as_deref(), + Some("lean4"), + "the fixture must actually be a lean4 buffer, or every \ + expansion assertion below is vacuous" + ); + (s, f) +} + +// --------------------------------------------------------------------------- +// 38 / 41 — the two expansion paths, and what an undo restores +// --------------------------------------------------------------------------- + +#[test] +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. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp "); + assert_eq!(text(&s), "α ", "terminator retained, not consumed"); + + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!( + text(&s), + "\\alp ", + "one undo restores the pre-expansion text WITH its terminator — \ + the expansion is a single edit" + ); +} + +#[test] +fn the_eager_path_takes_no_terminator_and_undoes_separately() { + // `alpha` has no longer key extending it, so it is one of the 1,550 + // eager keys: it expands the moment the final `a` lands, and a + // following space is a SEPARATE edit. Rev 8 asserted the finish-path + // undo text for this example, which is the trap (round 9). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "α", "eager expansion, no terminator typed"); + + type_str(&mut s, " "); + assert_eq!(text(&s), "α "); + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!(text(&s), "α", "the first undo removes the separate space"); + exec(&s, "pmacs.window.buffer():undo()"); + assert_eq!(text(&s), "\\alpha", "the second undoes the expansion"); +} + +#[test] +fn to_is_not_eager_because_longer_keys_extend_it() { + // The criterion rev 8 got wrong: `to` looks unique and is not. + // `top`, `to0`, `toa` and others extend it, so it needs a + // terminator. Bites against an eager rule that tests only "is this + // a key" without asking whether anything extends it. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\to"); + assert_eq!(text(&s), "\\to", "no expansion without a terminator"); + + type_str(&mut s, " "); + assert_eq!(text(&s), "→ ", "the finish path then resolves it"); +} + +// --------------------------------------------------------------------------- +// 39 — $CURSOR +// --------------------------------------------------------------------------- + +#[test] +fn the_cursor_placeholder_places_the_point_between_the_symbols() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\<>"); + assert_eq!(text(&s), "⟨⟩"); + // The placeholder is a point position, not a literal: typing lands + // between the brackets. + type_str(&mut s, "x"); + assert_eq!(text(&s), "⟨x⟩", "$CURSOR left the point inside"); +} + +// --------------------------------------------------------------------------- +// 40 — the pair collision +// --------------------------------------------------------------------------- + +#[test] +fn a_pending_abbreviation_is_never_corrupted_by_auto_pairing() { + // 64 keys contain a `lean4` pair-set character. Two DISTINCT bugs + // produce the same symptom here, so both are asserted: pairing + // running first, and a consumer that claims only completed + // expansions (which would hand each intermediate `[` to pairing). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\["); + assert_eq!( + text(&s), + "\\[", + "the intermediate `[` was CLAIMED — pairing inserted no `]`, \ + which is what keeps `\\[[]]` reachable" + ); + + type_str(&mut s, "[]]"); + assert_eq!(text(&s), "⟦⟧", "the full key resolves"); +} + +#[test] +fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { + // The other direction: claiming extensions must not disable pairing + // in Lean buffers generally. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "["); + assert_eq!(text(&s), "[]", "ordinary auto-pairing is untouched"); +} + +// --------------------------------------------------------------------------- +// 42 — a prefix that opens nothing +// --------------------------------------------------------------------------- + +#[test] +fn a_prefix_that_opens_no_key_is_left_literal_with_no_edit() { + // `W` is one of exactly six printable characters that begin no key + // (`$ % , ; @ W`). Rev 8 used `\zzzz`, which expands — `ze`, `zeta` + // and `zsqrtd` exist (round 9). + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\WWWW "); + assert_eq!(text(&s), "\\WWWW ", "literal text, no expansion"); +} + +#[test] +fn a_prefix_with_no_complete_match_still_expands_its_best_prefix() { + // The case rev 8 mistook for "no match": `z` DOES open a pending + // abbreviation, and the second `z` finishes it. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\zzzz "); + assert_eq!(text(&s), "ζzzz ", "`z` resolved through `ze`"); +} + +// --------------------------------------------------------------------------- +// 43 — lazy abandonment +// --------------------------------------------------------------------------- + +#[test] +fn moving_the_point_away_abandons_the_pending_abbreviation() { + // There is no cursor-motion hook, so the pending record is + // validated at the NEXT typed edit: the point must still be at the + // end of the pending span. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp"); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, "h"); + assert_eq!(text(&s), "h\\alp", "the `h` landed as plain text"); + + // The keystroke that makes abandonment OBSERVABLE. Asserting only + // the line above proves nothing: claiming an extension makes no + // edit, so a record that wrongly survived would look identical + // here. If `h` had extended the record to `alph`, this `a` + // completes `alpha` and eagerly expands — over a span whose offsets + // are now stale by one. + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "ha\\alp", + "`\\alp` is still literal: the record was dropped when the \ + point left the end of its span, not carried along" + ); +} + +#[test] +fn switching_buffers_clears_pending_state_eagerly() { + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + + // Open the second buffer FIRST, then come back. `find_or_open` + // fires `buffer.after-switch` only on the already-open branch — a + // fresh load fires `buffer.after-load` instead, and its own insert + // fires a record-less `buffer.after-edit`. Without this warm-up the + // test passes through the nil-record path and pins nothing about + // switching: deleting the after-switch subscriber leaves it green. + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + + type_str(&mut s, "\\alph"); + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "\\alpha", + "without the switch this would have eagerly expanded to α; \ + `buffer.after-switch` cleared the record" + ); +} + +// --------------------------------------------------------------------------- +// 44 / 45 — the setting and the language gate, both on the SOURCE buffer +// --------------------------------------------------------------------------- + +#[test] +fn disabling_the_setting_stops_expansion() { + let (mut s, _f) = lean_editor(); + exec(&s, "pmacs.config.set('lean.abbrev', false)"); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "no expansion when disabled"); + + exec(&s, "pmacs.config.set('lean.abbrev', true)"); + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, " \\alpha"); + assert_eq!(text(&s), "\\alpha α", "and it comes back live"); +} + +#[test] +fn the_setting_is_read_against_the_typed_edits_source_buffer() { + // A buffer-local override must not follow the user to another + // buffer of the same language — the `editing.auto-pair` precedent, + // including its round-2 correction to resolve `rec.buffer` rather + // than `pmacs.window.buffer()`. + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + + exec( + &s, + "pmacs.config.set_local(pmacs.window.buffer(), 'lean.abbrev', false)", + ); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "disabled in THIS buffer"); + + let od = other.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "α", "a second lean buffer is unaffected"); + + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + assert_eq!(text(&s), "\\alpha", "and the first is still disabled"); +} + +#[test] +fn no_abbreviation_state_is_opened_outside_a_lean_buffer() { + let dir = fresh_dir(); + let f = dir.join("a.rs"); + std::fs::write(&f, "").unwrap(); + let s = EditorState::new(); + exec(&s, "pmacs.lsp.config = {}"); + let fd = f.display().to_string(); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + let mut s = s; + + type_str(&mut s, "\\alpha"); + assert_eq!(text(&s), "\\alpha", "no expansion in Rust"); + + // And the leader opened nothing, so `[` still pairs normally. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\["); + assert_eq!( + text(&s), + "\\alpha\\[]", + "`\\[` in a Rust buffer pairs — the input method never armed" + ); +} + +// --------------------------------------------------------------------------- +// 45a / 45b / 45c / 45d / 45e — resolution rules +// --------------------------------------------------------------------------- + +#[test] +fn the_shortest_key_wins_not_the_longest() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp "); + assert_eq!(text(&s), "α ", "`alp` resolves through `alpha`"); + + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\al "); + assert_eq!( + text(&s), + "α ∀ ", + "`al` resolves through `all` (3) — NOT `alpha` (5). A \ + longest-match or unique-match-only rule passes the first \ + assertion and fails this one" + ); +} + +#[test] +fn an_unmatchable_tail_is_appended_not_dropped() { + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp7 "); + assert_eq!( + text(&s), + "α7 ", + "`7` finished `alp`; it is kept, not swallowed, and the whole \ + abbreviation is not abandoned" + ); +} + +#[test] +fn there_is_no_terminator_list() { + // `'+ '` is a key — a trailing SPACE is part of it. Bites against + // any hardcoded space/tab/RET terminator set. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\+ "); + assert_eq!(text(&s), "⊹", "the space EXTENDED rather than terminating"); +} + +#[test] +fn a_doubled_backslash_yields_one_literal_backslash() { + // Not a terminator case: the pending text is empty, `\` is itself a + // key, and it extends-and-eagerly-matches. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\\\"); + assert_eq!(text(&s), "\\", "one literal backslash"); + + // ...and no pending state was left open, so an ordinary letter is + // an ordinary letter. + type_str(&mut s, "n"); + assert_eq!(text(&s), "\\n", "two characters, not a newline"); +} + +#[test] +fn a_terminating_backslash_re_arms_as_a_new_leader() { + // `al` is NOT eager, so its pending record is still open when the + // second `\` arrives: the `\` terminates it, the expansion runs, + // and the same `\` must then open a fresh abbreviation. + // + // The framing's own example — `\alpha\to` — does NOT exercise this + // branch: `alpha` is eager, so the record is already closed and the + // `\` is handled by the ordinary open-a-leader path. It passes with + // the re-arm branch deleted, which is why the non-eager case is the + // one asserted first. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\al\\to "); + assert_eq!( + text(&s), + "∀→ ", + "the terminating `\\` expanded `al` AND opened a new \ + abbreviation at its own position" + ); + + // The criterion's example still holds, by the other route. + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\alpha\\to "); + assert_eq!(text(&s), "∀→ α→ "); +} + +#[test] +fn an_inserted_backslash_does_not_re_arm() { + // `setminus` expands to a literal `\`. That backslash is a + // programmatic replace, which arms no typed-edit record — so it + // opens no pending abbreviation. Bites against a future consumer + // that infers pending state from buffer text instead of provenance. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\setminus"); + assert_eq!(text(&s), "\\", "expanded to a literal backslash"); + + type_str(&mut s, "n"); + assert_eq!( + text(&s), + "\\n", + "the letter after it is a plain letter — the INSERTED backslash \ + armed nothing" + ); +} + +// --------------------------------------------------------------------------- +// 45h — the tie-break by source declaration order +// --------------------------------------------------------------------------- + +#[test] +fn equal_length_candidates_break_by_source_declaration_order() { + // `f<` and `f>` are both length 2. `f<` is declared first, so `\f` + // resolves to `‹`. This is the criterion that bites a map-shaped + // vendored table: with `pairs` iteration it passes or fails by hash + // order. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\f "); + assert_eq!(text(&s), "‹ ", "`f<` wins over `f>` by source order"); + + exec(&s, "pmacs.editor.goto_byte(pmacs.window.buffer():len())"); + type_str(&mut s, "\\\" "); + assert_eq!( + text(&s), + "‹ Ä ", + "`\"A` is the first of eleven equal-length candidates" + ); +} + +#[test] +fn reversing_the_vendored_sequence_reverses_the_tie() { + // The falsification 45h requires: run the same resolution against a + // deliberately reversed sequence and show it changes. If this did + // NOT change, the tie-break would not be reading source order at + // all and the assertion above would be passing by luck. + let (s, _f) = lean_editor(); + let forward: String = eval(&s, "return pmacs.lean_input._resolve('f')"); + assert_eq!(forward, "‹"); + + let reversed: String = eval( + &s, + " + local seq = pmacs.lean_abbrev + local rev = {} + for i = #seq, 1, -1 do rev[#rev + 1] = seq[i] end + -- Resolve `f` the way the module does, over the reversed order. + local best = nil + for i = 1, #rev do + local k, v = rev[i][1], rev[i][2] + if k:sub(1, 1) == 'f' then + if best == nil or #k < best.len then best = { sym = v, len = #k } end + end + end + return best.sym + ", + ); + assert_eq!( + reversed, "›", + "reversed source order picks `f>` — the tie really is decided \ + by position in the sequence" + ); +} + +// --------------------------------------------------------------------------- +// 45g — table integrity, limited to what the suite can actually check +// --------------------------------------------------------------------------- + +#[test] +fn the_vendored_table_is_self_consistent() { + // `abbreviations.json` is not shipped, so the suite cannot diff + // against it; the full source-fidelity check belongs to the + // generator, which re-parses its own output from disk. What is + // checkable here are the properties a corrupt emit breaks. + let (s, _f) = lean_editor(); + + let count: i64 = eval(&s, "return #pmacs.lean_abbrev"); + assert_eq!( + count, 1855, + "the declared entry count for the recorded upstream commit" + ); + + let (unique, cursor_ok, utf8_ok): (i64, bool, bool) = eval( + &s, + r#" + local seen, n = {}, 0 + local cursor_ok, utf8_ok = true, true + for i = 1, #pmacs.lean_abbrev do + local k, v = pmacs.lean_abbrev[i][1], pmacs.lean_abbrev[i][2] + if not seen[k] then seen[k] = true; n = n + 1 end + local _, c = v:gsub("%$CURSOR", "") + if c > 1 then cursor_ok = false end + -- A Lua pattern cannot validate UTF-8; check the shape the + -- emitter guarantees instead: no lone continuation byte at the + -- start of a sequence and no truncated tail. + if k:find("[\128-\191]") == 1 then utf8_ok = false end + end + return n, cursor_ok, utf8_ok + "#, + ); + assert_eq!( + unique, 1855, + "every key is unique — a collision would silently drop entries \ + from the derived lookup" + ); + assert!(cursor_ok, "no symbol carries more than one $CURSOR"); + assert!(utf8_ok, "no key begins with a continuation byte"); + + // The resolution spot-set named by 45g. + for (input, want) in [ + ("alpha", "α"), + ("to", "→"), + ("<>", "⟨$CURSOR⟩"), + ("+ ", "⊹"), + ("\\\\", "\\"), + ("n", "\\n"), + ("setminus", "\\"), + ("f", "‹"), + ] { + let got: String = eval(&s, &format!("return pmacs.lean_input._resolve('{input}')")); + assert_eq!(got, want, "resolution of {input:?}"); + } + + // The eager set is the one the state machine branches on. + let alpha_eager: bool = eval(&s, "return pmacs.lean_input._is_eager('alpha')"); + let to_eager: bool = eval(&s, "return pmacs.lean_input._is_eager('to')"); + assert!(alpha_eager, "`alpha` has no extension"); + assert!(!to_eager, "`to` is extended by `top`, `to0`, `toa`, …"); +} + +// --------------------------------------------------------------------------- +// 45i — pending state is per frontend +// --------------------------------------------------------------------------- + +/// Register a second frontend on the SAME buffer, with its own window. +fn attach_frontend(s: &EditorState, fid: FrontendId) -> WindowId { + let mut core = s.core.borrow_mut(); + let buffer_id = core.active_buffer_id(); + let text_view = { + let registry = core.registry.clone(); + let reg = registry.borrow(); + pmacs::text_view::TextView::new(reg.get(buffer_id).unwrap()) + }; + let win_id = WindowId::next(); + core.windows + .insert(win_id, Window::new(win_id, buffer_id, text_view)); + core.register_frontend_view( + fid, + FrontendView { + layout: Layout::single(win_id), + active: win_id, + fold_projection: true, + panel_capable: true, + frame_geometry: None, + panel_hidden: false, + }, + ); + win_id +} + +const B: FrontendId = FrontendId(9); + +#[test] +fn a_peer_edit_to_the_shared_buffer_abandons_the_pending_record() { + let (mut s, _f) = lean_editor(); + let b_win = attach_frontend(&s, B); + // B sits at the start of the buffer; A types at the end. + s.core.borrow_mut().windows.get_mut(&b_win).unwrap().cursor = 0; + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + type_as(&mut s, B, "p"); + assert!( + text(&s).contains('p'), + "B's keystroke landed as ordinary text rather than extending \ + A's abbreviation, got {:?}", + text(&s) + ); + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert!( + !text(&s).contains('∀'), + "A's record was abandoned: `revision()` is buffer-global, so \ + B's edit invalidates it even though B edited elsewhere. Got {:?}", + text(&s) + ); +} + +#[test] +fn a_peer_buffer_switch_does_not_clear_another_frontends_record() { + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("b.lean"); + std::fs::write(&other, "").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + // Warm up both buffers so B's switch takes `find_or_open`'s + // already-open branch, which is the only one that fires + // `buffer.after-switch`. A fresh load fires `buffer.after-load` + // and a record-less edit instead — and that path clears pending + // state for a different reason, which would make this test green + // no matter whose entries the subscriber clears. + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + attach_frontend(&s, B); + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + + // B switches buffers WITHOUT editing the shared buffer. + // Only B moves: the switch is scoped to B's own window, so A's + // window still shows the shared buffer with A's point where it was. + s.core.borrow_mut().active_frontend = B; + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + s.core.borrow_mut().active_frontend = FrontendId::LOCAL; + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert_eq!( + text(&s), + "∀ ", + "`buffer.after-switch` clears only the ACTING frontend's \ + entries — a blanket clear would discard A's half-typed \ + abbreviation" + ); +} + +#[test] +fn detaching_a_frontend_purges_only_its_own_pending_state() { + let (mut s, _f) = lean_editor(); + attach_frontend(&s, B); + + type_as(&mut s, FrontendId::LOCAL, "\\al"); + exec(&s, &format!("pmacs.hook.run('frontend.detached', {})", B.0)); + + type_as(&mut s, FrontendId::LOCAL, "l "); + assert_eq!( + text(&s), + "∀ ", + "B's detachment purged B's entries and left A's record valid" + ); +} From f3103a6953d42b27aceb94b1d6bc631d8f725ba6 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 16:47:54 -0400 Subject: [PATCH 2/4] fix(lean4): defer the expansion past the chain, and guard its point MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three defects, all about what happens AROUND the expansion rather than about resolving an abbreviation. A pair character that TERMINATES an abbreviation never reached auto-pairing: `\alp(` gave `α(`. Q#LN22 already said the terminator is not claimed and the implementation claimed it whenever an expansion succeeded. Merely declining is not enough either — the chain hands each consumer a copy of the record made before any consumer ran, so expanding inside the chain invalidates the copy pairing is holding and the closer is silently lost. Verified by mutation rather than assumed: expand-then-decline reproduces `α(` exactly. The expansion therefore runs on its OWN `buffer.after-edit` subscriber, registered after typed_edit.lua's and before lsp.lua's. A claim stops the chain but not a separate subscriber, which is the point: pairing claims the terminator it reacts to. The replaced span now covers only the leader and the typed text, so pairing's closer lands outside it and survives. One undo restores the same text either way, because the terminator was always its own insert. That second subscriber is a new instance of Q#AP7 — lsp.lua flushes didChange synchronously on the signature-trigger path, and `(` is a trigger — so acceptance 45m pins it with the sighelp fake server: no didChange may ever carry the unexpanded text. The relevance check is now three-part, as pairing's has been since #110: buffer, window, AND `ed.cursor() == rec.post_cursor`. A redefined self-insert can insert the completing character and then move the point, and expanding over a span the user has left teleports them back into it. Cursor placement after the replace is context-guarded, as `repair_cursor` is. A buffer intercept may switch buffers while `buf:replace` runs; the unguarded `goto_byte` then translated the Lean buffer's pre-edit point through the Lean buffer's edit and applied it to whatever was ambient. Q#LN22, criterion 38's span wording, and the ledger are corrected to describe the deferred design rather than the one that shipped — the rationale's source, not only the sites quoting it. Acceptance 45j/45k/ 45l/45m added; framing rev 10. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/lean_input.lua | 192 ++++++++++++++++++++------ docs/active-work.md | 25 +++- docs/agent-handoff.md | 9 +- docs/lean4-mode-framing.md | 112 +++++++++++++-- tests/lean_input_acceptance.rs | 241 +++++++++++++++++++++++++++++++++ 5 files changed, 523 insertions(+), 56 deletions(-) diff --git a/builtin/runtime/lean_input.lua b/builtin/runtime/lean_input.lua index da24378..7b205d2 100644 --- a/builtin/runtime/lean_input.lua +++ b/builtin/runtime/lean_input.lua @@ -124,6 +124,10 @@ end -- TUI-plus-GPU configuration this project ships. local pending = {} +-- Expansions the chain consumer decided on but did NOT perform, keyed +-- the same way. See `run_deferred` below for why they wait. +local deferred = {} + local function frontend_id() local ok, id = pcall(function() return pmacs.frontend.id() end) if ok then return id end @@ -157,19 +161,38 @@ end -- Expansion -- --------------------------------------------------------------------- --- Replace the pending span with `symbol`, placing the point at --- `$CURSOR` if the symbol carries one. Returns the byte offset just --- past the replacement, or nil when the edit was rejected or altered. +-- Right-gravity translation of `pos` through the effective edit — +-- pair.lua's shape, for the same reason: the point sits AFTER the +-- replaced span (on the terminator, or on a closer pairing inserted) +-- and has to move with it. +local function translate(pos, estart, estop, einserted) + if pos < estart then return pos end + if pos > estop then return pos - (estop - estart) + einserted end + return estart + einserted +end + +-- Replace the pending span (leader + typed text) with `symbol`. -- --- ONE `buf:replace` for the whole expansion: one undo step, one CRDT --- op, one effective-edit verification. A rejection drops the pending --- state and does not retry, the same discipline as comment.lua's Q#CT5 --- and pair.lua. -local function expand(buf, p, symbol, span_end) +-- The span deliberately STOPS BEFORE the terminator. Including the +-- terminator would make the expansion and the terminator one edit, but +-- it would also swallow whatever auto-pairing did with that terminator +-- — and a pair character is a legal terminator (`\alp(`). One undo +-- restores the same text either way, because the terminator was its own +-- insert to begin with. +-- +-- ONE `buf:replace`: one undo step, one CRDT op, one effective-edit +-- verification. A rejection drops the pending state and does not retry, +-- the same discipline as comment.lua's Q#CT5 and pair.lua. +local function expand(buf, start, span_end, symbol) local cursor_at = symbol:find(CURSOR, 1, true) local text = cursor_at and (symbol:gsub("%$CURSOR", "", 1)) or symbol - local start = p.start_offset + -- The context to compare against AFTER the edit. A buffer intercept + -- may switch window or buffer while the replace runs; the point in + -- whatever it switched to is not ours to move. + local win0 = pmacs.window.current() + local point0 = ed.cursor() + local ok, estart, estop, einserted = pcall(function() return buf:replace(start, span_end, text) end) @@ -188,7 +211,17 @@ local function expand(buf, p, symbol, span_end) -- the new end. Every later self-insert is then silently rejected and -- the editor looks dead. There is no daemon re-grounding that covers -- this; that only holds for an edit that lands at the cursor. - ed.goto_byte(cursor_at and (start + cursor_at - 1) or (start + #text)) + -- + -- Context-guarded exactly as pair.lua's `repair_cursor` is: if the + -- intercept switched us elsewhere, `goto_byte` would move the point + -- of a buffer that has nothing to do with this expansion. + if pmacs.window.current() == win0 and pmacs.window.buffer() == buf then + if cursor_at then + ed.goto_byte(start + cursor_at - 1) + else + ed.goto_byte(translate(point0, estart, estop, einserted)) + end + end return start + #text end @@ -245,6 +278,15 @@ local function on_typed_edit(rec) pending[fid] = nil return false end + -- ...and on a source edit whose context is no longer current. The + -- buffer and window matching is not enough: a redefined self-insert + -- can insert the character and THEN move the point, and expanding + -- over a span the user has left teleports them back into it. Pairing + -- makes the same three-part check for the same reason. + if ed.cursor() ~= rec.post_cursor then + pending[fid] = nil + return false + end local revision do @@ -287,55 +329,114 @@ local function on_typed_edit(rec) p.text = extended p.expected_revision = revision if eager[extended] then - local span_end = p.start_offset + 1 + #extended pending[fid] = nil - expand(buf, p, best[extended].symbol, span_end) + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = extended, + symbol = best[extended].symbol, + re_arm = false, + } end -- Claimed either way: an extension that has not yet completed must - -- NOT reach auto-pairing (`\[` in `\[[]]`). + -- NOT reach auto-pairing (`\[` in `\[[]]`), and a completing one is + -- part of the abbreviation, not a character pairing should react to. return true end - -- `ch` does not extend the abbreviation. Expand what is pending - -- FIRST, then let `ch` stand as ordinary text — the terminator is - -- retained, not consumed, and it sits inside the replaced span so the - -- whole thing is one undo step. + -- `ch` does not extend the abbreviation: it TERMINATES it, and a + -- terminator is an ordinary character that auto-pairing is entitled + -- to react to (`\alp(` must give `α()`). So the expansion is + -- DEFERRED to the subscriber below and this returns false, leaving + -- pairing a record whose offsets still describe the buffer. + -- + -- Expanding here and returning false would not do: the replace makes + -- pairing's copy of the record stale, so pairing declines and the + -- closer is silently lost. Expanding here and returning true is + -- worse — it is what shipped in the first revision of this file, and + -- it makes every pair-character terminator silently unpaired. pending[fid] = nil - local hit = best[p.text] - local after - if hit and #p.text > 0 then - -- `span_end` covers the terminator: the leader, the pending text, - -- and `ch`, which has already landed. What replaces it is the - -- symbol followed by `ch` itself. - local span_end = p.start_offset + 1 + #p.text + #ch - after = expand(buf, p, hit.symbol .. ch, span_end) + if best[p.text] and #p.text > 0 then + deferred[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = p.start_offset, + text = p.text, + symbol = best[p.text].symbol, + -- A terminating `\` re-arms as a NEW leader at its own position + -- (`\al\to` → `∀→`). Upstream gets this from `processChange`, + -- where a finished abbreviation reports `isAffected = false` and + -- so does not suppress the new-leader branch. This is NOT the + -- `\\` case: there the pending text is empty, `\` EXTENDS, and + -- the result is one literal backslash with nothing left open. + re_arm = ch == LEADER, + } + elseif ch == LEADER then + -- Nothing to expand, but the leader still opens a fresh + -- abbreviation where it landed. + pending[fid] = { + buffer = rec.buffer, + window = rec.window, + start_offset = rec.effective_start, + text = "", + expected_revision = revision, + } + return true end - -- A terminating `\` re-arms as a NEW leader at its own position - -- (`\alpha\to` → `α→`). Upstream gets this from `processChange`, - -- where a finished abbreviation reports `isAffected = false` and so - -- does not suppress the new-leader branch. This is not the `\\` case: - -- there the pending text is empty, `\` EXTENDS, and the result is one - -- literal backslash with no pending state left open. - if ch == LEADER then - local start = after and (after - #ch) or rec.effective_start - local ok, rev = pcall(function() return buf:revision() end) - if ok then + return false +end + +-- The deferred expansion, on its own `buffer.after-edit` subscriber. +-- +-- It runs AFTER the whole typed-edit chain — this chunk loads after +-- typed_edit.lua, and hook callbacks run in registration order — so +-- auto-pairing has already reacted to the terminator by the time the +-- expansion rewrites the text in front of it. Pairing's closer lands +-- after the terminator, outside the replaced span, so it survives. +-- +-- It must also run BEFORE lsp.lua's subscriber (Q#AP7): that one +-- flushes `didChange` synchronously on the signature-trigger path, and +-- a server told about `\alp ` instead of `α ` stays wrong until the +-- next edit. This chunk loads before lsp.lua for exactly that reason. +-- +-- A claim by ANY chain consumer stops the chain but not this — which +-- is the point. Pairing claims the terminator it reacts to. +local function run_deferred() + local fid = frontend_id() + if fid == nil then return end + local d = deferred[fid] + deferred[fid] = nil + if not d then return end + + local buf = pmacs.window.buffer() + if not buf or buf ~= d.buffer or pmacs.window.current() ~= d.window then + return + end + + -- The span must still hold exactly what was typed into it. Pairing + -- only edits at the point, which is past this span, so in practice + -- this holds; a buffer intercept is not obliged to be so polite. + local span_end = d.start_offset + 1 + #d.text + local ok, actual = pcall(function() + return buf:slice(d.start_offset, span_end) + end) + if not ok or actual ~= LEADER .. d.text then return end + + local after = expand(buf, d.start_offset, span_end, d.symbol) + if after and d.re_arm then + local rev_ok, rev = pcall(function() return buf:revision() end) + if rev_ok then pending[fid] = { - buffer = rec.buffer, - window = rec.window, - start_offset = start, + buffer = d.buffer, + window = d.window, + start_offset = after, text = "", expected_revision = rev, } end - return true end - - -- Claimed only if an expansion actually happened. Otherwise `ch` is - -- an ordinary character in a Lean buffer and auto-pairing should see - -- it — `\zz` leaves `z` free to pair if it ever were a pair char. - return after ~= nil end -- Q#KR11's seam: a detached frontend's pending state must not outlive @@ -343,8 +444,11 @@ end -- life of the session. pmacs.hook.add("frontend.detached", function(fid) pending[fid] = nil + deferred[fid] = nil end) +pmacs.hook.add("buffer.after-edit", run_deferred) + -- `buffer.after-switch` fires with NO arguments, so it cannot say whose -- switch it was. The acting frontend is the one that produced the most -- recent dispatched input event, which is what `pmacs.frontend.id()` diff --git a/docs/active-work.md b/docs/active-work.md index 034b1fd..f931da1 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -175,7 +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 9**, approved. Stage +- Framing `docs/lean4-mode-framing.md` **revision 10** (round 10 = + 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), @@ -183,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, 25 tests), and one + `tests/lean_input_acceptance.rs` (new, 29 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. @@ -239,11 +240,31 @@ If it does not, stop and repair the remote/fetch configuration. | `buffer.after-switch` clears every frontend | 1 | | delete the `buffer.after-switch` subscriber | 1 | | `frontend.detached` purges every frontend | 1 | + | claim the terminator | 1 | + | expand inside the chain, then decline | 2 | + | drop the `cursor() == post_cursor` check | 1 | + | place the point without the context guard | 1 | + | load lean_input.lua after lsp.lua | 1 | Acceptance 45f bit by construction: without a registered window for the source frontend it ran six fan-outs with a nil record and proved nothing, because `handle_remote_crdt_op` arms nothing unless the source's active window displays the buffer. +- **Round 10 (review) found three defects, all about what happens + AROUND the expansion rather than about resolving an abbreviation.** A + pair character that TERMINATES an abbreviation never reached pairing + (`\alp(` gave `α(`): the first revision claimed the terminator, and + merely declining is not enough either, because the chain hands each + consumer a copy of the record made before any consumer ran — so + expanding inside the chain invalidates pairing's copy and the closer + is lost anyway (verified by mutation, not assumed). The expansion now + runs on **its own `buffer.after-edit` subscriber** after the chain, + with a span that stops before the terminator. That is a new instance + of Q#AP7, so it is now pinned with the sighelp fake server. + Post-insert point motion was also mistaken for a valid span (the + relevance check needs `cursor() == post_cursor`, as pairing's has + since #110), and cursor placement could move a buffer an intercept + had switched to. - 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 32b1a10..d1dc46b 100644 --- a/docs/agent-handoff.md +++ b/docs/agent-handoff.md @@ -132,7 +132,14 @@ commands, read `docs/active-work.md` immediately after this file. (branch `lean4-stage4b-input-method`, framing rev 9): a vendored 1,855-entry table generated from `leanprover/vscode-lean4@17d1d08` by `scripts/regen-lean-abbrev`, plus a consumer registered on the - Stage 4a chain at priority 50, ahead of pairing. Its durable facts: + Stage 4a chain at priority 50, ahead of pairing. **A consumer + cannot both edit and let a later consumer act on the same + keystroke**: the chain hands each consumer a copy of the record made + before any consumer ran, so an edit invalidates every copy still to + be used. The expansion therefore runs on a SECOND + `buffer.after-edit` subscriber after the chain — which is how a + pair character that terminates an abbreviation still pairs + (`\alp(` → `α()`). 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 72a83fd..482ad84 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: **9**. +Revision 1 — initial. Current revision: **10**. ### Round 1 (rev 1 → rev 2) @@ -535,6 +535,38 @@ The mechanism (Q#LN11, Q#LN21, Q#LN22) needed no change — these were errors in the examples chosen to pin it, which is why a simulation over the real data found them and four review rounds over the prose did not. +### Round 10 (rev 9 → rev 10) + +Review of the Stage 4b implementation. Three defects in the expander, +all of them about what happens AROUND the expansion rather than about +resolving an abbreviation, plus one stale count. + +1. **A pair character that terminates an abbreviation never reached + auto-pairing.** Q#LN22 already said the terminator is not claimed; + the implementation claimed it whenever an expansion succeeded, so + `\alp(` gave `α(`. Not claiming is necessary and not sufficient — + the chain hands each consumer a copy of the record made before any + consumer ran, so expanding inside the chain invalidates the copy + pairing is holding and the closer is lost anyway. Q#LN22 now + specifies the deferred subscriber and the span that stops before the + terminator; acceptance 45j pins all three failure modes. +2. **Post-insert point motion was mistaken for a valid pending span.** + The relevance check compared buffer and window but not + `ed.cursor() == rec.post_cursor`, so a redefined self-insert that + inserts and then moves the point still expanded — and teleported the + point back. Pairing has made this three-part check since #110. + Acceptance 45k. +3. **Cursor placement could move the wrong buffer.** A buffer intercept + may switch buffers during `buf:replace`; the unguarded `goto_byte` + afterwards moved the switched-to buffer's point. `repair_cursor` is + the precedent. Acceptance 45l. +4. **The coherence census contradicted itself** — nine settings in one + paragraph, eight three paragraphs below. + +Acceptance 45m was added with them: the expansion now runs on its own +`buffer.after-edit` subscriber, which is a new instance of Q#AP7 and +was unpinned. + ## 1. What ships Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The @@ -1718,8 +1750,9 @@ reconstruction of it: - A subsequent self-insert `c` is claimed iff at least one key has `text .. c` as a prefix; then `text = text .. c`. If it is also uniquely-and-completely matching (one of the 1,550), expand now. -- If no key extends `text .. c`, expand `text` **first**, then let `c` - land normally — the chain does *not* claim `c`. +- If no key extends `text .. c`, `c` TERMINATES the abbreviation: the + chain does *not* claim it, and the expansion of `text` is + **deferred** until after the chain has run (round 10; see below). - **A terminating `c` that is itself `\` is then reprocessed as a new leader**, opening a fresh pending abbreviation at its position. This is the rule acceptance 45d depends on (`\alpha\to` → `α→`) and rev 6 @@ -1733,6 +1766,37 @@ reconstruction of it: broken by source rank, unmatchable tail appended (`\alp7` → `α7`). - `$CURSOR` is stripped from the symbol and its index becomes the point. +**The expansion is deferred past the chain, and its span stops before +the terminator** (round 10). "Not claiming the terminator" is necessary +and not sufficient: a pair character is a legal terminator (`\alp(` must +give `α()`), and the chain hands every consumer a *copy* of the record +made before any consumer ran. So expanding inside the chain and then +declining leaves auto-pairing holding offsets the replace has already +invalidated — pairing declines and the closer is silently lost, which a +probe confirmed. Claiming the terminator instead suppresses pairing +outright. Neither is recoverable from inside the chain. + +The expander therefore records the pending expansion and performs it on +its **own `buffer.after-edit` subscriber**, registered after +typed_edit.lua's and before lsp.lua's. A claim by any consumer stops the +chain but not a separate subscriber — which is the point, since pairing +claims the terminator it reacts to. The replaced span covers the leader +and the typed text only; whatever pairing did lands after it and +survives untouched. One undo restores the same text either way, because +the terminator was always its own insert. + +Two guards this exposes, both of which pairing already carries: + +- The relevance check is **three-part**, not two: buffer, window, **and + `ed.cursor() == rec.post_cursor`**. A redefined self-insert can insert + the completing character and then move the point, and expanding over a + span the user has left teleports them back into it. +- Cursor placement after the replace is **context-guarded**. A buffer + intercept may switch window or buffer while `buf:replace` runs; an + unguarded `goto_byte` then moves the point of a buffer that has + nothing to do with the expansion. `pair.lua`'s `repair_cursor` is the + precedent. + **Ownership is per frontend, not per buffer** (§2.11). The key is `(pmacs.frontend.id(), rec.buffer)`, and the stored `window` must still match `rec.window` for the state to be usable — a frontend that moved @@ -2490,11 +2554,14 @@ criterion 46 requires to stay byte-identical. it assumed `\alpha` takes the finish path when `alpha` is in the 1,550-key eager set (round 9; see 41). - *Finish path.* `\alp` + space yields `α `: the space lands first - and the expansion runs in the following `buffer.after-edit`, so - the terminator is **retained**, not consumed, and it is inside the - replaced span. One undo restores `\alp ` — with its space, not - `\al`. Rev 6 wrote the post-undo text without the terminator, - which would be true only if the terminator were swallowed. + and the expansion runs later in the same `buffer.after-edit` + fan-out, so the terminator is **retained**, not consumed. It sits + OUTSIDE the replaced span, which covers only the leader and the + typed text (round 10) — the observable text and the post-undo + text are the same either way, because the terminator was its own + insert. One undo restores `\alp ` — with its space, not `\al`. + Rev 6 wrote the post-undo text without the terminator, which + would be true only if the terminator were swallowed. - *Eager path.* `\alpha` yields `α` with no terminator typed, and a following space is a **separate** edit. One undo removes the space; a second restores `\alpha`. Asserting the finish-path undo @@ -2598,6 +2665,33 @@ criterion 46 requires to stay byte-identical. `$CURSOR` more than once; - the resolution spot-set behaves: `alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`, and the tie cases from 45h. +45j. **A pair character that TERMINATES an abbreviation still pairs** + (round 10). `\alp(` yields `α()` with the point between the pair. + Bites three ways, all of which produce different wrong answers: + claiming the terminator gives `α(`; expanding inside the chain and + then declining also gives `α(`, because the replace invalidates the + record copy pairing is holding; and pairing running first gives + `\alp()` unexpanded. Criterion 40 is the same collision from the + other side, and passing it says nothing about this one. +45k. **The relevance check is three-part.** A redefined + `buffer.self-insert` that inserts the completing character and then + moves the point must not expand: `\alph` + `a` under such an + override leaves literal `\alpha` with the point where the command + put it. Bites against checking only buffer and window — the + expansion would otherwise teleport the point back into a span the + user has left. +45l. **Cursor placement is context-guarded.** A buffer intercept that + switches buffers during `buf:replace` must not have the + switched-to buffer's point moved. Bites against an unguarded + `goto_byte`, which translates the LEAN buffer's pre-edit point + through the LEAN buffer's edit and applies it to whatever is + ambient. +45m. **Q#AP7 for the deferred subscriber.** The expansion runs on a + second `buffer.after-edit` subscriber, so it inherits pairing's + flush-ordering obligation: no `didChange` may ever carry the + unexpanded text. Pinned with the `sighelp` fake server and `(` as + the trigger — the flush carrying the terminator carries `α()`. + Falsified by loading lean_input.lua after lsp.lua. 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. @@ -2752,7 +2846,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 9) +### 9.1 Coherence impact — stages 4a and 4b (rev 10) **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 01ee89e..9270f1b 100644 --- a/tests/lean_input_acceptance.rs +++ b/tests/lean_input_acceptance.rs @@ -8,10 +8,12 @@ use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; use pmacs::protocol::FrontendId; use pmacs::window::{FrontendView, Layout, Window, WindowId}; use std::path::PathBuf; use std::sync::atomic::{AtomicUsize, Ordering}; +use std::time::{Duration, Instant}; fn fresh_dir() -> PathBuf { static SEQ: AtomicUsize = AtomicUsize::new(0); @@ -49,6 +51,10 @@ fn text(s: &EditorState) -> String { String::from_utf8_lossy(&b.as_bytes()).into_owned() } +fn cursor(s: &EditorState) -> i64 { + eval(s, "return pmacs.editor.cursor()") +} + fn type_as(s: &mut EditorState, fid: FrontendId, chars: &str) { for ch in chars.chars() { s.dispatch_key(fid, key(KeyCode::Char(ch))); @@ -176,6 +182,33 @@ fn a_pending_abbreviation_is_never_corrupted_by_auto_pairing() { assert_eq!(text(&s), "⟦⟧", "the full key resolves"); } +#[test] +fn a_pair_character_that_terminates_an_abbreviation_still_pairs() { + // The other half of the collision, and the one the first revision + // of this file got wrong. `(` does not extend `alp`, so it + // TERMINATES — and a terminator is an ordinary character that + // pairing is entitled to react to. + // + // Claiming the terminator suppresses pairing entirely (`α(`). + // Expanding before declining is no better: the replace makes + // pairing's copy of the record stale, so pairing declines and the + // closer is silently lost. Only deferring the expansion past the + // chain gives both. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alp("); + assert_eq!( + text(&s), + "α()", + "the abbreviation expanded AND the terminator paired" + ); + assert_eq!( + cursor(&s), + 3, + "and the point sits between the pair — after α (2 bytes) and \ + the opener" + ); +} + #[test] fn a_pair_character_outside_a_pending_abbreviation_still_pairs() { // The other direction: claiming extensions must not disable pairing @@ -271,6 +304,93 @@ fn switching_buffers_clears_pending_state_eagerly() { ); } +#[test] +fn a_self_insert_that_moves_the_point_afterwards_does_not_expand() { + // Buffer and window matching is not enough. A redefined + // `buffer.self-insert` may insert the completing character and THEN + // move the point; expanding over a span the user has left teleports + // them back into it. Pairing makes the same three-part check + // (`ed.cursor() ~= rec.post_cursor`) for the same reason. + let (mut s, _f) = lean_editor(); + type_str(&mut s, "\\alph"); + exec( + &s, + r#" + pmacs.command.unregister("buffer.self-insert") + pmacs.command.define { + name = "buffer.self-insert", + description = "test override: insert, then move the point away", + fn = function(cp) + pmacs.editor.insert_char_over_region(cp) + pmacs.editor.goto_byte(0) + end, + } + "#, + ); + + type_str(&mut s, "a"); + assert_eq!( + text(&s), + "\\alpha", + "the record died with the point that left it — no expansion" + ); + assert_eq!(cursor(&s), 0, "and the point stayed where it was moved to"); +} + +#[test] +fn an_intercept_that_switches_buffers_does_not_move_the_other_points() { + // A buffer intercept may switch window or buffer while the replace + // runs. An unguarded `goto_byte` afterwards moves the point of + // whatever it switched TO — a buffer with nothing to do with this + // expansion. Pairing's `repair_cursor` guards the same way. + let (mut s, f) = lean_editor(); + let dir = fresh_dir(); + let other = dir.join("other.lean"); + std::fs::write(&other, "0123456789").unwrap(); + let od = other.display().to_string(); + let fd = f.display().to_string(); + + exec(&s, &format!("pmacs.buffer.find_or_open({od:?})")); + exec(&s, &format!("pmacs.buffer.find_or_open({fd:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + exec( + &s, + &format!( + r#" + _G.SWITCHED = false + pmacs.buffer.add_intercept(pmacs.window.buffer(), function(op) + if op.kind == "replace" and not _G.SWITCHED then + _G.SWITCHED = true + pmacs.buffer.find_or_open({od:?}) + end + return nil + end) + "# + ), + ); + + type_str(&mut s, "\\alpha"); + let switched: bool = eval(&s, "return _G.SWITCHED"); + assert!(switched, "the intercept must actually have fired"); + assert_eq!( + text(&s), + "0123456789", + "we are now in the buffer the intercept switched to" + ); + // Whatever point the switch left in that buffer, the expansion must + // not have moved it. Unguarded, `goto_byte` runs against the + // ambient buffer and translates the LEAN buffer's pre-edit point + // (6) through the LEAN buffer's replace, landing at 2 here — a + // number with no meaning in this buffer at all. + assert_eq!( + cursor(&s), + 0, + "its point is untouched — the expansion's cursor placement is \ + guarded on the window and buffer still being the ones it \ + edited" + ); +} + // --------------------------------------------------------------------------- // 44 / 45 — the setting and the language gate, both on the SOURCE buffer // --------------------------------------------------------------------------- @@ -566,6 +686,127 @@ fn the_vendored_table_is_self_consistent() { assert!(!to_eager, "`to` is extended by `top`, `to0`, `toa`, …"); } +// --------------------------------------------------------------------------- +// Q#AP7 for the deferred expansion: it must land before lsp.lua flushes +// --------------------------------------------------------------------------- + +#[test] +fn the_expansion_reaches_the_first_did_change() { + // The expansion runs on its OWN `buffer.after-edit` subscriber, + // after the typed-edit chain. That makes it a new instance of the + // Q#AP7 obligation pairing already carries: lsp.lua's subscriber + // flushes `didChange` SYNCHRONOUSLY on the signature-trigger path, + // and `(` is a trigger. A server told about `\alp(` instead of + // `α()` stays wrong until the next edit — diagnostics, semantic + // tokens and inlay hints all frozen at stale byte positions. + // + // Falsified by loading lean_input.lua after lsp.lua in + // `src/editor.rs`: the expansion would then arrive in the SECOND + // didChange, or not at all. + let dir = fresh_dir(); + let sink = dir.join("changes.jsonl"); + let sink_disp = sink.display().to_string(); + let fake = env!("CARGO_BIN_EXE_pmacs_fake_lsp").to_owned(); + + let f = dir.join("a.lean"); + std::fs::write(&f, "").unwrap(); + 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.lean4 = {{ + command = '{fake}', + env = {{ + PMACS_FAKE_LSP_MODE = 'sighelp', + PMACS_FAKE_LSP_CHANGE_SINK = '{sink_disp}', + }}, + }}" + ), + ); + + 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, "\\alp("); + assert_eq!(text(&s), "α()", "precondition: the expansion happened"); + + // Wait for the flush that carries the `(` keystroke. Earlier + // keystrokes have already produced their own didChanges, so + // `changes[0]` is NOT the one under test — asserting on it compares + // against `\al` and fails for the wrong reason. + 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.iter().any(|t| t.contains('α')) { + break c; + } + assert!( + Instant::now() < deadline, + "no didChange carrying the expansion reached the fake server; got {:?}", + did_change_texts(&sink) + ); + std::thread::sleep(Duration::from_millis(10)); + }; + assert!( + !changes.iter().any(|t| t == "\\alp("), + "no didChange may ever carry the UNEXPANDED text — one would mean lsp.lua flushed before the deferred expansion ran (Q#AP7). Got {changes:?}" + ); + assert_eq!( + changes.last().map(String::as_str), + Some("α()"), + "the flush that carries the terminator carries the expansion and pairing's closer with it" + ); +} + +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() +} + // --------------------------------------------------------------------------- // 45i — pending state is per frontend // --------------------------------------------------------------------------- From 0d7ec7e3a6c1384e6d95b68456c8290add4e92fc Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 17:00:58 -0400 Subject: [PATCH 3/4] 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 From d1bff6ac30869978db6cf47d7ca02f4cb10b1be8 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 26 Jul 2026 17:15:24 -0400 Subject: [PATCH 4/4] fix(lean4): count fan-outs where a claim cannot skip the count MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 11 put the nesting count 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 a record the replace had invalidated. `\alp(` gave `α(` again. The count now comes from a no-op consumer registered 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. The other plausible home does not work and the comment now says why: a subscriber registered beside `run_deferred` is too late, because the whole nested fan-out completes inside the OUTER chain's subscriber, before either of them runs. Acceptance 45o pins the short-circuit path — a consumer at 25 that claims when the record is nil, so the nested pass never reaches the expander. 45n passes against this bug, which is why both exist. Counting in the expander fails 45o and nothing else. Framing rev 12 also names the shape rounds 10–12 share: each fix was correct about the failure it was shown and wrong about the boundary of the mechanism it leaned on — 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. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B --- builtin/runtime/lean_input.lua | 41 +++++++++++++++++------ docs/active-work.md | 24 ++++++++++++-- docs/agent-handoff.md | 6 +++- docs/lean4-mode-framing.md | 58 +++++++++++++++++++++++++++++---- tests/lean_input_acceptance.rs | 59 ++++++++++++++++++++++++++++++++++ 5 files changed, 168 insertions(+), 20 deletions(-) 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