docs(lean4): rev 6 — re-scout Stage 4 and split it into 4a and 4b
Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against main
@ d400f30 produced six findings that change the plan and three that
confirm it. The pmacs-side facts were verified in a worktree at that
commit; the upstream facts by reading leanprover/vscode-lean4 @ 17d1d08.
The split: Stage 4's risk column read "refactors pair.lua's provenance
read" — every language's auto-pairing — for a stage the prose called the
Lean input method, which is exactly the rule §4 states and exactly what
round 4 found for Stage 3. Rev 5 had noticed the shape and answered it
with a commit boundary; a commit boundary is not a review boundary.
Stage 4a is now the typed-edit consumer chain (substrate, no Lean) and
4b the input method.
Rev 5's expansion semantics were wrong in three ways. Resolution is the
shortest key having the input as a prefix (\al yields ∀ from `all`, not
`alpha`); there is no terminator list at all ('+ ' is a key, so space
extends after \+; '\' is a key, so \\ yields \); and an unmatchable tail
is appended rather than dropped (\alp7 yields α7).
Three further findings. There is no cursor-motion hook, so acceptance 43
as written was not buildable and abandonment is lazy. dispatch_key is
only half of 4b's production path — \ and the letters are not excluded
from the optimistic classifier, and that producer is crdt-gated, so a
crdt-gated integration test is dark in CI and dark in the gate list. And
the whole expansion has cross-peer-degraded undo, a wider bite than
Q#LN6's three bracket pairs; set_round_trip_input would fix it and is
rejected with reasons.
New decisions Q#LN21 (undo degradation) and Q#LN22 (the state machine);
Q#LN10 and Q#LN11 rewritten; §2.11 records the upstream algorithm; §9.1
states the coherence impact for both stages. Acceptance keeps its
existing numbers and adds letter suffixes on both sides of the split.
Citation sweep per COHERENCE §25: five live citations moved in the 50
commits since rev 5.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B
This commit is contained in:
parent
d400f30c06
commit
3b54c78494
|
|
@ -14,11 +14,13 @@ backlog.
|
|||
machine-local: `origin` may name this canonical URL, a release mirror,
|
||||
or something else, and therefore has no authority by name alone.
|
||||
- Canonical base at this snapshot:
|
||||
`githubsucks/main` @ `d152120` (the bottom-panel landed-doc refresh #156
|
||||
atop the inline-math slice #158, dired Stage 1 #165, the GPU terminal
|
||||
input fix #166, Lean 4 Stage 2 #161, the dired framing #164,
|
||||
COHERENCE.md #163, find-file #162, Lean 4 Stage 1 #160, and the minimap
|
||||
blank-slab fix #159; protocol v20).
|
||||
`githubsucks/main` @ `d400f30` (Lean 4 Stage 3b #170 atop Stage 3a
|
||||
#167, the bottom-panel landed-doc refresh #156, the inline-math slice
|
||||
#158, dired Stage 1 #165, the GPU terminal input fix #166, Lean 4
|
||||
Stage 2 #161, the dired framing #164, COHERENCE.md #163, find-file
|
||||
#162, Lean 4 Stage 1 #160, and the minimap blank-slab fix #159;
|
||||
protocol v20). The previous snapshot named `d152120`; the recovery
|
||||
check below accepts it or anything newer.
|
||||
- On the transfer source, `origin/main` named a release mirror at
|
||||
`d3fa632` and lagged badly. On the current destination, `origin` names
|
||||
the canonical URL. This difference is why all recovery begins by
|
||||
|
|
@ -55,7 +57,7 @@ git status --short --branch
|
|||
The `git log` command must expose `d152120` or a newer intentional main.
|
||||
If it does not, stop and repair the remote/fetch configuration.
|
||||
|
||||
## Lean 4 lane (Arc 8) — Stages 1+2 MERGED; 3a IN REVIEW (#167); 3b STACKED
|
||||
## Lean 4 lane (Arc 8) — Stages 1, 2, 3a, 3b MERGED; Stage 4 IN FRAMING
|
||||
|
||||
- Stage 1 **merged as #160** (`main` @ `0827dd1`, 2026-07-25, one review
|
||||
round, all twelve checks green). Branch `githubsucks/lean4-stage1`
|
||||
|
|
@ -189,7 +191,7 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
suites**; `git diff --check` clean. The sweep needs an isolated
|
||||
`XDG_CONFIG_HOME` and `-- --skip basedpyright`.
|
||||
|
||||
### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` (branch `lean4-stage3a-seams`)
|
||||
### Stage 3a — dispatch seams + `pmacs.fs.canonicalize` — MERGED #167 (`main` @ `6f348c9`)
|
||||
|
||||
- Worktree `../pmacs-lean-stage3`, branched off `githubsucks/main` @
|
||||
`46a1b8f`. Carries framing **rev 5** (the Stage 3 split) as its first
|
||||
|
|
@ -253,7 +255,7 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
`#[cfg(unix)]` is NOT sufficient for such a fixture —
|
||||
`#[cfg(target_os = "linux")]` is. Cost one red CI round to learn.
|
||||
|
||||
### Stage 3b — the Lean language server (branch `lean4-stage3b-server`)
|
||||
### Stage 3b — the Lean language server — MERGED #170 (`main` @ `d400f30`)
|
||||
|
||||
- Same worktree `../pmacs-lean-stage3`, **branched off
|
||||
`lean4-stage3a-seams`, not off `main`** — 3b consumes 3a's response
|
||||
|
|
@ -463,6 +465,61 @@ If it does not, stop and repair the remote/fetch configuration.
|
|||
describes the pushed tree; recording it late is the #161 fmt-blocker
|
||||
error in a slower form.)
|
||||
|
||||
### Stage 4 — framing rev 6, split into 4a/4b (branch `lean4-stage4a-typed-edit-chain`)
|
||||
|
||||
- Stages 3a and 3b **merged as #167** (`main` @ `6f348c9`) and **#170**
|
||||
(`main` @ `d400f30`), 2026-07-26. Both were integrated against a main
|
||||
that had advanced 50 commits mid-review; the only conflict either time
|
||||
was this ledger's own lane headings, resolved by keeping both sides.
|
||||
- Worktree `../pmacs-lean-stage4`, branched off `main` @ `d400f30`.
|
||||
Framing-only so far: `docs/lean4-mode-framing.md` **revision 6**. No
|
||||
code. Awaiting user approval before implementation, per the workflow.
|
||||
- **Round 5 re-scout split Stage 4 into 4a (substrate) and 4b (Lean).**
|
||||
4a is the typed-edit consumer chain — `builtin/runtime/typed_edit.lua`
|
||||
plus `pair.lua` re-expressed as one registered consumer, no behavior
|
||||
change. 4b is the input method. The split is forced by §4's own rule,
|
||||
which Stage 4's risk column ("refactors `pair.lua`'s provenance read")
|
||||
broke while the prose called the stage Lean-only.
|
||||
- **This is the SECOND consecutive re-scout to find that rule broken**
|
||||
(round 4 found it for Stage 3). Rev 5 had even noticed the shape and
|
||||
answered it with a commit boundary. **A commit boundary is not a review
|
||||
boundary.** Re-check every remaining stage against §4 at scout time;
|
||||
the rule is not self-enforcing.
|
||||
- **Rev 5's expansion semantics were wrong in three ways**, found by
|
||||
reading `leanprover/vscode-lean4` @ `17d1d08` rather than inferring
|
||||
from behavior. Resolution is *shortest key having the input as a
|
||||
prefix* (`\al` → `∀` from `all`, not `alpha`); there is **no
|
||||
terminator list** (`'+ '` is a key, so space extends after `\+`; `'\'`
|
||||
is a key, so `\\` → `\`); and an unmatchable tail is **appended**,
|
||||
not dropped (`\alp7` → `α7`).
|
||||
- **There is no cursor-motion hook**, so rev 5's acceptance 43 ("moving
|
||||
the cursor out abandons it") was not buildable. Abandonment is lazy —
|
||||
validated at the next typed edit — and the criterion now asserts what
|
||||
pmacs can actually detect. Upstream drives this off `changeSelections`;
|
||||
that seam does not exist here.
|
||||
- **`dispatch_key` is only half the production path for 4b.** The
|
||||
auto-pair suite gets away with dispatch-only because Q#AP1 removed the
|
||||
pair chars from the optimistic classifiers; `\` and the letters are
|
||||
NOT excluded, so on a CRDT frontend the optimistic producer is the real
|
||||
path. That producer is `#[cfg(feature = "crdt")]` and CI never enables
|
||||
`crdt`, and the gate list runs `--features crdt` only for `--lib` — a
|
||||
crdt-gated integration test is **dark twice over**.
|
||||
- The whole expansion has cross-peer-degraded undo (Q#LN21): six
|
||||
source-peer optimistic inserts replaced by one daemon-peer op.
|
||||
`set_round_trip_input` would fix it and is rejected — it also disables
|
||||
`dispatch_idle`, so RET stops inserting a newline.
|
||||
- Table facts re-derived at `17d1d08`: 1,855 entries, 36,861 bytes, all
|
||||
keys ASCII, **64** keys carry a `lean4` pair-set char, **305** keys are
|
||||
proper prefixes of another (so 1,550 expand eagerly), **26** values
|
||||
carry `$CURSOR`, **93** are multi-codepoint.
|
||||
- Citation sweep per COHERENCE §25: five live citations moved in the 50
|
||||
commits since rev 5 — `take_typed_edit` 12827→12990,
|
||||
`handle_server_requests` 1549→1815, `fs.stat` 93→133,
|
||||
`detect_buffer_language` 452→457, `send_request`/`send_notification`
|
||||
9342/9361→9507/9527.
|
||||
- Verification: none yet — the branch carries no code. `git diff --check`
|
||||
clean.
|
||||
|
||||
## Dired lane — Stage 0 MERGED; Stage 1 IN REVIEW (PR #165)
|
||||
|
||||
- Approved framing: `docs/dired-framing.md` **revision 6** — rev 5 is the
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ pmacs has no Lean support of any kind: `grep -rin lean` over `*.rs`,
|
|||
plain buffer — no grammar, no major mode, no comment syntax, no pair set,
|
||||
no server.
|
||||
|
||||
This lane closes that in eight stages. Stage boundaries are drawn where
|
||||
This lane closes that in nine stages. Stage boundaries are drawn where
|
||||
the *substrate* changes, not where the feature list does — see §4.
|
||||
§9 states the lane's coherence impact per `COHERENCE.md` §20.
|
||||
|
||||
|
|
@ -21,11 +21,12 @@ the *substrate* changes, not where the feature list does — see §4.
|
|||
#144 (LaTeX), #146 (HTML+CSS). Stage 1 is that pattern almost exactly.
|
||||
- Stages 2 and 4–6 are **not** that pattern, and none should be mistaken
|
||||
for a one-liner. Stage 2 changes `ensure_server`, shared by every LSP
|
||||
language. Stage 4 builds the editor's first input method. Stage 5 is the
|
||||
language. Stage 4a changes how typed-character provenance is consumed
|
||||
and Stage 4b builds the editor's first input method. Stage 5 is the
|
||||
first consumer of a non-standard LSP method family. Stage 6 adds a
|
||||
severity-routing policy to `LspServerSpec`.
|
||||
- The user's stated north star is **matching or exceeding what VS Code
|
||||
does with Lean**. §5's bet 6 scores honestly how close the eight stages get
|
||||
does with Lean**. §5's bet 6 scores honestly how close the nine stages get
|
||||
and names precisely what is still missing.
|
||||
|
||||
Parallel-safety: Stage 1 touches `Cargo.toml`, `src/syntax.rs`,
|
||||
|
|
@ -283,10 +284,131 @@ rather than a bare root), `ensure_server` 527 → **610**,
|
|||
pre-#161 line numbers inside Q#LN15 are left as written: that stage has
|
||||
landed and its citations are historical record, not navigation.
|
||||
|
||||
### Round 5 (rev 5 → rev 6) — Stage 4 re-scout and split
|
||||
|
||||
Stages 3a and 3b landed (#167, #170). Re-scouting Stage 4 against `main`
|
||||
@ `d400f30` produced **six findings that change the plan** and three
|
||||
that confirm it. The pmacs-side facts were verified in a worktree at
|
||||
that commit; the upstream facts were verified by downloading and reading
|
||||
`leanprover/vscode-lean4` at commit `17d1d08` (2026-05-29) — the
|
||||
algorithm, not its documentation, since the `lean4-unicode-input`
|
||||
package ships no README.
|
||||
|
||||
1. **Stage 4 violated this document's own splitting rule — the same way
|
||||
Stage 3 did.** §4 says "no PR in this arc mixes a cross-cutting
|
||||
substrate change with Lean feature content," and §4's own risk column
|
||||
for Stage 4 read *"refactors `pair.lua`'s provenance read."*
|
||||
`pair.lua` is every language's auto-pairing; the refactor is
|
||||
cross-cutting substrate by exactly the test that split out stages 2
|
||||
and 3a. Rev 5 already conceded the shape without acting on it —
|
||||
Q#LN10 said the refactor "lands *first*, as its own commit with no
|
||||
behavior change, so a regression bisects cleanly." A commit boundary
|
||||
is not a review boundary. **Stage 4 is now 4a (the typed-edit
|
||||
consumer chain, no Lean) and 4b (the input method).** Confirmed
|
||||
`pair.lua:226` is still the **only** production `take_typed_edit`
|
||||
caller; the other eight call sites are all in
|
||||
`tests/auto_pair_acceptance.rs`.
|
||||
2. **The expansion semantics in rev 5's Q#LN10 were wrong in three
|
||||
ways.** Reading `AbbreviationProvider.ts` and `TrackedAbbreviation.ts`
|
||||
rather than inferring from behavior:
|
||||
- Rev 5 said expansion fires on "a unique complete match that no
|
||||
longer key extends." Upstream's rule is
|
||||
`findSymbolsByAbbreviationPrefix(abbrev)[0]` — the symbol of the
|
||||
**shortest key having `abbrev` as a prefix**. `\alp` + space is not
|
||||
a failure; it yields `α`, because `alpha` is the shortest key
|
||||
starting with `alp`. Verified against the table: `\al` → `∀`, from
|
||||
`all`, not from `alpha`.
|
||||
- Rev 5 named "an explicit terminator (space, tab, RET, or a second
|
||||
`\`)." **There is no terminator list upstream.** A character
|
||||
terminates iff extending the pending key by it leaves zero prefix
|
||||
matches. Space usually does — but `'+ '` **is a key** (one of
|
||||
1,855), so after `\+` a space extends rather than terminates. And a
|
||||
second `\` is not a terminator either: `'\'` is a key mapping to
|
||||
`\`, so `\\` extends, matches uniquely, and expands to a single
|
||||
backslash. It terminates only when the pending key is non-empty and
|
||||
no key extends it.
|
||||
- Rev 5 did not carry the suffix rule at all. When no key has
|
||||
`abbrev` as a prefix, upstream recurses on `abbrev` minus its last
|
||||
character and **appends the leftover**: `\alp7` → `α7`. Dropping
|
||||
this makes a large class of real input silently unexpandable.
|
||||
3. **There is no cursor-motion hook, so acceptance 43 as written cannot
|
||||
be built.** The Rust core fires exactly eight named hooks
|
||||
(`builtin/hooks/default.lua`): `buffer.before-save`,
|
||||
`buffer.after-load`, `buffer.after-edit`, `buffer.after-switch`,
|
||||
`buffer.after-save`, `editor.before-quit`, `frontend.detached`,
|
||||
`process.after-tick`. Upstream drives abandonment off
|
||||
`changeSelections`, a seam pmacs does not have. Abandonment must
|
||||
therefore be **lazy** — validated at the next typed edit against the
|
||||
pending region — which changes what acceptance 43 can assert. Q#LN22
|
||||
states the state machine this forces.
|
||||
4. **`dispatch_key` is only half of Stage 4b's production path.** Rev 5
|
||||
inherited the auto-pairing suite's dispatch-driven harness without
|
||||
noticing why that harness is sufficient *there*: Q#AP1 removed the
|
||||
pair characters from both optimistic classifiers, so for pair chars
|
||||
dispatch **is** production. `\` and the ASCII letters are not
|
||||
excluded — `classify_key` returns `Insert(c)` for them
|
||||
(`src/optimistic.rs:144`: `Char(c) if !c.is_control() &&
|
||||
!is_builtin_pair_char(c)`), so on a CRDT frontend an abbreviation is
|
||||
typed entirely through the *optimistic* producer, which arms the same
|
||||
record from `handle_remote_crdt_op` (`src/daemon.rs:3965` pins the
|
||||
classification). A dispatch-only Stage 4b suite would pin the path
|
||||
real users do not take. The trap underneath: that producer is
|
||||
`#[cfg(feature = "crdt")]`, and CI never enables `crdt` — so a
|
||||
crdt-gated integration test is dark twice over, since the required
|
||||
gate list runs `--features crdt` only for `--lib`. Q#LN22 and §7 say
|
||||
what to do about it instead of discovering it in review.
|
||||
5. **The whole expansion has cross-peer-degraded undo, and it is a
|
||||
larger bite than `⟨⟩`'s.** Q#LN6 already accepts this for three
|
||||
bracket pairs. But there the mismatch is one optimistic opener
|
||||
against one daemon-peer closer; here the user's `\alpha` is six
|
||||
source-peer optimistic inserts and the expansion is a single
|
||||
daemon-peer `replace` **over all six**. Q#LN21 takes the decision —
|
||||
including why `pmacs.buffer.set_round_trip_input`, which already
|
||||
exists and would fix it, is the wrong instrument.
|
||||
6. **The table's shape is sharper than "1,855 entries."** Re-counted at
|
||||
`17d1d08`: 1,855 entries, all `string → string`, **all keys ASCII**,
|
||||
longest key 25 characters, 36,861 bytes of JSON. **64** keys contain
|
||||
a `lean4` pair-set character (rev 5's number, reproduced exactly).
|
||||
Three numbers rev 5 did not have and the algorithm needs: **305**
|
||||
keys are proper prefixes of another key (so 1,550 are eager-expandable
|
||||
on uniqueness and 305 are not), **26** values carry `$CURSOR` (not
|
||||
just `\<>`), and **93** values are multi-codepoint. Two values contain
|
||||
a backslash — `n` → `\n` and `setminus` → `\` — which is why upstream
|
||||
needs a `doNotTrackNewAbbr` guard and why §2.11 records that pmacs
|
||||
does not.
|
||||
|
||||
Confirmations, recorded because each was load-bearing and unverified:
|
||||
|
||||
7. **`take_typed_edit`'s one-shot contract is unchanged**
|
||||
(`src/editor_core.rs:4047`): per-frontend, cleared by the producer
|
||||
when the fan-out returns, nil to a nested manual `hook.run`. The
|
||||
hazard rev 5 built Q#LN10 around is real and still the reason 4a
|
||||
exists.
|
||||
8. **Load order still constrains the chain.** `pair.lua` loads at
|
||||
`src/editor.rs:430` and `lsp.lua` at `:436`, and Q#AP7's reason
|
||||
holds: `lsp.lua`'s `buffer.after-edit` callback synchronously flushes
|
||||
`didChange` on the signature-trigger path. An expansion that landed
|
||||
after that flush would send the server the unexpanded text.
|
||||
9. **Embedding the table needs no special machinery.** Every builtin
|
||||
runtime chunk is an `include_str!`, and `lsp.lua` is already 111 KB
|
||||
of the 414 KB total. A ~45 KB generated Lua table is within the
|
||||
existing practice, so Q#LN11 embeds it rather than inventing a
|
||||
lazy-load path.
|
||||
|
||||
Citation drift repaired per COHERENCE §25, on the same terms as round
|
||||
4's sweep. Five live citations moved in the 50 commits since rev 5:
|
||||
`take_typed_edit` 12827 → **12990**, `handle_server_requests` 1549 →
|
||||
**1815**, `fs.stat` 93 → **133**, `detect_buffer_language` 452 →
|
||||
**457**, and `send_request`/`send_notification` 9342/9361 →
|
||||
**9507**/**9527**. Left as written: the pre-#161 numbers inside Q#LN15
|
||||
and the revision-history entries above, which are historical record
|
||||
rather than navigation.
|
||||
|
||||
## 1. What ships
|
||||
|
||||
Eight stages, after round 4 split Stage 3. The north star is VS Code
|
||||
parity; the honest statement of where that lands is in §5, bet 6.
|
||||
Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
|
||||
north star is VS Code parity; the honest statement of where that lands
|
||||
is in §5, bet 6.
|
||||
|
||||
**Stage 1 — grammar, mode, and the editing table stakes.** `.lean` files
|
||||
highlight, carry a `lean4` major mode, and get comment-toggle and
|
||||
|
|
@ -315,10 +437,19 @@ on 3a's seam. Adds `textDocument/waitForDiagnostics`. Diagnostics, hover,
|
|||
completion, goto-definition, document symbols, and semantic tokens all
|
||||
arrive through the existing typed surfaces.
|
||||
|
||||
**Stage 4 — the Unicode input method.** Typing `\alpha` produces `α`,
|
||||
**Stage 4a — the typed-edit consumer chain.** Pure substrate, no Lean
|
||||
content, split from Stage 4 in round 5 for the reason stages 2 and 3a
|
||||
were: it changes machinery every language runs through. The one-shot
|
||||
`take_typed_edit()` record stops being auto-pairing's private property
|
||||
and becomes a small ordered chain that reads it once and offers it to
|
||||
registered consumers. `pair.lua` becomes the chain's first and only
|
||||
consumer, with no behavior change.
|
||||
|
||||
**Stage 4b — the Unicode input method.** Typing `\alpha` produces `α`,
|
||||
`\to` produces `→`, `\<>` produces `⟨⟩` with the point between them.
|
||||
1,855 abbreviations vendored from vscode-lean4. This is the stage that
|
||||
makes Lean actually typable in pmacs.
|
||||
1,855 abbreviations vendored from vscode-lean4, registered as a chain
|
||||
consumer ahead of auto-pairing. This is the stage that makes Lean
|
||||
actually typable in pmacs.
|
||||
|
||||
**Stage 5 — the goal view.** A `*lean-goal*` panel that renders
|
||||
`$/lean/plainGoal` at the point, refreshed on a debounced tick and on
|
||||
|
|
@ -405,7 +536,7 @@ injections_query }`. Adding a grammar is one entry plus one `Cargo.toml`
|
|||
line; the doc comment at `src/syntax.rs:756` says exactly this and it has
|
||||
held for every grammar since.
|
||||
|
||||
`builtin/runtime/syntax.lua:452` `detect_buffer_language` resolves, in
|
||||
`builtin/runtime/syntax.lua:457` `detect_buffer_language` resolves, in
|
||||
order: modeline → `pmacs.parse.language_for_path` (the grammar extension
|
||||
table) → `pmacs.lsp.filetypes[ext]` → `pmacs.parse.language_from_filename`
|
||||
→ shebang. A grammar entry claiming `lean` therefore resolves `.lean`
|
||||
|
|
@ -486,13 +617,13 @@ and pin it.*
|
|||
|
||||
- `pmacs.lsp` already exposes generic `send_request(id, method, params)`
|
||||
→ request id and `send_notification(id, method, params)`
|
||||
(`src/lua_bindings/mod.rs:9342`, `:9361`). Non-standard methods need no
|
||||
(`src/lua_bindings/mod.rs:9507`, `:9527`). Non-standard methods need no
|
||||
new Rust to *send*.
|
||||
- `LspEventKind` (`src/lsp.rs:264`) has generic `Notification { method,
|
||||
params }` and `Response { id, result, error, method }` variants. Unknown
|
||||
server methods are delivered, not dropped.
|
||||
- **But `events_take` has exactly one consumer**: `handle_server_requests`
|
||||
at `builtin/runtime/lsp.lua:1549`, driven off `pmacs._async.tick`. It
|
||||
at `builtin/runtime/lsp.lua:1815`, driven off `pmacs._async.tick`. It
|
||||
`take`s — a drain. Its `if/elseif` chain handles five `request` methods
|
||||
and `initialized`, and **ignores every `notification` and every
|
||||
`response`**. A second module calling `events_take` would steal events
|
||||
|
|
@ -556,7 +687,7 @@ character": subscribe to `buffer.after-edit`, gate on
|
|||
`ed.this_command() == "buffer.self-insert"` (`pair.lua:229`), then take the
|
||||
exact provenance record.
|
||||
|
||||
`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12827`) returns
|
||||
`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12990`) returns
|
||||
`{ buffer, window, codepoint, char, requested_start, requested_end,
|
||||
effective_start, effective_end, inserted_len, post_cursor, clean }` — or
|
||||
nil. Its doc comment is explicit:
|
||||
|
|
@ -570,7 +701,19 @@ it on every self-insert. A Lean abbreviation expander that independently
|
|||
calls `take_typed_edit()` in the same `buffer.after-edit` fan-out gets nil
|
||||
or steals it from auto-pairing, depending on hook order — and hook order is
|
||||
not a contract. This is the single load-bearing constraint on Stage 4 and
|
||||
the reason Stage 4 is its own PR rather than a rider on Stage 1.
|
||||
the reason Stage 4 is its own PR rather than a rider on Stage 1 — and,
|
||||
after round 5, the reason its substrate half is Stage 4a rather than a
|
||||
first commit on a Lean branch.
|
||||
|
||||
Re-verified at `d400f30`: `pair.lua:226` remains the **only** production
|
||||
caller. The eight other call sites in the tree are all in
|
||||
`tests/auto_pair_acceptance.rs`. So the chain Stage 4a introduces has
|
||||
exactly one consumer to migrate, which is what makes a no-behavior-change
|
||||
substrate PR possible at all.
|
||||
|
||||
Two producers arm the record, not one, and §2.11 is where that matters:
|
||||
the dispatch fallback and — under `#[cfg(feature = "crdt")]` — the
|
||||
optimistic CRDT arm reached from `handle_remote_crdt_op`.
|
||||
|
||||
Related, from `pair.lua:30`'s Q#AP1 note: only the nine built-in pair chars
|
||||
`()[]{}"'` and backtick are excluded from the frontends' optimistic
|
||||
|
|
@ -680,6 +823,78 @@ The publish path absorbs into the Rust store *and* still delivers the
|
|||
notification to `events_take`, so Lua can observe them; but suppressing
|
||||
them from the store needs a Rust-side policy, not a Lua filter. Q#LN18.
|
||||
|
||||
### 2.11 The upstream input method (external, verified by reading it)
|
||||
|
||||
Scouted 2026-07-26 against `leanprover/vscode-lean4` @ `17d1d08`,
|
||||
package `lean4-unicode-input`, files `AbbreviationProvider.ts`,
|
||||
`TrackedAbbreviation.ts`, `AbbreviationRewriter.ts`,
|
||||
`AbbreviationConfig.ts`, and `abbreviations.json`. The package ships no
|
||||
README, so the algorithm below is read off the source. Apache-2.0.
|
||||
|
||||
**Resolution.** `findSymbolsByAbbreviationPrefix(p)` collects every key
|
||||
having `p` as a prefix, sorts them by **key length ascending**, and maps
|
||||
to symbols. `getReplacementText(a)`:
|
||||
|
||||
1. If any key has `a` as a prefix, return the shortest such key's symbol.
|
||||
2. Otherwise recurse on `a` minus its last character; if that yields
|
||||
something, return it **with the dropped character appended**.
|
||||
3. Otherwise undefined — no expansion.
|
||||
|
||||
Verified against the table: `alpha` → `α`, `alp` → `α` (via `alpha`),
|
||||
`al` → `∀` (via `all`, *not* `alpha` — shortest wins, and this is
|
||||
surprising enough to be worth an acceptance criterion), `alp7` → `α7`
|
||||
via rule 2, `a` → `α` (`a` is itself a key, among 29 prefix matches).
|
||||
|
||||
**Tracking.** The leader `\` is inserted into the buffer like any other
|
||||
character, and the tracked range starts after it; the replaced range
|
||||
spans the leader inclusive (`abbreviationRange.moveKeepEnd(-1)`). So the
|
||||
buffer literally shows `\alpha` until expansion, then that whole span
|
||||
becomes `α`.
|
||||
|
||||
**Termination.** There is no terminator set. On each typed character
|
||||
`c`, if `findSymbolsByAbbreviationPrefix(a .. c)` is empty the
|
||||
abbreviation is marked `finished`, **`c` is not absorbed into it**, and
|
||||
the pending text expands before `c` lands. Otherwise `c` extends the
|
||||
key. Two consequences the obvious "space ends it" model gets wrong:
|
||||
|
||||
- `'+ '` is a key, so after `\+` a space **extends**. Space is a
|
||||
terminator by consequence, never by rule.
|
||||
- `'\'` is a key (→ `\`), so `\\` extends, is uniquely complete, and
|
||||
eagerly expands to one backslash. A second `\` terminates only when
|
||||
the pending key is non-empty and unextendable — at which point the
|
||||
rewriter starts a *new* tracked abbreviation on it.
|
||||
|
||||
**Eager expansion.** When `eagerReplacementEnabled`, an abbreviation
|
||||
expands the moment it is *unique and complete*: exactly one key has it
|
||||
as a prefix, and it is itself a key. 1,550 of the 1,855 keys qualify;
|
||||
the other 305 are proper prefixes of some other key and must wait for
|
||||
termination. `\to` is in the first group — it expands with no terminator
|
||||
typed, which is why acceptance 41 is meaningful and not a restatement of
|
||||
38.
|
||||
|
||||
**Cursor placement.** `$CURSOR` is stripped from the symbol and its
|
||||
index becomes the post-expansion point, applied only when the point sat
|
||||
at the end of the abbreviation. 26 values carry it.
|
||||
|
||||
**Abandonment.** Upstream expands on `changeSelections` — any tracked
|
||||
abbreviation the cursor has left. pmacs has no cursor-motion hook
|
||||
(round-5 finding 3), so this seam does not exist here and Q#LN22 makes
|
||||
abandonment lazy instead.
|
||||
|
||||
**The re-arm guard pmacs does not need.** `setminus` → `\` and `n` →
|
||||
`\n`, so an expansion can insert a backslash; upstream sets
|
||||
`doNotTrackNewAbbr` across the replace so that backslash does not open a
|
||||
new abbreviation. In pmacs the expansion is a programmatic `buf:replace`
|
||||
that arms no typed-edit record, so the chain sees nothing and cannot
|
||||
re-arm. The guard is unnecessary here **because of** the provenance
|
||||
contract, not by accident — and the acceptance must pin it, because a
|
||||
future consumer that inferred from buffer text rather than provenance
|
||||
would reintroduce the bug.
|
||||
|
||||
**What pmacs does not have to carry.** Multi-cursor. Upstream tracks a
|
||||
`Set<TrackedAbbreviation>` and sorts changes bottom-up for that reason;
|
||||
pmacs has one point, so one pending abbreviation per buffer.
|
||||
|
||||
## 3. Decisions
|
||||
|
||||
### Q#LN1 — Bundle `arborium-lean` 2.18; reject `tree-sitter-lean4`
|
||||
|
|
@ -911,7 +1126,7 @@ file's directory.
|
|||
|
||||
**How the walk tests for the marker — and why not the obvious way.**
|
||||
`pmacs.fs.stat` is asynchronous: it returns an awaitable handle
|
||||
(`builtin/runtime/fs.lua:93`) that only settles under `:await()` inside a
|
||||
(`builtin/runtime/fs.lua:133`) that only settles under `:await()` inside a
|
||||
coroutine. The resolver has no coroutine. It runs synchronously inside
|
||||
`ensure_server` ← `attach_buffer` ← the `buffer.after-load` hook, so
|
||||
awaiting is not merely slow there, it is unavailable — and blocking the
|
||||
|
|
@ -1102,86 +1317,192 @@ The binding is general, not Lean-shaped: it serves every future
|
|||
function-valued `root`, and it is what lets #161's doc comment stop
|
||||
warning about a footgun and start naming a fix.
|
||||
|
||||
### Q#LN10 — Stage 4 mechanism: one shared provenance read, not two
|
||||
### Q#LN10 — Stage 4a: one shared provenance read, not two
|
||||
|
||||
The hazard is §2.6 — `take_typed_edit()` is one-shot and `pair.lua`
|
||||
already consumes it.
|
||||
already consumes it. A second independent caller in the same
|
||||
`buffer.after-edit` fan-out gets nil or steals the record, depending on
|
||||
hook order, and hook order is not a contract.
|
||||
|
||||
Decision: **`pair.lua` stops being the sole consumer.** Extract the
|
||||
provenance read into a single `buffer.after-edit` subscriber owned by a
|
||||
small shared module, which takes the record once and passes it to an
|
||||
ordered list of typed-edit consumers (auto-pair, Lean abbreviation).
|
||||
Consumers return whether they handled the edit; the first that does stops
|
||||
the chain.
|
||||
small shared module — `builtin/runtime/typed_edit.lua`, loaded
|
||||
immediately before `pair.lua` — which takes the record once and offers
|
||||
it to registered consumers in a defined order. A consumer returns
|
||||
whether it **claimed** the edit; the first that claims stops the chain.
|
||||
|
||||
Two consequences worth stating up front:
|
||||
`pmacs.typed_edit.add_consumer { name = <string>, priority = <number>,
|
||||
fn = function(rec) ... end }`, lowest priority first, ties broken by
|
||||
registration order. Priority is an explicit number rather than
|
||||
load-order-implied because Q#LN22's collision makes ordering
|
||||
load-bearing, and rev 5's "the abbreviation consumer runs first" is a
|
||||
claim a reader must be able to check without reconstructing
|
||||
`src/editor.rs`'s include list.
|
||||
|
||||
- This touches `pair.lua`, which is load-bearing for auto-pairing
|
||||
acceptance. The full pairing suite is a required gate for Stage 4, and
|
||||
the refactor lands *first*, as its own commit with no behavior change,
|
||||
so a regression bisects cleanly.
|
||||
- Ordering is a contract, not an accident, and the collision is real:
|
||||
**64 of the 1,855 abbreviation keys contain a character in the proposed
|
||||
`lean4` pair set** — `\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`,
|
||||
`\{}` → `{$CURSOR}`. With pairing first, typing `\[` inserts `[]`
|
||||
with the point between, so the pending key is corrupted to `\[]` before
|
||||
the second `[` is ever typed and `\[[]]` becomes unreachable. The
|
||||
abbreviation consumer runs first.
|
||||
**Stage 4a ships this and nothing else.** Its whole content is:
|
||||
`typed_edit.lua`, `pair.lua` re-expressed as one registered consumer,
|
||||
and the `include_str!` line. Round 5's finding 1 is why this is a PR and
|
||||
not a first commit — `pair.lua` is every language's auto-pairing, and a
|
||||
reviewer looking at a Lean PR should not have to also review a rewrite
|
||||
of it.
|
||||
|
||||
(Rev 1 justified this with `\<>`, which was wrong: `<` is not in the
|
||||
pair set per Q#LN6, so that key is safe under either order.)
|
||||
**The no-behavior-change claim must be pinned, not asserted.** The full
|
||||
`tests/auto_pair_acceptance.rs` suite is a required gate for 4a and must
|
||||
pass **unmodified** — a suite edited to accommodate the refactor proves
|
||||
nothing (the recorded lesson: what a test suite pins is its assertions).
|
||||
Three assertions the existing suite already makes are the load-bearing
|
||||
ones, because they are what a chain could plausibly break: that a second
|
||||
`take_typed_edit()` in the same fan-out yields nil, that pairing still
|
||||
sees the exact record via `_capture_records`, and that the Q#AP7 ordering
|
||||
against `lsp.lua`'s `didChange` flush still holds.
|
||||
|
||||
**The contract that collision exposes:** the abbreviation consumer must
|
||||
claim a self-insert that **extends an open pending abbreviation**, not
|
||||
only one that completes an expansion. A consumer that only claims
|
||||
completed expansions hands every intermediate keystroke to auto-pairing,
|
||||
which is exactly how `\[` gets corrupted. "Claimed" here means the chain
|
||||
stops, not that an edit was made.
|
||||
**What 4a deliberately does not do.** It does not change the `all-must-
|
||||
succeed` contract, so a consumer that throws still fails the fan-out for
|
||||
everyone. The chain owner therefore `pcall`s each consumer and reports
|
||||
through `pmacs.editor.set_status`, matching `pair.lua`'s existing
|
||||
never-throw-from-after-edit discipline — this is behavior-preserving for
|
||||
pairing (which already never throws) and is the guardrail 4b needs.
|
||||
|
||||
Expansion semantics (matching vscode-lean4 and `lean4-input`):
|
||||
|
||||
- `\` opens a pending abbreviation, tracked per buffer with its start
|
||||
offset. Every subsequent self-insert that extends it is claimed. The
|
||||
pending state is abandoned on any non-self-insert command, buffer
|
||||
switch, or cursor move away from the pending region.
|
||||
- Expansion fires on a unique complete match that no longer key extends,
|
||||
or on an explicit terminator (space, tab, RET, or a second `\`).
|
||||
- The vendored table's `$CURSOR` placeholder becomes the point position
|
||||
after the replace — this is how `\<>` yields `⟨|⟩`.
|
||||
- The whole expansion is **one `buf:replace`** — one undo step, one CRDT
|
||||
op, one effective-edit verification. Same discipline as
|
||||
`comment.lua`'s Q#CT5.
|
||||
- Gated by `pmacs.config.define{ name = "lean.abbrev", type = "boolean",
|
||||
default = true, mutability = "live" }`, read against the *source* buffer
|
||||
of the typed edit — the `editing.auto-pair` precedent (`pair.lua:44`),
|
||||
including its round-2 correction to resolve `rec.buffer` rather than
|
||||
`pmacs.window.buffer()`.
|
||||
|
||||
### Q#LN11 — Stage 4 data: vendor the table, generated, attributed
|
||||
### Q#LN11 — Stage 4b data: vendor the table, generated, attributed
|
||||
|
||||
`abbreviations.json` in `leanprover/vscode-lean4` is a flat
|
||||
`string → string` object of **1,855 entries** (counted, not estimated),
|
||||
of which **64 contain a character in the `lean4` pair set** — the
|
||||
collision Q#LN10's ordering exists to handle. vscode-lean4 is Apache-2.0.
|
||||
`string → string` object of **1,855 entries**, verified at commit
|
||||
`17d1d08` (2026-05-29), 36,861 bytes, all keys ASCII, longest key 25
|
||||
characters. The counts the algorithm depends on, all re-derived from the
|
||||
file rather than estimated:
|
||||
|
||||
| Count | What it drives |
|
||||
|---|---|
|
||||
| 64 keys containing a `lean4` pair-set char | Q#LN22's ordering |
|
||||
| 305 keys that are proper prefixes of another | which keys can expand eagerly |
|
||||
| 1,550 keys uniquely-and-completely matching | the eager-expansion set |
|
||||
| 26 values containing `$CURSOR` | point placement |
|
||||
| 93 multi-codepoint values | the replace is not one-char-for-many |
|
||||
|
||||
vscode-lean4 is Apache-2.0.
|
||||
|
||||
Vendor it as a generated `builtin/runtime/lean_abbrev.lua` with a header
|
||||
recording source repo, commit, license, and the regeneration command —
|
||||
the `builtin/queries/latex/highlights.scm` precedent (#144) for
|
||||
third-party data, extended with provenance because this is a much larger
|
||||
artifact under a named license.
|
||||
recording source repo, commit, license, entry count, and the
|
||||
regeneration command — the `builtin/queries/latex/highlights.scm`
|
||||
precedent (#144) for third-party data, extended with provenance because
|
||||
this is a much larger artifact under a named license.
|
||||
|
||||
Not fetched at runtime, not a package-manager dependency: the input method
|
||||
must work offline and on first launch.
|
||||
Not fetched at runtime, not a package-manager dependency: the input
|
||||
method must work offline and on first launch.
|
||||
|
||||
**Upkeep is a documented manual process, not code.** There is no automatic
|
||||
sync and none is wanted — an editor that silently re-downloads its input
|
||||
method has a supply-chain problem, not a feature. The generator script
|
||||
lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit as its
|
||||
argument, and rewrites the file including its provenance header. The
|
||||
header records source commit, license, entry count, and the regeneration
|
||||
command, so the file is self-describing to whoever next touches it. A
|
||||
refresh is an ordinary PR with a visible diff — which is the point: the
|
||||
diff is the review.
|
||||
**Embedded, not lazily loaded.** ~45 KB of generated Lua joins the 414 KB
|
||||
of builtin runtime already compiled in by `include_str!`, of which
|
||||
`lsp.lua` alone is 111 KB. Inventing a lazy-load path for an 11% increase
|
||||
would be new machinery bought with no measurement, and the arithmetic is
|
||||
stated here so a reviewer can disagree with it on numbers.
|
||||
|
||||
**Upkeep is a documented manual process, not code.** There is no
|
||||
automatic sync and none is wanted — an editor that silently re-downloads
|
||||
its input method has a supply-chain problem, not a feature. The generator
|
||||
script lives at `scripts/regen-lean-abbrev`, takes a vscode-lean4 commit
|
||||
as its argument, and rewrites the file including its provenance header,
|
||||
so the file is self-describing to whoever next touches it. A refresh is
|
||||
an ordinary PR with a visible diff — which is the point: the diff is the
|
||||
review.
|
||||
|
||||
**The generator must reject a table it cannot faithfully encode.** Keys
|
||||
are ASCII today but nothing upstream promises that; a key containing a
|
||||
character the emitted Lua would have to escape, or a duplicate after
|
||||
normalization, aborts the regeneration rather than silently emitting a
|
||||
table that disagrees with its source. Same discipline as Q#LN20's
|
||||
refusal to hand back a lossy path.
|
||||
|
||||
### Q#LN21 — Stage 4b: the expansion's undo is cross-peer-degraded; ship it, name it
|
||||
|
||||
`classify_key` (`src/optimistic.rs:144`) returns `Insert(c)` for `\` and
|
||||
for every ASCII letter — only the nine built-in pair chars are excluded
|
||||
(Q#AP1). So on a CRDT frontend the user's `\alpha` arrives as six
|
||||
**source-peer** optimistic inserts, while the expansion is a single
|
||||
**daemon-peer** `buf:replace` spanning all six. Undo across that boundary
|
||||
is not chronologically arbitrated; this is the same defect Q#LN6 already
|
||||
accepts for `⟨⟩`, `⦃⦄`, `⟮⟯`, one order of magnitude wider.
|
||||
|
||||
Considered and rejected: `pmacs.buffer.set_round_trip_input(buf, true)`,
|
||||
which exists, is per-buffer, and would fix this exactly. Its six current
|
||||
callers are all read-only generated buffers — listview, compile, dired,
|
||||
terminal — and it does considerably more than disable optimistic insert:
|
||||
per `src/editor_core.rs:505`, `dispatch_idle` reports false, so RET
|
||||
reaches buffer-local bindings instead of inserting a newline. Turning it
|
||||
on for every ordinary editable Lean source file would trade a known undo
|
||||
degradation for an unknown behavior change across the whole editing
|
||||
surface, and would make Lean the one language whose typing has a
|
||||
different latency profile.
|
||||
|
||||
Also rejected: adding `\` to the always-round-trip set. It is
|
||||
frontend-side and language-blind, so this would tax LaTeX, C, shell, and
|
||||
every string literal in the editor to fix one language.
|
||||
|
||||
Decision: **accept the degradation, name it in the module comment, and
|
||||
do not paper over it.** The general fix is chronological cross-peer undo
|
||||
arbitration — already on the standing backlog, and the same fix Q#LN6
|
||||
points at. What Stage 4b owes is honesty about scope: this is not "a few
|
||||
brackets," it is every abbreviation the user types on a CRDT frontend.
|
||||
|
||||
### Q#LN22 — Stage 4b mechanism: lazy abandonment, explicit ordering
|
||||
|
||||
**Ordering.** The abbreviation consumer registers ahead of auto-pairing.
|
||||
The collision is real: 64 keys contain a `lean4` pair-set character —
|
||||
`\[[]]` → `⟦⟧`, `\(())` → `⸨⸩`, `\{{}}` → `⦃⦄`, `\{}` → `{$CURSOR}`.
|
||||
With pairing first, typing `\[` inserts `[]` with the point between, so
|
||||
the pending key is corrupted to `\[]` before the second `[` is typed and
|
||||
`\[[]]` becomes unreachable.
|
||||
|
||||
(Rev 1 justified this with `\<>`, which was wrong: `<` is not in the pair
|
||||
set per Q#LN6, so that key is safe under either order.)
|
||||
|
||||
**The contract the collision exposes:** the consumer must claim a
|
||||
self-insert that **extends an open pending abbreviation**, not only one
|
||||
that completes an expansion. A consumer that claims only completed
|
||||
expansions hands every intermediate keystroke to auto-pairing, which is
|
||||
exactly how `\[` gets corrupted. "Claimed" means the chain stops, not
|
||||
that an edit was made.
|
||||
|
||||
**State machine**, per §2.11's ground truth rather than rev 5's
|
||||
reconstruction of it:
|
||||
|
||||
- `\` typed in a `lean4` buffer opens a pending abbreviation: `{ buffer,
|
||||
start_offset, text = "" }`, one per buffer, keyed on `rec.buffer`.
|
||||
- A subsequent self-insert `c` is claimed iff at least one key has
|
||||
`text .. c` as a prefix; then `text = text .. c`. If it is also
|
||||
uniquely-and-completely matching (one of the 1,550), expand now.
|
||||
- If no key extends `text .. c`, expand `text` **first**, then let `c`
|
||||
land normally — the chain does *not* claim `c`.
|
||||
- Expansion resolves through §2.11's three-rule `getReplacementText`,
|
||||
including the suffix rule (`\alp7` → `α7`).
|
||||
- `$CURSOR` is stripped from the symbol and its index becomes the point.
|
||||
|
||||
**Abandonment is lazy, because there is no cursor-motion hook** (round-5
|
||||
finding 3). Pending state is validated at the next typed edit and
|
||||
discarded when any of these no longer holds: the record's buffer is the
|
||||
pending buffer; `rec.effective_start` equals `start_offset + 1 +
|
||||
#text` (the point is still at the end of the pending span); and the
|
||||
buffer's `revision()` advanced by exactly the pending edit. `buffer.
|
||||
after-switch` clears it eagerly since that hook *does* exist. The
|
||||
practical difference from upstream: a user who clicks away mid-`\alp`
|
||||
and types elsewhere gets the pending state dropped rather than expanded.
|
||||
Upstream expands it. **This is a deliberate divergence** — expanding
|
||||
into a region the user has left is the worse failure, and pmacs cannot
|
||||
detect the departure at the moment it happens.
|
||||
|
||||
**One `buf:replace`** for the whole expansion — one undo step, one CRDT
|
||||
op, one effective-edit verification, with the same
|
||||
rejected/altered-by-intercept reporting as `comment.lua`'s Q#CT5 and
|
||||
`pair.lua`. A rejection drops the pending state; it does not retry.
|
||||
|
||||
**Gate:** `pmacs.config.define{ name = "lean.abbrev", type = "boolean",
|
||||
default = true, mutability = "live" }`, read against the **source**
|
||||
buffer of the typed edit — the `editing.auto-pair` precedent
|
||||
(`pair.lua:46`), including its round-2 correction to resolve
|
||||
`rec.buffer` rather than `pmacs.window.buffer()`.
|
||||
|
||||
**Language gate:** the consumer opens no pending abbreviation outside a
|
||||
`lean4` buffer, resolved from `rec.buffer` for the same reason. `\` in a
|
||||
Rust buffer is an ordinary character and `\[` there still pairs.
|
||||
|
||||
### Q#LN12 — Stage 5 sends `$/lean/plainGoal` through a typed Rust request
|
||||
|
||||
|
|
@ -1418,13 +1739,14 @@ never lands.
|
|||
| 2 | multi-root server affinity | **`ensure_server`, shared by every language** | — |
|
||||
| 3a | notification/response seams + purge; `pmacs.fs.canonicalize` | **the shared event drain, run by every language** | — |
|
||||
| 3b | `lake serve` + probe/latch, Lake root, `waitForDiagnostics` | none — Lean-only files plus one config entry | 1, 2, 3a |
|
||||
| 4 | Unicode input method | **refactors `pair.lua`'s provenance read** | 1 |
|
||||
| 4a | typed-edit consumer chain | **refactors `pair.lua`'s provenance read, shared by every language** | — |
|
||||
| 4b | Unicode input method | none — Lean-only files plus one chain consumer | 1, 4a |
|
||||
| 5 | goal panel | new typed LSP request; panel adopter | 3a, 3b |
|
||||
| 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3b, 5 |
|
||||
| 7 | module hierarchy | listview adopter + one typed Rust request | 3a, 3b |
|
||||
|
||||
Four of the eight carry risk that is *not* about Lean — stages 1, 2, 3a,
|
||||
and 6 each change something every language touches. That is the
|
||||
Five of the nine carry risk that is *not* about Lean — stages 1, 2, 3a,
|
||||
4a, and 6 each change something every language touches. That is the
|
||||
organizing principle of the split: **no PR in this arc mixes a
|
||||
cross-cutting substrate change with Lean feature content.** A reviewer
|
||||
looking at Stage 2 sees only `ensure_server`; a reviewer looking at Stage
|
||||
|
|
@ -1436,6 +1758,16 @@ Lean-only. One generalization shipped as Stage 2; extracting the other as
|
|||
3a is what makes the claim true again. The rule is only worth writing
|
||||
down if it survives contact with a stage that is inconvenient to split.
|
||||
|
||||
Round 5 found the *same* rule broken again, by Stage 4, whose risk column
|
||||
read "refactors `pair.lua`'s provenance read" — every language's
|
||||
auto-pairing — for a stage described as the Lean input method. Rev 5 had
|
||||
noticed the shape and answered it with a commit boundary; a commit
|
||||
boundary is not a review boundary. Twice in two re-scouts is the
|
||||
interesting part: **this rule is not self-enforcing, and a stage only
|
||||
looks Lean-only until someone re-reads its own risk column.** Every
|
||||
remaining stage should be re-checked against it at scout time, not
|
||||
assumed.
|
||||
|
||||
Ordering notes:
|
||||
|
||||
- **Stage 2 has no Lean in it and could ship independently of this arc.**
|
||||
|
|
@ -1453,11 +1785,21 @@ Ordering notes:
|
|||
`builtin/runtime/lsp.lua`. Unlike stages 1 and 2, this pair is strictly
|
||||
sequential — recorded here, per the #126/#127 lesson, rather than
|
||||
discovered in a rebase.
|
||||
- **Stage 4 does not depend on stages 2, 3a, or 3b** and could run in
|
||||
parallel, but should not: both touch `lsp.lua`/`pair.lua`-adjacent
|
||||
runtime files, and the #126/#127 lesson is that parallel-safety
|
||||
requires the file split be agreed *before* either lane starts.
|
||||
Sequential is cheaper.
|
||||
- **Stage 4a depends on nothing in this arc** — not even Stage 1. It is
|
||||
a pure runtime-substrate change whose only content is `pair.lua` and a
|
||||
new module beside it, and it would be worth landing if the Lean arc
|
||||
were abandoned tomorrow, because "the typed-edit record has exactly
|
||||
one consumer forever" is not a property anyone chose.
|
||||
- **4a and 4b cannot run as sibling worktrees**, for the 3a/3b reason:
|
||||
4b's consumer is written against the registration API 4a adds. Strictly
|
||||
sequential, recorded before either starts.
|
||||
- **Stage 4b depends on stages 1 and 4a and on nothing else** — not on
|
||||
2, 3a, or 3b. The input method is useful with no language server at
|
||||
all, which is the honest ordering argument for putting it this early:
|
||||
a user with no Lean toolchain installed still gets a Lean editor that
|
||||
can type Lean. It could run in parallel with the 5/6/7 lane, but
|
||||
should not, per the #126/#127 lesson that parallel-safety requires the
|
||||
file split be agreed *before* either lane starts.
|
||||
- **Stage 6 depends on Stage 5** only for the read-only generated-buffer
|
||||
and panel machinery, which Stage 5 establishes. If Stage 5 slips, Stage
|
||||
6 can carry that machinery itself at the cost of duplicating it.
|
||||
|
|
@ -1496,7 +1838,22 @@ Stated so they can be scored, per house style.
|
|||
inside `buffer.after-edit` re-enters the hook in a way pairing does not
|
||||
already survive. Confidence: medium — pairing does the same thing, but
|
||||
over a single codepoint rather than a multi-byte span.
|
||||
6. **These eight stages reach rough VS Code parity for everything except
|
||||
5a. **Lazy abandonment is good enough without a cursor-motion hook**
|
||||
(rev 6, Q#LN22). Falsified if a user in normal editing hits a case
|
||||
where stale pending state produces a *wrong* expansion rather than a
|
||||
dropped one — the failure mode this design chooses. Confidence:
|
||||
medium-high, because every path that can invalidate the state either
|
||||
goes through `buffer.after-edit` (where it is checked) or through
|
||||
`buffer.after-switch` (where it is cleared), and the residual is a
|
||||
cursor move with no intervening edit, which the next typed edit
|
||||
catches by position. If it fails, the fix is a cursor-motion hook —
|
||||
substrate work with its own framing, not a patch to this stage.
|
||||
5b. **Stage 4a is behavior-preserving.** Falsified by any change to
|
||||
`tests/auto_pair_acceptance.rs` being needed to make it pass.
|
||||
Confidence: high, and cheap to score — it is a diff-level check, not
|
||||
a judgment call. This bet is stated separately from bet 5 because it
|
||||
is the one a reviewer can falsify in ten seconds.
|
||||
6. **These nine stages reach rough VS Code parity for everything except
|
||||
the interactive infoview.** Scored honestly rather than aspirationally.
|
||||
What lands: highlighting, goal view, Unicode input, diagnostics,
|
||||
hover, completion, goto-definition, symbols, semantic tokens, `#eval`
|
||||
|
|
@ -1528,10 +1885,26 @@ What remains deferred:
|
|||
- **GPU goal band** — blocked on bottom-panel Stage 2 (Q#LN14). The panel
|
||||
is grid-only until then.
|
||||
- **A `cursor.after-move` hook** — there is none (Q#LN13), so Stage 5
|
||||
polls off `process.after-tick`. A real motion hook would serve the goal
|
||||
view, `completion.lua`'s cursor-delta heuristic, and the outline/hover
|
||||
panels alike; it is substrate work that should not be invented inside a
|
||||
language lane.
|
||||
polls off `process.after-tick` and Stage 4b abandons pending
|
||||
abbreviations lazily rather than on departure (Q#LN22, round-5 finding
|
||||
3). A real motion hook would serve the goal view, the input method,
|
||||
`completion.lua`'s cursor-delta heuristic, and the outline/hover panels
|
||||
alike; it is substrate work that should not be invented inside a
|
||||
language lane. Two consumers in this arc now want it, which is worth
|
||||
recording as evidence for whoever frames it.
|
||||
- **Chronological cross-peer undo arbitration** — the general fix for
|
||||
Q#LN6's bracket pairs and Q#LN21's abbreviation expansions alike.
|
||||
Already on the standing backlog; named again here because Stage 4b
|
||||
widens the exposure from three pair characters to every abbreviation a
|
||||
user types on a CRDT frontend, which changes how often the existing
|
||||
defect is met without changing what it is.
|
||||
- **Per-buffer optimistic-apply policy** — the narrower thing Q#LN21
|
||||
actually wanted and did not build. `set_round_trip_input` is the only
|
||||
existing lever and it is too blunt (it also changes RET dispatch); a
|
||||
frontend-side, language-aware round-trip character set would fix the
|
||||
undo degradation for Lean without taxing every other language, and
|
||||
would retire Q#AP1's limitation too. Frontend + protocol work, so
|
||||
Q#LN14's no-protocol-change rule keeps it out of this arc entirely.
|
||||
- **LSP server reaping / LRU** — Q#LN15's per-root affinity makes
|
||||
unbounded `lake serve` growth possible. No editor caps this by default
|
||||
and pmacs will not either in this arc, but the policy question is now
|
||||
|
|
@ -1758,12 +2131,44 @@ revision take letter suffixes rather than displacing anything. Round 3's
|
|||
finding 4 was stale cross-references surviving a renumber; not
|
||||
renumbering is the cheaper way to not repeat it.
|
||||
|
||||
**Stage 4 — the Unicode input method**
|
||||
**Stage 4a — the typed-edit consumer chain**
|
||||
|
||||
38. `\alpha` + space yields `α`; the whole expansion is a single undo step.
|
||||
Criterion 46 keeps its number and moves here — it was always the
|
||||
substrate pin, filed under Stage 4 only because Stage 4 was one stage.
|
||||
Per the no-renumbering rule above, round 5's additions take letter
|
||||
suffixes on both sides of the split.
|
||||
|
||||
46. **Provenance-refactor pin:** the full `tests/auto_pair_acceptance.rs`
|
||||
suite passes **unmodified**. A suite edited to accommodate the
|
||||
refactor proves nothing; the diff for 4a must show zero lines
|
||||
changed in that file.
|
||||
46a. The chain reads the record exactly once: with two consumers
|
||||
registered, a `take_typed_edit()` from inside either observes nil,
|
||||
and both consumers receive the *same* record fields. Bites against a
|
||||
chain that re-takes per consumer (which would hand the second one
|
||||
nil in production and pass a single-consumer test).
|
||||
46b. Ordering is by declared priority, not registration order: two
|
||||
consumers registered low-priority-last still run
|
||||
low-priority-first. Bites against a chain that "works" only because
|
||||
`include_str!` order happens to agree with intent.
|
||||
46c. A claiming consumer stops the chain — a later consumer does not
|
||||
run — and a non-claiming one does not.
|
||||
46d. A consumer that throws is contained: the fan-out still succeeds,
|
||||
the other consumers still run, and the failure reports through
|
||||
`set_status`. Bites against the `all-must-succeed` contract taking
|
||||
the whole fan-out down with one bad consumer (Q#LN10).
|
||||
46e. **Q#AP7 ordering survives.** The existing `sighelp` fake-server
|
||||
test — pairing's closer must be in the buffer before `lsp.lua`
|
||||
flushes `didChange` — still holds with pairing behind the chain.
|
||||
Falsified by moving the chain's registration after `lsp.lua`'s.
|
||||
|
||||
**Stage 4b — the Unicode input method**
|
||||
|
||||
38. `\alpha` + space yields `α`; the whole expansion is a single undo
|
||||
step, and one undo restores `\alpha` rather than `\alph`.
|
||||
39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR`
|
||||
placeholder.
|
||||
40. **Pair-collision pin (Q#LN10).** `\[[]]` yields `⟦⟧`: each `[` is
|
||||
40. **Pair-collision pin (Q#LN22).** `\[[]]` yields `⟦⟧`: each `[` is
|
||||
claimed as an extension of the pending abbreviation, so auto-pairing
|
||||
never inserts a closing `]` into the pending key. Bites against an
|
||||
ordering where pairing runs first, and against a consumer that claims
|
||||
|
|
@ -1773,15 +2178,55 @@ renumbering is the cheaper way to not repeat it.
|
|||
41. `\to` yields `→` eagerly on uniqueness, with no terminator typed.
|
||||
42. A prefix with no match (`\zzzz` + space) is left as literal text; no
|
||||
edit is made.
|
||||
43. Moving the cursor out of a pending abbreviation abandons it.
|
||||
43. **Lazy abandonment (Q#LN22).** Because there is no cursor-motion
|
||||
hook, this asserts what pmacs can actually detect: after `\alp`, an
|
||||
explicit `goto_byte` elsewhere followed by typing `h` inserts a
|
||||
plain `h` and leaves the `\alp` text untouched — the pending state
|
||||
is dropped, not expanded. Plus: `buffer.after-switch` clears pending
|
||||
state eagerly. **Rev 5's version of this criterion was not
|
||||
buildable**; recorded so the change is visible rather than silent.
|
||||
44. `pmacs.config.set("lean.abbrev", false)` disables expansion; the
|
||||
setting is read against the typed edit's **source** buffer.
|
||||
45. Expansion does not fire in a non-`lean4` buffer — including that a
|
||||
pending abbreviation is never opened there, so `\[` in a Rust buffer
|
||||
still pairs normally.
|
||||
46. **Provenance-refactor pin:** the full auto-pairing acceptance suite
|
||||
passes unchanged, and a bite against the pre-refactor `pair.lua`
|
||||
confirms the shared-consumer commit is behavior-preserving.
|
||||
45a. **Shortest-key resolution (§2.11).** `\alp` + space yields `α`, and
|
||||
`\al` + space yields `∀` — from `all`, not `alpha`. The second is
|
||||
the one that bites: a "longest match" or "unique match only"
|
||||
implementation passes the first and fails this.
|
||||
45b. **Suffix rule.** `\alp7` + space yields `α7`. Bites against an
|
||||
implementation that drops unmatchable trailing characters or
|
||||
abandons the whole abbreviation.
|
||||
45c. **There is no terminator list.** `\+` followed by space extends
|
||||
rather than terminating, because `'+ '` is a key. Bites against any
|
||||
implementation with a hardcoded space/tab/RET terminator set — which
|
||||
is what rev 5 specified.
|
||||
45d. **`\\` yields a single `\`**, by extension-and-eager-match rather
|
||||
than by treating the second `\` as a terminator. And after a
|
||||
*non-empty* pending key, a second `\` does terminate and open a new
|
||||
abbreviation: `\alpha\to` + space yields `α→`.
|
||||
45e. **No re-arm through inserted text (§2.11).** `\setminus` + space
|
||||
yields a literal `\`, and typing an ordinary letter after it inserts
|
||||
that letter — the inserted backslash opens no pending abbreviation,
|
||||
because the expansion is a programmatic replace that arms no record.
|
||||
Bites against a future consumer that infers pending state from
|
||||
buffer text instead of provenance.
|
||||
45f. **Both producers, and the CI-darkness stated.** The dispatch path
|
||||
is pinned by the criteria above. The optimistic CRDT producer
|
||||
(round-5 finding 4) is pinned by a separate criterion driving
|
||||
`handle_remote_crdt_op`, which is `#[cfg(feature = "crdt")]` and
|
||||
therefore **dark in CI and dark in the required gate list**, since
|
||||
that list runs `--features crdt` only for `--lib`. The PR must
|
||||
either land that coverage as a `--lib` test where the gate reaches
|
||||
it, or state in its description that the optimistic path was
|
||||
verified only locally and name the command. Silence here is the
|
||||
failure mode — a green CI would otherwise read as covering the path
|
||||
most users take.
|
||||
45g. **Table integrity.** The generated `lean_abbrev.lua` round-trips:
|
||||
its entry count matches the header's declared count, and a spot set
|
||||
of entries (`alpha`, `to`, `<>`, `+ `, `\`, `n`, `setminus`) matches
|
||||
`abbreviations.json` byte-for-byte. Bites against a generator that
|
||||
silently drops or mangles keys (Q#LN11).
|
||||
|
||||
**Stage 5 — the goal view**
|
||||
|
||||
|
|
@ -1847,7 +2292,7 @@ renumbering is the cheaper way to not repeat it.
|
|||
it, with the extra success-gate §2.9 forces.
|
||||
- **#110 (auto-pairing)** — `take_typed_edit()` provenance, the fail-closed
|
||||
discipline on transformed source edits, and Q#AP1's optimistic-classifier
|
||||
limitation. Stage 4 is built on all three.
|
||||
limitation. Stage 4a generalizes the first; 4b is built on all three.
|
||||
- **#127 (config registry)** — `pmacs.config.define` and the
|
||||
source-buffer-resolution correction. Q#LN10's gate follows
|
||||
`editing.auto-pair` exactly.
|
||||
|
|
@ -1895,8 +2340,8 @@ alongside sixteen other languages — deliberately *not* the typed registry,
|
|||
because moving one language's entry there while the other sixteen stay
|
||||
put would fragment the surface rather than unify it. Migrating
|
||||
`pmacs.lsp.config` wholesale is a config-arc concern; this lane must not
|
||||
create a precedent that makes it harder. Stage 4's `lean.abbrev` gate is
|
||||
where this arc does enter the registry, and Q#LN10 already commits to the
|
||||
create a precedent that makes it harder. Stage 4b's `lean.abbrev` gate is
|
||||
where this arc does enter the registry, and Q#LN22 already commits to the
|
||||
`editing.auto-pair` shape.
|
||||
|
||||
**Background-work attribution (§9).** Three pieces of background work,
|
||||
|
|
@ -1928,3 +2373,59 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from
|
|||
#161 — surfacing the spawn failure itself. Each is a behavior change for
|
||||
languages other than Lean, and §4's rule is what keeps them out of a Lean
|
||||
PR.
|
||||
|
||||
### 9.1 Coherence impact — stages 4a and 4b (rev 6)
|
||||
|
||||
**Sections served.** §6 (interaction islands) primarily, and in the
|
||||
*preventing* direction rather than the fixing one — see below. §11
|
||||
(config registry) secondarily, by adding one option in the established
|
||||
shape rather than a new switch mechanism.
|
||||
|
||||
**Golden journey (§2).** No step is touched by 4a. 4b improves step 4
|
||||
(editing) for Lean specifically and changes nothing for any other
|
||||
language: the pending-abbreviation state exists only in `lean4` buffers.
|
||||
Neither stage changes launch, open, or attach.
|
||||
|
||||
**Interaction islands (§6).** **None added, and this is the load-bearing
|
||||
claim of Stage 4b.** An input method is the archetypal island: a modal
|
||||
state where ordinary keys mean something else, usually with its own
|
||||
keymap, its own escape, and its own set of commands that only work
|
||||
inside it. Stage 4b deliberately has none of those. There is no keymap,
|
||||
no dispatch shadow, no mode line indicator, no command that only works
|
||||
mid-abbreviation, and no key that exits. The pending state is invisible
|
||||
to every other subsystem, is abandoned by ordinary editing, and its
|
||||
worst failure is that the user's literal text stays literal. The
|
||||
`lean.abbrev` switch is an ordinary registry boolean, not an island
|
||||
toggle.
|
||||
|
||||
Stage 4a's chain is the mechanism that makes that possible, and it also
|
||||
retires a smaller island risk: today the only way for a second feature to
|
||||
react to a typed character is to compete with `pair.lua` for a one-shot
|
||||
record, and the natural workaround — inferring from buffer text — is how
|
||||
input methods grow their own private state and, eventually, their own
|
||||
modal surface.
|
||||
|
||||
**Config registry (§11).** One option, `lean.abbrev`, in exactly the
|
||||
`editing.auto-pair` shape (boolean, `mutability = "live"`, resolved
|
||||
against the typed edit's source buffer). This is the arc entering the
|
||||
registry as §9's earlier text predicted, and it is a genuine adoption
|
||||
rather than a new surface. Stage 4a adds none.
|
||||
|
||||
**Background-work attribution (§9).** Neither stage does background work.
|
||||
Both are synchronous inside an existing hook fan-out; no process is
|
||||
spawned, no timer armed, no request issued. There is nothing to attribute
|
||||
and nothing to worsen — recorded explicitly because "none" is an answer
|
||||
this section should be able to give without ambiguity.
|
||||
|
||||
**Debt this revision retires.** The unowned assumption that
|
||||
`take_typed_edit()` has exactly one consumer forever. That was never a
|
||||
decision — it was the shape of the only caller — and every future
|
||||
typed-character feature would have had to rediscover it. Stage 4a turns
|
||||
an accident into an API with a stated ordering contract.
|
||||
|
||||
**Debt this revision names rather than pays.** One, and it is real:
|
||||
Q#LN21's cross-peer undo degradation, now covering every abbreviation
|
||||
rather than three bracket pairs. The fix is chronological cross-peer undo
|
||||
arbitration, already on the standing backlog and already blocking Q#LN6.
|
||||
Stage 4b makes the existing gap more visible without widening the class
|
||||
of defect — but "more visible" is the honest word, not "unchanged."
|
||||
|
|
|
|||
Loading…
Reference in New Issue