From a38296583b81c83848c0217e8d76765b4173e8c7 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:44:53 -0400 Subject: [PATCH] docs: frame Lean 4 mode (Arc 8) The approved framing for Arc 8, revision 4, after three review rounds. Seven stages: grammar/mode, multi-root LSP affinity, the Lean language server, the Unicode input method, the goal view, the #eval output channel, and module hierarchy. 19 decisions, 64 acceptance criteria. Committed as this branch first commit per the house workflow; the implementation of Stage 1 follows. Co-Authored-By: Claude Opus 5 (1M context) --- docs/lean4-mode-framing.md | 1467 ++++++++++++++++++++++++++++++++++++ 1 file changed, 1467 insertions(+) create mode 100644 docs/lean4-mode-framing.md diff --git a/docs/lean4-mode-framing.md b/docs/lean4-mode-framing.md new file mode 100644 index 0000000..e1fe060 --- /dev/null +++ b/docs/lean4-mode-framing.md @@ -0,0 +1,1467 @@ +# Lean 4 mode — framing (Arc 8) + +pmacs has no Lean support of any kind: `grep -rin lean` over `*.rs`, +`*.lua`, `*.toml`, `*.md` returns zero hits outside the words "clean", +"boolean", and "leans on". A `.lean` file today opens as a pathless-ish +plain buffer — no grammar, no major mode, no comment syntax, no pair set, +no server. + +This lane closes that in seven stages. Stage boundaries are drawn where +the *substrate* changes, not where the feature list does — see §4. + +## 0. Why this lane, why now + +- Arc 5 (terminal), Arc 4 (themes), the config registry, and the mode + system are all complete, and Arc 7 Stage 1 (bottom panel) merged as #155 + at `e745068`. The goal view in Stage 5 is the first real consumer of the + panel placement API outside listview/compile/terminal, which is a useful + forcing function for it. +- The language-support pattern is well worn and cheap: #123 (JSON/YAML), + #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 + 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 seven stages get + and names precisely what is still missing. + +Parallel-safety: Stage 1 touches `Cargo.toml`, `src/syntax.rs`, +`src/highlight.rs`, and four runtime Lua files. Stage 2 touches +`src/lua_bindings/mod.rs` and `builtin/runtime/lsp.lua` only. Folding +Stage 3 (the other open lane) touches `pmacs-gpu/*` and +`src/semantic_render.rs`. None of the three footprints overlap; the only +file Stage 1 shares with anything is `Cargo.toml`, at one line. + +Stages 1 and 2 are independent of each other and **can** run as sibling +worktrees — they share no file. Per the #126/#127 lesson, that split is +recorded here, before either starts, rather than discovered during a +rebase. + +## 0.1 Revision history + +Revision 1 — initial. + +### Round 1 (rev 1 → rev 2) + +Five findings, all revision edits — no re-scout was required. The reviewer +independently reproduced both crate teardowns, every file:line citation, +the blast-radius greps, and the Lean server facts. + +1. **Acceptance 8 contradicted the change it pinned.** The negative pin + named Lua and Python as "byte-identical" fixtures, but both are among + the languages `constructor` retro-paints — so a fixture that didn't + move would have been exactly the vacuous-assertion shape from the #155 + R2 lesson. Acceptance 7/8 redrawn: Lua and Python moved to the positive + side with asserted deltas, and the negative pin now uses languages + verified to emit none of the four names. +2. **The retro-paint is broader than rev 1 stated, and differently + shaped.** `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated + into the `javascriptreact`, `typescript`, and `typescriptreact` + entries (`src/syntax.rs:1009`–`1056`), so `constructor` reaches + **seven** language entries, not four. More importantly the *shape* is + not "constructors": rust/python/javascript tag **every capitalized + identifier** (`#match? "^[A-Z]"`), and lua tags **every + table-constructor brace**. §2.3 and Q#LN4 now state this, because it + is what the ruling is actually about. +3. **The goal view's refresh loop had no seam.** There is no motion hook. + Named the real mechanism (debounced polling off `process.after-tick`) + in Q#LN13 rather than letting it grow a polling loop or new hook + substrate unframed. + +*(Round-1 findings are stated against the features, not stage numbers: +round 2 renumbered the stages, so a rev-1 "Stage 4" is now Stage 5.)* +4. **Q#LN10's ordering example didn't motivate the ordering.** `<` is not + in the proposed pair set, so `\<>` is safe under either order. Replaced + with the real collisions (64 abbreviation keys contain a pair-set + character), and stated the contract that finding exposes: the + abbreviation consumer must claim self-inserts that *extend an open + pending abbreviation*, not only completed expansions. +5. **Q#LN8's resolver must honor the search boundary.** A Lua + `lean-toolchain` walk that ignores `pmacs.project.search_boundary()` + breaks the contract `detect_project_within` exists to enforce and makes + the Stage 3 outermost-root test non-hermetic. + +### Round 2 (rev 2 → rev 3) — scope expansion + +Not review findings: the user pulled seven items out of §6 and into scope, +with the stated north star that **the arc should eventually match or +exceed what VS Code does with Lean**. Folded in, with two designs +corrected against ground truth the expansion request assumed differently: + +- **Lake version probe** (was deferred) → Q#LN7, rewritten. **Corrected: + there is no blocking process run in pmacs.** `pmacs.process` is + `spawn`/`write_stdin`/`terminate`/`list`/`status`/`events_take`/ + `forget`/`resize_pty`, all drained asynchronously off + `process.after-tick`; nothing returns output synchronously. A lazy + probe therefore cannot gate the first attach, so the design is + probe-plus-fallback-latch rather than probe-then-configure. Second + correction: **`lake` being on PATH does not mean Lean works** — see + §2.9, where the scouting machine's own `lake --version` fails. +- **Multi-root Lake scoping** (was deferred) → Q#LN15, and promoted to + its own stage. **Corrected: `root` is computed at + `builtin/runtime/lsp.lua:537`, *after* the reuse loop at `:529`–`:536`, + not before it.** The fix therefore hoists the computation above the + loop, which makes `project_root_for` run on the reuse path where it + previously did not — a real consequence for Q#LN8's function-valued + resolver, handled there. +- **`⦃⦄` / `⟮⟯` pairs** → folded into Q#LN6. +- **Lean in markdown fences** → Q#LN17. +- **`textDocument/waitForDiagnostics`** → Q#LN16. +- **Abbreviation table upkeep** → Q#LN11, as a documented process rather + than a deferral. +- **`#eval` / `#check` output channel** → Q#LN18, its own stage. +- **Module hierarchy** → Q#LN19, its own stage. + +Deliberately still deferred: the interactive infoview (`$/lean/rpc/*`) — +named as the arc's eventual destination, not its scope; the GPU goal band +(blocked on bottom-panel Stage 2); a `cursor.after-move` hook; `.olean` / +`.ilean`; and block-comment toggle, which the user confirmed belongs to +the comment arc's framing rather than this one. + +Nits corrected in round 1: the ledger-drift note (`agent-handoff.md` +omits the panel lane rather than describing it as in-review); Q#LN12's +layering (`_request_*_raw` are the Lua bindings in +`src/lua_bindings/mod.rs`; `src/lsp.rs` has `request_hover` — Stage 5 +touches both files); §2.2's chain step is +`pmacs.parse.language_from_filename`; §2.3 no longer calls +`Style::default()` entries "styled"; and bet 1's grammar count. + +### Round 3 (rev 3 → rev 4) + +Six findings against the round-2 expansion. All revision edits. + +1. **The response half of the seam was never designed** (the real hole). + Q#LN16 and Q#LN19 both awaited replies "through the Q#LN9 seam", and + acceptance pinned it — but Q#LN9 defined only `on_notification` and a + notification arm. Confirmed: **no Lua anywhere consumes + `ev.kind == "response"`**, so a `send_request` reply is drained and + dropped; `send_request` is effectively write-only from Lua. Q#LN9 now + specifies both halves, including one-shot removal-before-invoke and a + pending-response purge on server death, with acceptance mirroring the + notification-side integrity pins. +2. **The affinity key silently fragmented loose files for every + language.** `project_root_for`'s last fallback is `dir_of(path)`, so it + **never returns nil for a file with a path** — a naive + `(language_id, root)` key would give every directory of markerless + scratch files its own server, in Python and Go and TypeScript, caused + by a change made for Lean. Q#LN15 now rules: the affinity key is the + root only when a root was actually *detected*, and nil for the + fallback. Two acceptance cases pin it. +3. **An acceptance criterion was unimplementable.** `pmacs.hook` exposes + `add` / `define` / `list` / `run` and **no `remove`**, so "leaves no + `process.after-tick` subscription" could not be satisfied or tested. + Reworded to the observable: after teardown, ticks issue no request and + write nothing. +4. **Four stale cross-references survived the round-2 renumber**, despite + that round claiming reconciliation: the opening "four stages"; §2.5 + still calling multi-root a §6 deferral; Q#LN12's "only Rust in Stages + 2–4", broken three ways; and §4's row 7 omitting Stage 7's typed + request. Q#LN12 now carries a per-stage Rust table instead of a prose + claim, which is harder to get wrong on the next renumber. +5. **Q#LN7's latch had no named observation mechanism.** Added: it polls + `pmacs.lsp.list()` state on the `process.after-tick` cadence (there is + no event for "died before initialize"), it calls `pmacs.lsp.stop` + before spawning the fallback so `RestartPolicy` cannot respawn the + broken command underneath it, and it updates `command`/`args` only, + preserving user-supplied `env`/`settings`/`init_options`/`root`. +6. Wording: `\{}` expands to `{$CURSOR}`; `⦃⦄` comes from `\{{}}`. + + +## 1. What ships + +Seven stages. 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 +auto-pairing (including `⟨⟩`, `⦃⦄`, `⟮⟯`). Lean fenced blocks in markdown +highlight too. No LSP, no protocol change, no frontend change. + +**Stage 2 — multi-root LSP server affinity.** Pure substrate, no Lean +content: `ensure_server` stops reusing a server across project roots. +Independently valuable for every language pmacs supports; a prerequisite +for Lean being usable across more than one Lake package. Split out +precisely *because* it is cross-cutting — see §4. + +**Stage 3 — the Lean language server.** `pmacs.lsp.config.lean4` drives +`lake serve` with a Lake-aware outermost root, a lazy toolchain probe and +a one-shot `lean --server` fallback, and a notification-subscription seam +so `$/lean/fileProgress` has an owner. 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 `α`, +`\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. + +**Stage 5 — the goal view.** A `*lean-goal*` panel that renders +`$/lean/plainGoal` at the point, refreshed on a debounced tick and on +file-progress completion, displayed through #155's +`pmacs.window.display(buf, { side = "bottom" })`. + +**Stage 6 — the `#eval` / `#check` output channel.** Lean reports command +output as *information*-severity diagnostics, which pmacs currently +squiggles and counts in the modeline. Routes them to a `*lean-output*` +panel instead, via a per-server severity policy that changes nothing for +any other language. + +**Stage 7 — module hierarchy.** `$/lean/prepareModuleHierarchy` and +`$/lean/moduleHierarchy/{imports,importedBy}` into the existing listview +panel. + +## 2. Ground truth (scouted 2026-07-24, `main` @ `e745068`) + +### 2.1 Crate facts (external, verified by downloading and reading both) + +Two candidate grammar crates exist. They are not close in quality. + +**`tree-sitter-lean4` 0.3.0** (`wvhulle/tree-sitter-lean`) — **rejected**: + +- Depends on `tree-sitter = "0.25"` **directly**, not on the shared + `tree-sitter-language 0.1` ABI crate. The workspace is on + `tree-sitter = "0.26"`, and `^0.25` excludes it, so this forks the graph + and its `Language` is a different type from ours. This is the exact + failure mode already documented for `tree-sitter-dockerfile` in + `Cargo.toml`'s comments. +- `src/lib.rs` exports only `pub fn language() -> Language`. Its README + advertises `tree_sitter_lean4::LANGUAGE.into()`, which **does not + exist** — the README is stale. +- Its `include` list is `["build.rs", "src/*", "grammar.js", "grammar/*", + "tree-sitter.json"]`. **No `queries/`.** It ships no highlights query at + all; the upstream repo's queries target Helix. +- Its `build.rs` shells out to a `tree-sitter` CLI when `src/parser.c` is + absent. `parser.c` *is* in the package, so this would not fire — but it + is a live hazard in a crate we would otherwise depend on. + +**`arborium-lean` 2.18.1** (`bearcove/arborium`) — **selected**: + +- `[dependencies] tree-sitter-language = "0.1"` and nothing else at + runtime. No second `tree-sitter` in the graph. +- `grammar/src/parser.c` declares `#define LANGUAGE_VERSION 15` and + `.abi_version = LANGUAGE_VERSION`. ABI 15 is current for tree-sitter + 0.25/0.26. Pre-generated; no CLI at build time. A 1,150-byte + `grammar/scanner.c` supplies one external token (`NEWLINE`). +- Exports `pub const fn language() -> LanguageFn`, plus + `HIGHLIGHTS_QUERY` (`include_str!("../queries/highlights.scm")`, 213 + lines), `INJECTIONS_QUERY` (empty string), and `LOCALS_QUERY` (empty + string). +- `edition = "2024"`, `rust-version = "1.85"`. The workspace is edition + 2024 / MSRV 1.95 on rustc 1.95.0. Compatible. +- **Two things to verify at implementation, not assumed here.** (a) Every + existing entry in `BUILTIN_LANGUAGES` is spelled + `tree_sitter_foo::LANGUAGE.into()` — a `LanguageFn` const. arborium + exposes a `const fn` instead, so the entry reads + `arborium_lean::language().into()`, a shape no current entry uses. + (b) arborium's README shows usage against a + `tree_sitter_patched_arborium` crate. That crate is *not* in the + dependency graph and the `LanguageFn` ABI is the shared one, so this + should be cosmetic — but the loader gets a real parse smoke test against + `tree-sitter 0.26` before the entry is trusted. + +Neither crate is first-party. `leanprover` ships no tree-sitter grammar; +Lean's own tooling parses with the Lean kernel. The upstream README of the +rejected crate says so plainly: *"Lean is a very extensible language. +Therefore, the Tree-Sitter grammar is of limited use."* That is true and it +bounds what Stage 1 can promise — see the bets in §5. + +### 2.2 The grammar table and the detection chain + +`src/syntax.rs:816` `BUILTIN_LANGUAGES` is a `&[LanguageEntry]` of +`{ name, extensions, loader, highlights_query, locals_query, +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 +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` +without any `pmacs.lsp.filetypes` entry; adding one would be dead weight. + +**`LanguageEntry.name` is the LSP `language_id`.** `ensure_server` at +`builtin/runtime/lsp.lua:540` passes `language_id = language` straight +into `pmacs.lsp.spawn`, and the surrounding comments (lines 70, 86, 122) +record that `c`/`cpp` and the four TS/JS entries exist as separate entries +*only* so that id is accurate. This makes the entry name a wire-visible +decision, not a label — see Q#LN2. + +### 2.3 The global capture table (the #146 trap) + +`Theme::default_dark()` at `src/highlight.rs:143` is a single flat +`&[(&str, Style)]` shared by **every** language and by LSP semantic-token +type names. `lookup()` walks dotted prefixes right-to-left, so +`@function.definition` falls back to `function`. + +Resolving arborium's Lean query against the current table: + +| Lean capture | Resolves to | Effect | +|---|---|---| +| `@comment` `@string` `@number` `@operator` `@constant` | themselves | distinct style | +| `@constant.builtin` `@property` `@attribute` | themselves | distinct style | +| `@function.definition` `@function.call` `@function.builtin` | `function` | distinct style | +| `@type.definition` | `type` | distinct style | +| `@string.special` | `string` | distinct style | +| `@keyword.conditional` `.function` `.import` `.modifier` | `keyword` | styled, but flattened | +| `@variable` | `variable` | **entry exists but is `Style::default()`** — visually plain | +| `@punctuation.special` `.bracket` `.delimiter` | `punctuation` | **`Style::default()`** — visually plain | +| `@constructor` | — | **unstyled** | +| `@character` | — | **unstyled** | +| `@warning` | — | **unstyled** | + +Blast radius of adding each name, measured over every `.scm` in the +workspace's actual dependency graph (crates confirmed present in +`Cargo.lock`): + +- **`constructor` — seven language entries, not four grammars.** The + emitting crates are `tree-sitter-javascript`, `-lua`, `-python`, and + `-rust`, but `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated + base-first into `javascriptreact`, `typescript`, and `typescriptreact` + as well (`src/syntax.rs:1009`–`1056`), so the reachable set is + `rust`, `lua`, `python`, `javascript`, `javascriptreact`, `typescript`, + `typescriptreact`. + + **And the shape is not "constructors".** Verified against the crate + queries: + + ```scheme + ; rust, python, javascript — every capitalized identifier + ((identifier) @constructor (#match? @constructor "^[A-Z]")) + + ; lua — every table-constructor brace + (table_constructor [ "{" "}" ] @constructor) + ``` + + So adding `constructor` recolors **every capitalized identifier** in + five entries (in Rust that is `Some`/`None`/`Ok`/`Err` and every + class-cased name; in Python/JS/TS every class-cased name) and **every + `{`/`}` of a Lua table literal.** That is the change being ruled on in + Q#LN4 — not a narrow constructor-only recolor. +- `character` — `tree-sitter-zig` only. +- `keyword.conditional` — `tree-sitter-cmake` and `-zig` only. Both + currently flatten to `keyword`. +- `warning` — used by **no** grammar in the graph. + +Verified clean of all four names (usable as negative-pin fixtures): +markdown, json, yaml, html, css, c, cpp, go, containerfile, make, toml, +bash. + +This is the #146 lesson verbatim: *the capture table is global, so adding a +capture name retro-paints every other language; check the reverse direction +and pin it.* + +### 2.4 The LSP substrate + +- `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 + 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:1448`, 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 + from it. Any new consumer must extend that loop, not open a second one. +- **`_request_*_raw` helpers route outbound positions through + `outbound_position` (byte → negotiated encoding); a raw `send_request` + does not.** This is handoff §4's standing invariant, and it is sharper + for Lean than for any language pmacs already supports: Lean source is + saturated with non-ASCII (`α`, `→`, `⟨⟩`, `∀`), the Lean server + negotiates UTF-16 by default, and a raw byte column is wrong on + essentially every interesting line. This is why Stage 5 is not + "just call `send_request` from Lua" — see Q#LN12. + +### 2.5 Project-root detection + +`project_root_for` (`builtin/runtime/lsp.lua:513`) resolves: +`pmacs.lsp.config[language].root` → `pmacs.project.detect` → the file's own +directory. Two gaps for Lean: + +1. **No Lean marker, and no way to add one.** `default_markers()` + (`src/project.rs:145`) is `Cargo.toml`, `.luarc.json`, `pyproject.toml`, + `go.mod`, `deno.json`, `deno.jsonc`, `package.json`, `.git`. The + `pmacs.project` Lua surface is `detect`, `set_search_boundary`, + `search_boundary` — **there is no marker-registration binding.** +2. **`detect_project` returns the innermost match; Lean needs the + outermost.** `walk_for_marker` returns the first ancestor that matches. + `lean4-mode` deliberately does the opposite: + + ```elisp + (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) + (setq root dir + file-name (file-name-directory (directory-file-name dir)))) + ``` + + It keeps walking *past* each hit and takes the topmost. This matters + concretely: Lake vendors dependencies under `/.lake/packages/*`, + and each vendored package carries its own `lean-toolchain`. Opening + `/.lake/packages/batteries/Batteries/Data/List.lean` must serve + from ``, not from `batteries`. Innermost-wins gets this backwards + every time, and the symptom is a server that starts, initializes, and + then reports import errors for the whole file. + +Third, and the reason Stage 2 exists: `ensure_server` +(`builtin/runtime/lsp.lua:527`) reuses any live server with a matching +`language_id` regardless of the new file's project, so **the first `.lean` +file opened fixes the root for every later `.lean` file.** For most +languages that is an inconvenience; for Lean, where `lake serve` is bound +to one package, it is a correctness failure. Rev 1 carried this as a +deferral. **It is now Stage 2 / Q#LN15.** + +One property of `project_root_for` matters for that fix and is easy to +miss: its final fallback is `dir_of(path)`, so **it never returns nil for +a file with a path.** A markerless scratch file's "root" is its own +directory. Q#LN15's affinity rule has to account for that or it silently +changes loose-file behavior for every language. + +### 2.6 Typed-edit provenance — the only input-method-shaped seam + +`builtin/runtime/pair.lua` is the whole precedent for "react to a typed +character": subscribe to `buffer.after-edit`, gate on +`ed.this_command() == "buffer.self-insert"` (`pair.lua:213`), then take the +exact provenance record. + +`pmacs.editor.take_typed_edit()` (`src/lua_bindings/mod.rs:12798`) 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: + +> Consuming clears the slot: later callbacks and nested manual hook runs +> see nil, and the producer clears any untaken record when the fan-out +> returns. Per-frontend — one frontend can never take another's record. + +**It is one-shot and first-come-first-served.** `pair.lua` already consumes +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. + +Related, from `pair.lua:30`'s Q#AP1 note: only the nine built-in pair chars +`()[]{}"'` and backtick are excluded from the frontends' optimistic +classifiers. A pair char outside that set still pairs, but its opener is a +source-peer op and its closer a daemon-peer op, so **its undo is +cross-peer-degraded**. Lean's `⟨⟩` is outside that set. + +### 2.7 Panels and generated read-only buffers + +- #155 landed on `main` at `e745068`. `pmacs.window.display(buf, { side = + "bottom", select = true })` is the placement call; `listview.lua:138` + shows the adopter shape, gated on `spec.display == "panel"`. + `pmacs.window.params()` and `pmacs.window.quit()` complete the surface. +- Read-only generated buffers use the listview idiom, documented at + `builtin/runtime/compile.lua:264`: an erroring `pmacs.buffer.add_intercept` + for user edits, with module writes passing `{ bypass_intercept = true }`. +- **Note for whoever picks this up on another machine:** the ledgers are + stale about this. `docs/active-work.md:57` still heads the lane "Stage 1 + IN REVIEW"; `docs/agent-handoff.md` §1 is stamped at #148 and **omits + the bottom-panel lane entirely**. It merged at `e745068`. That drift is + #156's business, not this lane's, but do not scout Stage 5 off either + file. + +### 2.8 Lean server facts (external, verified against `leanprover/lean4`) + +From `src/Lean/Server/FileWorker/RequestHandling.lean` and +`src/Lean/Data/Lsp/Extra.lean`: + +- `$/lean/plainGoal` — params extend `TextDocumentPositionParams`; result + is `PlainGoal { rendered : String, goals : Array String }` or null. +- `$/lean/plainTermGoal` — result `PlainTermGoal { goal : String, + range : Range }` or null. +- `$/lean/fileProgress` — a server→client **notification**, params + `{ textDocument : VersionedTextDocumentIdentifier, processing : Array + { range : Range, kind : "processing" | "fatalError" } }`. This is the + "orange bar": which regions are still elaborating. +- Also present, all deferred here: `$/lean/rpc/{connect,call,release, + keepAlive}` (the interactive widget/infoview stack), + `$/lean/prepareModuleHierarchy`, `$/lean/moduleHierarchy/{imports, + importedBy}`, `$/lean/waitForILeans`, `textDocument/waitForDiagnostics`. +- From `src/Lean/Data/Lsp/InitShutdown.lean`: + `InitializationOptions { hasWidgets? : Option Bool, logCfg? : Option + LogConfig }`. `hasWidgets?` **defaults to false**, and its documented + meaning is: when true, the server may *omit* information from standard + LSP messages because the client will fetch it interactively. A + plain-goal client wants the default. Omitting `initializationOptions` + entirely is accepted (`FromJson` maps missing/null to `none`). +- Server launch, from `lean4-mode`'s `lean4--server-cmd`: `lake serve` when + Lake ≥ 3.1.0 is found, else `lean --server`. + +### 2.9 There is no blocking process run — and `lake` on PATH proves nothing + +The complete `pmacs.process` Lua surface is `spawn`, `write_stdin`, +`terminate`, `list`, `status`, `events_take`, `forget`, `resize_pty`, +`_tick`. `ProcessSpec` (`src/process.rs:193`) carries no +wait-for-output mode, and there is no `wait_with_output` anywhere in +`src/process.rs`. Everything is asynchronous and drained off +`process.after-tick`, which is how compile mode streams. + +**Consequence: any toolchain probe is async, and cannot gate the attach +that triggered it.** A design that reads "probe, then set +`pmacs.lsp.config.lean4.command`, then attach" cannot be written against +this substrate. + +Second, and sharper — scouted on this machine: + +``` +$ elan --version +elan 4.2.1 (3d5138e15 2026-03-18) +$ lake --version +error: no default toolchain configured. run `elan default stable` to ... +$ lean --version +error: no default toolchain configured. run `elan default stable` to ... +``` + +`elan` installs `lake` and `lean` as **toolchain shims**. Both are on +PATH, both are executable, and both fail. So: + +- A version probe must parse a *failure*, not just a version string — + `lake --version` returning non-zero is a normal, common state. +- `command -v lake` is worthless as a capability check. +- The failure modes a Lean client must survive are: lake absent, lake + present but shimmed with no toolchain, lake present and working but too + old, and lake working but the directory is not a Lake package. Only the + third is a *version* question. +- **Acceptance cannot assume a working Lean toolchain exists.** Every + Stage 3+ test runs against the fake LSP server; a live `lake serve` + smoke is PATH-gated *and* success-gated, following the #123 JSON/YAML + provider-smoke pattern. + +### 2.10 Information-severity diagnostics are squiggled and counted + +`src/diag.rs:50` defines `DiagnosticSeverity` with `Information` mapped +from LSP severity `3` (`:103`). Information diagnostics get the +`ui.diag.info` face (`:408`), a `UnderlineStyle::Single` squiggle +(`:426`), and a slot in the severity count tuple (`:223`) that feeds the +modeline. + +Lean reports every `#eval`, `#check`, `#print`, and `example` result as an +information-severity diagnostic at the command's position. Under the +current surface those render as underlined "problems" with a gutter sign +and a modeline count — which is why rev 1 called them noise. The claim is +now specific: they are not merely unstyled, they are **actively +mis-rendered as defects**, and the count misleads. + +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. + +## 3. Decisions + +### Q#LN1 — Bundle `arborium-lean` 2.18; reject `tree-sitter-lean4` + +Per §2.1. The decision is forced by the dependency graph, not by taste: +`tree-sitter-lean4`'s `tree-sitter ^0.25` cannot coexist with the +workspace's 0.26. Its missing queries and stale README are secondary. + +Risk accepted: `arborium-lean` is a third-party republish from a grammar +collection, not the grammar's upstream. `codebook-tree-sitter-latex` (#144) +set this precedent for exactly the same reason — no usable first-party +crate exists. The mitigation is the same: pin a real parse + highlight +smoke test so a bad republish fails our suite, not a user's file. + +### Q#LN2 — Name the entry `lean4`, not `lean` + +`LanguageEntry.name` becomes the `didOpen` `language_id` (§2.2), and the +Lean ecosystem's id is `lean4` (vscode-lean4 uses it; `lean` is Lean 3). +The grammar's C symbol is `tree_sitter_lean`, but that is arborium's +business — the entry name is ours to choose. + +Consequences, all deliberate: `pmacs.comment.strings.lean4`, +`pmacs.pair.sets.lean4`, `pmacs.lsp.config.lean4`, and a mode line reading +`lean4`. An Emacs `-*- mode: lean -*-` or a Vim `ft=lean` modeline is +normalized to `lean4` through `pmacs.parse.modeline_aliases`, so neither +spelling strands a file. + +### Q#LN3 — Extensions: `lean` only + +Not `.olean` (compiled binary artifacts — opening one as text is never +what the user wants) and not `.ilean` (JSON metadata; if anything it +belongs to the `json` entry). + +### Q#LN4 — Add four capture entries and pin the retro-paint in both directions + +**Ruled (round 1): add to the global table.** The alternative is an in-repo +overlay, and there is no partial option — see below. + +Add to `Theme::default_dark()`: `constructor`, `character`, +`keyword.conditional`, and `warning`. + +Rationale, per name: + +- **`constructor`** is the consequential one. Per §2.3 it reaches seven + language entries and its real effect is *"recolor every capitalized + identifier in five entries and every `{}` in Lua"*. That is stated + bluntly because it is the decision, not a side effect. It is + nevertheless the right call: capitalized-identifier-as-constructor is + the mainstream editor convention (it is what nvim-treesitter, Helix, and + Zed all render off these same queries), those tokens are currently + *unstyled* rather than deliberately plain, and Lua's braces gaining a + colour is a cosmetic difference on a token that today renders as default + text. The cost of avoiding it is owning a forked 213-line query forever. +- `character` — `tree-sitter-zig` only, currently unstyled. +- `keyword.conditional` currently flattens to `keyword`. Giving it + `keyword.control`'s brighter style makes Lean's `if`/`then`/`else`/ + `match`/`do` read the way Rust's already do, and reaches cmake and zig + the same way. +- `warning` has zero blast radius and gives Lean's `(sorry)` — an + unproved goal, the single most important thing to see in a proof file — + a visible style. + +All four are pinned in the reverse direction exactly as #146 required — +acceptance 7 asserts the retro-paint *happened* on each affected language, +acceptance 8 asserts it did not leak into languages that emit none of the +four names. + +**Rejected alternative:** an in-repo query overlay +(`builtin/queries/lean4/highlights.scm`) rewriting the capture names into +the existing vocabulary, the #144 LaTeX pattern. It avoids touching the +global table, but it forks a 213-line query we would then own and +hand-merge on every arborium bump. Overlays are for grammars whose crate +ships *no* usable query; arborium ships one. + +**There is no middle option.** Styling Lean's constructors without +touching the other seven entries requires renaming the capture, which +requires the overlay, which forks the query. The choice is binary: accept +the retro-paint, or own the fork. + +### Q#LN5 — Comments: `--` only in Stage 1 + +`pmacs.comment.strings.lean4 = "--"`. Lean's block comment is `/- ... -/` +and its docstring is `/-- ... -/`; block-comment toggling is an existing +named deferral of the comment arc (`docs/comment-toggle-framing.md`) and +this lane does not front-run it. + +### Q#LN6 — Pair set includes `⟨⟩`, and the degradation is named + +`pmacs.pair.sets.lean4 = { "()", "[]", "{}", "⟨⟩", "⦃⦄", "⟮⟯", '""' }`. + +`⟨⟩` (anonymous constructor) is among the most-typed constructs in Lean and +omitting it would make the pair set feel broken. It is outside the nine +built-in pair chars, so per §2.6 its undo is cross-peer-degraded. That is a +documented, pre-existing limitation of user-extended pairs whose general +fix is chronological cross-peer undo arbitration — already on the standing +backlog. Ship it; name it in the module comment. + +`''` is excluded: Lean uses `'` as a primed-identifier suffix (`h'`, +`foo'`), so pairing it would fight the user constantly. Same reasoning that +excludes it for Rust. + +`⦃⦄` (strict implicit binder) and `⟮⟯` ride along — one list entry each, +same degradation, and both have abbreviation keys (`\{{}}`, `\([])'`) so +omitting them would make the input method produce brackets the pair set +does not understand. + +### Q#LN7 — `lake serve` by default, with a lazy probe **and** a failure latch + +```lua +pmacs.lsp.config.lean4 = pmacs.lsp.config.lean4 or { + command = "lake", + args = { "serve" }, +} +``` + +`lean4-mode` probes Lake's version and falls back to `lean --server` below +3.1.0. This lane does the same, but **lazily and asynchronously**, and +pairs it with a failure latch — because §2.9 makes probe-alone +insufficient in two independent ways. + +**Where the probe runs.** Not at init: `pmacs.lsp.config` is a declarative +table, and spawning a process at startup for every user, Lean-using or +not, is the cost rev 1 refused. It runs on the first `.lean` attach, in +`builtin/runtime/lean.lua`, cached for the session. + +**Why the probe cannot gate the first attach.** There is no blocking +process run (§2.9). `pmacs.process.spawn` + `events_take` off +`process.after-tick` is the only shape available, so the probe's verdict +arrives *after* `ensure_server` has already had to decide. This is the +correction to the round-2 request, which assumed the verdict could be +consulted before configuring. + +**The design that follows:** + +1. First `.lean` attach spawns `lake serve` optimistically and fires + `lake --version` alongside it, with `cwd` at the resolved Lake root. +2. If the probe reports a version below 3.1.0, or the server dies before + `initialize` completes, a **one-shot latch** swaps in `lean --server` + and restarts once. The latch is per session and never re-arms. + + **How the latch observes failure.** There is no event for "exited + before initialize" — the drain ignores state events. The latch polls + `pmacs.lsp.list()` for the server's `state.kind` on the same + `process.after-tick` cadence Q#LN13 uses, and treats + `crashed`/`stopped` reached without an intervening `initialized` as + the trigger. (Q#LN9's pending-response purge fires on the same + transition, so anything already awaiting a reply fails cleanly rather + than hanging.) + + **Interplay with `RestartPolicy`.** The manager will otherwise respawn + the same broken command underneath the latch, producing a loop the + latch cannot see the end of. So the latch calls `pmacs.lsp.stop` on + the failing server *first*, then swaps the config, then spawns — the + fallback is a fresh server, not a restart of the old one. + + **The swap is a field update, not a table replacement.** It rewrites + only `command` and `args`, preserving any user-supplied `env`, + `settings`, `init_options`, and `root` on `pmacs.lsp.config.lean4`. A + wholesale table replacement would silently discard a user's + `init.lua` configuration at exactly the moment they are least likely + to notice. +3. If `lean --server` also fails, the error surfaces through the ordinary + `pmacs.lsp.last_error` path. pmacs does not attempt to install a + toolchain. + +**Why a latch and not just a probe.** Per §2.9 the failure modes are lake +absent, lake shimmed-with-no-toolchain, lake too old, and +not-a-Lake-package. **Only the third is a version question**, and the +scouting machine exhibits the second — `lake --version` there exits +non-zero with `error: no default toolchain configured`. Since the failure +path must exist regardless, the probe's job shrinks to the one case +failure detection would otherwise handle slowly (an old-but-working lake +that starts a useless server). Probe and latch are complements, not +alternatives. + +**Named risk.** The optimistic first spawn means a user on a +lake-less-but-lean-ful toolchain sees one failed spawn before the +fallback. That is a one-line status message, once per session, and it +buys not blocking every other user's first attach behind a process +round-trip. + +No `init_options`. Per §2.8, `hasWidgets?` defaults to false and that is +the correct value for a client that reads plain goals out of standard +messages. + +### Q#LN8 — Lake-aware root via a **function-valued** `config.root` + +Generalize `project_root_for` (`builtin/runtime/lsp.lua:513`) so +`pmacs.lsp.config[lang].root` may be a `function(path) -> string|nil` as +well as a string, and implement Lean's resolver in +`builtin/runtime/lean.lua`: walk up from the file's directory collecting +every ancestor containing `lean-toolchain`, and return the **outermost**; +fall back to `pmacs.project.detect`, then the file's directory. + +**The walk stops at `pmacs.project.search_boundary()`.** This is not +optional politeness: `detect_project_within` (`src/project.rs:213`) exists +precisely so a stray marker above a temp fixture cannot leak into +detection, and a Lua walk that ignores the boundary breaks that contract — +including for acceptance 23, whose outermost-root assertion is otherwise +non-hermetic against any `lean-toolchain` that happens to sit in an +ancestor of the test's tempdir. + +Why this and not the two alternatives: + +- *Adding `lean-toolchain` to Rust's `default_markers()`* does not work — + `detect_project` is innermost-wins by construction (§2.5), and inverting + it globally would change Rust/Go/Node root detection for every user. +- *A `pmacs.project.add_marker` Lua binding* is a bigger new surface than + this lane needs and still leaves the innermost/outermost problem. + +The function-valued `root` is ~3 lines in `lsp.lua`, is a strict +generalization (a string still works), and puts the Lean-specific rule in +the Lean module where it belongs. + +### Q#LN9 — Notification **and response** subscription seams in the existing dispatch + +Per §2.4 there is exactly one `events_take` consumer, and its `if/elseif` +chain handles five `request` methods plus `initialized`. It ignores +notifications **and responses** — and no Lua anywhere in the runtime +consumes `ev.kind == "response"`. So today a `send_request` reply is +drained and dropped on the floor: **`send_request` is effectively a +write-only API from Lua.** + +Rev 2 specified only the notification half. That was a hole, since +Q#LN16 (`waitForDiagnostics`), Q#LN19 (`imports` / `importedBy`), and +Q#LN12's typed goal request all await replies. Both halves ship in +Stage 3. + +```lua +pmacs.lsp.on_notification(method, fn) -- fn(sid, params); persistent +pmacs.lsp.on_response(sid, request_id, fn) -- fn(result, err); ONE-SHOT +``` + +Routed from two new arms of the existing loop: + +- `elseif ev.kind == "notification"` → every subscriber registered for + `ev.method`. +- `elseif ev.kind == "response"` → the one-shot registered for + `(sid, ev.id)`, **removed before it is invoked** so a raising handler + cannot be re-entered. + +Each handler is `pcall`ed, so one raising subscriber cannot stall the +drain or starve the `request` arms that share it. + +**Pending-response lifetime.** A one-shot whose server dies never fires on +its own, leaking the registration and hanging whatever awaits it. On +`crashed` / `stopped` / `restarting` for a `sid`, every pending one-shot +for that `sid` is invoked with an error and cleared. This is what lets +Stage 5's in-flight tracking (acceptance 52) be honest rather than +optimistic, and it is what Q#LN7's latch observes (below). + +Explicitly **not** a second `events_take` caller — a second drain would +steal events from `handle_server_requests`. The tests pin that in both +directions: a Lean subscriber must not cause `workspace/applyEdit` to be +missed, and a raising subscriber must not stop later events in the same +drain. + +Stage 3 registers `$/lean/fileProgress` on the notification seam and +`waitForDiagnostics` on the response seam; stages 5 and 7 use the response +seam for `plainGoal` and the hierarchy calls. + +### Q#LN10 — Stage 4 mechanism: one shared provenance read, not two + +The hazard is §2.6 — `take_typed_edit()` is one-shot and `pair.lua` +already consumes it. + +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. + +Two consequences worth stating up front: + +- 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. + + (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 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. + +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 + +`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. + +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. + +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. + +### Q#LN12 — Stage 5 sends `$/lean/plainGoal` through a typed Rust request + +Per §2.4, `send_request` does **not** route positions through +`outbound_position`. Lean negotiates UTF-16 and Lean source is +overwhelmingly non-ASCII, so a Lua-built byte column would be wrong +wherever it matters most. + +Stage 5 therefore adds a typed request that reuses `outbound_position` +unchanged. It spans **two files**, because the `_raw` naming is a layer +boundary, not a module: + +- `src/lsp.rs` — `request_plain_goal`, alongside `request_hover` + (`src/lsp.rs:1690`) and `request_definition` (`:1733`), which is where + `outbound_position` is actually applied. +- `src/lua_bindings/mod.rs` — the `_request_plain_goal_raw` binding, + alongside the `_request_hover_raw` family (`:9501`–`:9823`). + +It is a thin builder — the result is passed through as JSON and parsed in +Lua, since `PlainGoal` is two fields and does not warrant a typed store. + +It exists specifically to honor handoff §4's standing invariant rather +than quietly reintroduce the bug it was written to prevent. + +**Where the arc's Rust actually lives** (rev 2 stated this in pre-renumber +stage numbers and was wrong three ways): + +| Stage | Rust | +|---|---| +| 1 | `Cargo.toml` + `BUILTIN_LANGUAGES` entry + Q#LN4's four capture entries | +| 2 | `lsp.list()` row builder (`mod.rs:9919`) | +| 3 | **none** — Lua only | +| 4 | **none** — Lua only | +| 5 | `request_plain_goal` + its binding | +| 6 | `LspServerSpec` severity-policy field and its publish-path honoring | +| 7 | `request_prepare_module_hierarchy` + its binding | + +Stages 3 and 4 — the two largest Lean-specific stages — are entirely Lua. + +### Q#LN13 — Stage 5 goal panel shape + +- `*lean-goal*`, read-only via the erroring-intercept idiom, module writes + with `{ bypass_intercept = true }` (§2.7). +- Displayed with `pmacs.window.display(buf, { side = "bottom", select = + false })`. `select = false`: a goal view that steals focus on every + cursor move is unusable. +- **Refresh mechanism, named explicitly because there is no motion hook.** + The complete hook inventory is `buffer.{after-edit,after-load, + after-save,after-switch,before-save}`, `editor.before-quit`, + `frontend.detached`, and `process.after-tick`. Nothing fires on cursor + movement. Stage 5 therefore refreshes from a **debounced poll off + `pmacs.hook.add("process.after-tick", …)`** — the cadence pattern + autosave (`autosave.lua:139`) and compile (`compile.lua:687`) already + use — comparing the point against the last position it queried and + issuing at most one in-flight `$/lean/plainGoal` at a time. + + This is written down so Stage 5 cannot quietly grow either an + unframed polling loop or new hook substrate. A `cursor.after-move` hook + would be the better long-term answer; it is out of scope here and is + named in §6. +- Also refreshed on a `$/lean/fileProgress` notification whose + `processing` array no longer covers the point's range. +- Content: `PlainGoal.rendered` when present, "no goals" when the result is + null with the file elaborated, "elaborating…" when file-progress still + covers the point. The three states are distinct and the middle one is the + one users actually need to trust. +- Keys under `pmacs.keymap.bind { scope = "mode", mode = "lean4", … }` + (#129's mode-scoped keymaps). + +### Q#LN14 — No protocol change in any stage + +Stages 1–4 and 7 touch no wire surface at all. Stage 5's panel rides #155 +Stage 1, which is grid-only and bumped nothing; Stage 6 adds a field to +the in-process `LspServerSpec`, which is not wire. A GPU-rendered goal band +needs bottom-panel Stage 2, which is itself unframed — so the GPU half is +deferred, not attempted. Protocol stays v20. + +### Q#LN15 — Multi-root server affinity (Stage 2, substrate) + +Today `ensure_server` reuses any live server whose `language_id` matches, +**regardless of project root** (`builtin/runtime/lsp.lua:524`–`536`, whose +own comment documents this as a known limitation). For Lean this is not a +rough edge but a correctness failure: `lake serve` is bound to one Lake +package, so the second package a user opens gets a server that cannot +resolve its imports. + +The change is small and spans two files: + +- **`src/lua_bindings/mod.rs:9919`** — the `lsp.list()` row builder sets + `id`/`label`/`language_id`/`command`/`state`/`attempt`. Add `root_uri` + from `spec.root_uri` (already `Option` on `LspServerSpec`, + `src/lsp.rs:125`) and `cwd`. Bump the `create_table_with_capacity` + hint. +- **`builtin/runtime/lsp.lua:521`–`551`** — hoist `local root = + project_root_for(language, path)` **above** the reuse loop and match on + the `(language_id, root_uri)` pair. + +**Correcting the round-2 request:** `root` is currently computed at +`:537`, *after* the loop, not before it. Hoisting is therefore part of the +change, and it has a consequence: `project_root_for` begins running on the +reuse path, where it previously ran only on spawn. For Q#LN8's +function-valued Lean resolver — which walks the filesystem — that means +once per attach rather than once per spawn. The resolver memoizes per +directory for the session. + +**Comparison rule, part 1 — hand-spawned servers.** Compare +`info.root_uri` against the request's affinity key, with nil matching nil. +A server spawned directly from `init.lua` with only `cwd` set has +`root_uri = nil` and will therefore *not* match a root-bearing request — +it gets a new server rather than being silently adopted. Conservative and +deliberate, but a behavior change, so acceptance asserts it. + +**Comparison rule, part 2 — markerless files must not fragment.** Per +§2.5, `project_root_for` **never returns nil for a file with a path**: its +last fallback is `dir_of(path)`. A naive `(language_id, root)` key +therefore gives *every directory of markerless scratch files its own +server*, for **every language** — two loose `.py` files in different +directories would spawn two pyrights where today they share one. That is a +silent regression for Python, Go, TypeScript and everyone else, caused by +a change made for Lean. + +Ruling: **the affinity key is the root only when a root was actually +detected.** `project_root_for` returns `(root, source)` with `source` one +of `"config"`, `"detected"`, or `"fallback"`; the affinity key is `root` +for the first two and **`nil` for `"fallback"`**. The directory is still +passed as `cwd` / `rootUri` exactly as today — only the *matching* key +changes. + +Consequences, both intended: + +- Files in a real project (Cargo/Lake/go.mod/…) get one server per root — + the fix. +- Markerless loose files keep today's single shared server per language — + no change, which is the point. + +**Rejected alternative:** keying on the fallback directory anyway and +accepting per-directory servers. It fragments the common scratch-file case +for every language in the editor to buy nothing for Lean, whose files are +essentially always in a Lake package. + +**Blast radius, stated plainly.** This is the central server-affinity +function for *every* LSP language in pmacs. A bug here routes a file to +the wrong server: diagnostics land on the wrong buffer, or a redundant +server spawns. This is why it is Stage 2 and its own PR, with no Lean +content in the diff — a cross-cutting change to every language's server +affinity must not be reviewable only as a Lean feature. + +**Named risk: unbounded server growth.** Per-root affinity means opening +files across N Lake packages spawns N `lake serve` processes, and Lean +elaboration is memory-hungry. rust-analyzer has the same property and no +editor caps it by default. No cap ships here; `pmacs.lsp.stop` is the +manual escape, and an LRU reaping policy is named in §6. + +### Q#LN16 — `textDocument/waitForDiagnostics` (Stage 3) + +A plain request (no position, so no `outbound_position` concern — Q#LN12 +does not apply). It resolves when the server has finished elaborating the +document. + +Two uses, in order of importance: + +1. **Deterministic acceptance.** Lean elaboration is slow and + asynchronous; a test that sleeps is flaky and a test that polls is + slow. This is the seam that makes a live `lake serve` smoke + deterministic when a toolchain happens to be present. +2. A `M-x lean-wait-for-diagnostics` command, and a gate for the goal + panel's "elaborating" state (Q#LN13) that is cheaper than parsing + `$/lean/fileProgress` ranges. + +Sent through `pmacs.lsp.send_request` and awaited through the Q#LN9 +notification/response seam. ~20 lines. + +### Q#LN17 — Lean in markdown fences (Stage 1) + +The injection engine (#122) resolves fence names through +`pmacs.parse.injection_aliases`, a case-folded, Lua-extensible map +snapshotted into `ParseRequest`. Register `lean` and `lean4` → `lean4`. + +Two lines, and it is the one place where the Lean 3 spelling is +deliberately *not* normalized away: a ` ```lean ` fence is overwhelmingly +Lean 4 in practice, and mapping it to the `lean4` grammar is right. + +`lean4-mode` does the equivalent through `markdown-code-lang-modes`. Being +in Stage 1 means Lean blocks in this repo's own docs highlight from the +first PR. + +### Q#LN18 — `#eval` / `#check` output channel (Stage 6) + +Per §2.10, Lean's command output arrives as information-severity +diagnostics and pmacs squiggles them, signs them in the gutter, and counts +them in the modeline. VS Code shows them in the infoview instead. This +stage routes them. + +Decision: **a per-server severity policy on the spec, not a Lua filter.** +The publish path absorbs into the Rust `DiagnosticStore` before Lua sees +the notification, so a Lua-side filter would suppress the *display* while +leaving the store's counts wrong. Add an optional +`diagnostic_severity_policy` to `LspServerSpec` — default "all severities +to the store", which is a no-op for every existing language — and have the +Lean config route `Information` to the output channel only. + +The channel itself is a `*lean-output*` buffer using the same read-only +generated-buffer idiom as Q#LN13, appended to in position order and +cleared per publish for the owning document. + +Deliberately *not* merged into the goal panel: a goal is a property of the +point, output is a property of the file, and the two refresh on different +triggers. Merging them is what makes VS Code's infoview complicated. + +### Q#LN19 — Module hierarchy (Stage 7) + +`$/lean/prepareModuleHierarchy` at the point returns hierarchy items; +`$/lean/moduleHierarchy/imports` and `.../importedBy` expand one in either +direction. Rendered with `pmacs.listview.open{ name, header, rows, +on_visit, on_refresh, display = "panel" }` (`listview.lua:111`) — the same +panel the LSP references/outline views already use. + +`prepareModuleHierarchy` is position-bearing, so it goes through the +Q#LN12 typed-request path; the two expansion calls take an item, not a +position, and can use `send_request` directly. + +Last stage because it is the least load-bearing: it is navigation +convenience, and nothing else in the arc depends on it. + +## 4. Stage boundaries and why this order + +Each stage is one branch, one PR, and is independently useful if the next +never lands. + +| Stage | Ships | Substrate risk | Depends on | +|---|---|---|---| +| 1 | grammar, mode, comments, pairs, md fences | new crate; **global capture table** | — | +| 2 | multi-root server affinity | **`ensure_server`, shared by every language** | — | +| 3 | `lake serve` + probe/latch, Lake root, notification seam, `waitForDiagnostics` | two `lsp.lua` generalizations | 1, 2 | +| 4 | Unicode input method | **refactors `pair.lua`'s provenance read** | 1 | +| 5 | goal panel | new typed LSP request; panel adopter | 3 | +| 6 | `#eval` / `#check` output channel | **new `LspServerSpec` policy field** | 3, 5 | +| 7 | module hierarchy | listview adopter + one typed Rust request | 3 | + +Three of the seven carry risk that is *not* about Lean — stages 1, 2, 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 3 sees only Lean. + +Ordering notes: + +- **Stage 2 has no Lean in it and could ship independently of this arc.** + It is sequenced here because Lean is the language that makes its absence + a correctness bug rather than an inconvenience, and because Stage 3's + acceptance would otherwise have to encode the broken behavior. +- **Stage 4 does not depend on stages 2–3** 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 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. + +Stage 1 is deliberately shippable alone. If the arborium grammar turns out +to be worse in practice than its query suggests (see §5, bet 3), that is +discovered at Stage 1 for the cost of Stage 1 — and stages 2 through 7 are +almost entirely independent of grammar quality, since they are driven by +the language server rather than the parse tree. + +## 5. Categorical bets + +Stated so they can be scored, per house style. + +1. **`arborium-lean`'s ABI-15 parser loads under `tree-sitter 0.26` with a + single `tree-sitter` in the graph.** Falsified by `cargo tree -d` + showing a duplicate, or by the loader failing `Parser::set_language`. + Confidence: high — `tree-sitter-language 0.1` exists precisely for this + and roughly fifteen shipped grammars already rely on it. +2. **No protocol change in any stage.** Falsified by any new wire variant. + Confidence: high. +3. **The grammar is good enough that highlighting reads as correct on + ordinary Lean, including Mathlib-style files.** This is the weakest bet + in the lane, and the upstream author's own warning is the reason: Lean's + syntax is user-extensible via macros, so a static grammar necessarily + mis-parses custom notation. Scored against a real fixture set at Stage 1 + acceptance. If it fails, Stage 1 still ships — degraded highlighting on + exotic notation is strictly better than none — but the framing is + revised to say so plainly rather than overselling it. +4. **`$/lean/plainGoal` alone is a useful goal view, without the + `$/lean/rpc/*` widget stack.** Confidence: medium-high — it is exactly + what `lean4-mode` shipped for years before infoview widgets, and + `hasWidgets? = false` is a supported client posture, not a hack. +5. **The abbreviation expander needs no Rust.** Falsified if the one-shot + provenance refactor (Q#LN10) cannot be done in Lua, or if `buf:replace` + 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 seven 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` + output, module hierarchy, correct multi-package roots. What does + **not**: interactive/collapsible goals, `Try this` code-action + suggestions, widgets, the term-mode goal on hover, and the + `$/lean/rpc/*` session that powers all of them. That gap is real and + is the arc's eventual destination (§6) — a framing that claimed parity + without it would be overselling. +7. **Stage 2's affinity change breaks no existing language.** Falsified by + any regression in the Rust/Python/Go/TS acceptance suites, or by a + user's hand-spawned server no longer being adopted in a way they + relied on. Confidence: medium-high for the suites, deliberately lower + for hand-spawned servers — Q#LN15's comparison rule changes that case + on purpose, and the acceptance pins it rather than hiding it. + +## 6. Deferred (named) + +Pruned in round 2 — seven former entries are now stages 1–7 (see §0.1). +What remains deferred: + +- **Interactive infoview** — `$/lean/rpc/{connect,call,release,keepAlive}`, + widgets, collapsible goal trees, `Try this` code actions, term-mode goal + on hover. **This is the arc's eventual destination, not a rejection.** + It needs `hasWidgets? = true`, a real RPC session lifecycle with + keep-alive, and a rendering surface for structured rather than plain + goals — plausibly its own multi-stage arc once stages 1–7 are in. Bet 6 + scores what its absence costs. +- **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. +- **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 + live in a way it was not before. +- **Block-comment toggle** (`/- -/`) and **docstring awareness** + (`/-- -/`) — confirmed as owned by the comment arc's framing, not this + one. +- **`.olean` / `.ilean` handling** (Q#LN3). +- **Lean 3 support** — `.lean` files predating Lean 4 will mis-parse. + Out of scope permanently; Lean 3 is end-of-life. + +## 7. Acceptance + +**Stage 1** + +1. `cargo tree -d` shows exactly one `tree-sitter` version after adding + `arborium-lean`. +2. A `.lean` fixture parses: the loader produces a tree whose root node is + `module` and which is not all-ERROR. +3. Opening `foo.lean` sets `pmacs.buffer.major_mode` to `lean4`. +4. An Emacs `-*- mode: lean -*-` modeline and a Vim `ft=lean` modeline both + resolve to `lean4`. +5. Highlighting produces non-default styles for a comment, a `def` name, a + `theorem` name, a string, and a numeric literal in the fixture. +6. `(sorry)` picks up the `warning` style. +7. **Reverse-direction positive pin (#146).** Every language the four new + capture entries reach asserts its *expected delta* — not that nothing + moved, since these languages necessarily move: + - `rust`, `python`, `javascript`, `javascriptreact`, `typescript`, + `typescriptreact`: a capitalized identifier (`Some`, `MyClass`) picks + up the `constructor` style. All seven entries are covered because + `HIGHLIGHT_QUERY` composition means the JS-family entries inherit the + rule rather than restating it — a regression in composition would + otherwise go unseen. + - `lua`: a table literal's `{` and `}` pick up the `constructor` style. + - `zig`: a character literal picks up `character`; a conditional picks + up `keyword.conditional`. + - `cmake`: a conditional picks up `keyword.conditional`. +8. **Reverse-direction negative pin.** Fixtures in languages verified to + emit **none** of the four capture names render byte-identically to + their pre-change baseline: `markdown`, `json`, `yaml`, `html`, `css`, + `c`, `cpp`, `go`, `toml`, `bash`. + + Rev 1 named Lua and Python here, which was a self-contradiction: both + are retro-painted by `constructor`, so a fixture that did not move + would have been vacuous — the #155 R2 assertion shape. Whichever + fixtures ship, the negative pin must be shown non-vacuous by + confirming it *fails* when a capture the language does emit is added. +9. `M-;` comments and uncomments a Lean line with `--`. +10. Typing `⟨` inserts `⟨⟩` with the point between; likewise `⦃` and `⟮`. + Typing `'` after an identifier does **not** pair. +11. A ` ```lean ` fence and a ` ```lean4 ` fence in a markdown buffer both + highlight as Lean (Q#LN17); a fence with an unknown name still does + not. +12. **No live toolchain required.** The whole Stage 1 suite passes on a + machine with no `lean`, no `lake`, and no configured elan toolchain + (§2.9) — Stage 1 touches no process at all. + +**Stage 2 — multi-root affinity (no Lean content)** + +13. `pmacs.lsp.list()` rows carry `root_uri` and `cwd`. +14. Two files of the **same language in different project roots** spawn + **two** servers, each with its own `rootUri`. Exercised with the fake + server so it is toolchain-free. +15. Two files of the same language in the **same** root reuse **one** + server — the pre-change behavior, pinned so the fix does not become + "always spawn". +16. **Regression pin, per language:** the existing Rust, Python, Go, and + TypeScript attach paths behave unchanged for the single-root case + that is all they exercised before. +17. **Hoist pin:** `project_root_for` is called on the reuse path, and a + function-valued `root` is invoked at most once per directory per + session (Q#LN15's memoization) rather than once per attach. +18. **Hand-spawned server pin:** a server spawned from `init.lua` with + `cwd` but no `root_uri` is *not* adopted by a root-bearing attach — + the deliberate behavior change, asserted rather than discovered. +19. A crashed or stopped server in the matching root is not reused; a new + one spawns. +20. **Loose-file pin (Q#LN15 part 2).** Two **markerless** files of the + same language in **different** directories still share **one** server. + This is the no-change case, and it is the one a naive `(language_id, + root)` key breaks — `project_root_for` never returns nil for a file + with a path, so it must be asserted, not assumed. +21. **Fallback-vs-detected pin.** A file under a real project marker and a + markerless file of the same language get **different** servers, and + the markerless one's server carries the fallback directory as `cwd` + while matching on a nil affinity key. + +**Stage 3 — the Lean language server** + +22. Opening a `.lean` file inside a Lake package spawns one server with + `cwd` and `rootUri` at the package root. +23. **Outermost-root pin:** a file under + `/.lake/packages/dep/…` whose ancestor chain contains two + `lean-toolchain` files resolves to ``, not to `dep`. Run with + `pmacs.project.set_search_boundary` at the fixture root so the + assertion is hermetic. +24. **Boundary pin:** with the search boundary set at the fixture root, a + `lean-toolchain` planted in an ancestor *above* the boundary is not + reached — the resolver stops at the boundary rather than walking past + it. +25. A string-valued `pmacs.lsp.config.lean4.root` still works — the Q#LN8 + generalization is strictly additive. +26. `didOpen` carries `languageId = "lean4"`. +27. **Fallback-latch pin (Q#LN7):** a `lake` stub that exits non-zero — + reproducing §2.9's shimmed-elan state — causes exactly **one** restart + against `lean --server`, and a second failure surfaces an error rather + than looping. The latch does not re-arm within the session. +28. **Probe pin:** a `lake` stub reporting version 3.0.0 triggers the + fallback; one reporting 3.1.0 does not. A stub that never exits does + not block the attach — the optimistic `lake serve` spawn proceeds. +29. A `$/lean/fileProgress` notification delivered through the fake server + reaches a registered `on_notification` subscriber. +30. **Dispatch-integrity pin:** with a Lean subscriber registered, a + `workspace/applyEdit` request in the same drain is still handled — no + event is stolen. +31. A subscriber that raises does not prevent later events in the same + drain from being processed. +32. **Response-seam pin (Q#LN9).** A `send_request` reply reaches its + registered `on_response` one-shot, and the one-shot is **removed + before** invocation — a raising handler is not re-entered. Bites + against rev 2, where no Lua consumed `ev.kind == "response"` at all + and the reply was dropped. +33. **Response dispatch-integrity pin.** With a response subscriber + registered, `workspace/applyEdit` in the same drain is still handled; + a raising response handler does not stop later events in that drain. + Mirrors the notification-side pins above. +34. **Pending-purge pin.** A server that dies with a response outstanding + invokes the pending one-shot with an error and clears it — the + registration does not leak and the awaiting caller does not hang. +35. **Config-preservation pin (Q#LN7).** After the fallback latch fires, + user-supplied `env` / `settings` / `init_options` / `root` on + `pmacs.lsp.config.lean4` survive; only `command` and `args` change. +36. **No-respawn-loop pin.** The latch stops the failing server before + spawning the fallback, so `RestartPolicy` does not respawn the broken + command underneath it. +37. `textDocument/waitForDiagnostics` resolves through the response seam + (Q#LN16). **PATH-and-success-gated live smoke:** if `lake serve` + starts successfully a real elaboration completes and diagnostics + arrive; skipped otherwise, never failed. + +**Stage 4 — the Unicode input method** + +38. `\alpha` + space yields `α`; the whole expansion is a single undo step. +39. `\<>` yields `⟨⟩` with the point between them, from the `$CURSOR` + placeholder. +40. **Pair-collision pin (Q#LN10).** `\[[]]` 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 + 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. +43. Moving the cursor out of a pending abbreviation abandons it. +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. + +**Stage 5 — the goal view** + +47. `$/lean/plainGoal` is sent with a position encoded through + `outbound_position` — pinned with a UTF-16 fake server and a + non-ASCII Lean line, which fails against a raw byte column. +48. A non-null `PlainGoal` renders `rendered` into `*lean-goal*`. +49. A null result with the file elaborated renders "no goals". +50. A point inside a range still covered by `$/lean/fileProgress` renders + the elaborating state, not "no goals". +51. **Refresh pin (Q#LN13).** Moving the point to a new position and + driving `process.after-tick` past the debounce issues exactly one new + `$/lean/plainGoal`; ticking again with the point unmoved issues none. +52. **In-flight pin.** A second point move while a request is outstanding + does not issue a concurrent request, and the panel ends on the result + for the *latest* position — a stale response for an abandoned + position never wins. +53. The panel opens at the bottom without stealing focus. +54. `*lean-goal*` rejects a user edit and accepts a module write. +55. **Teardown pin.** After the Lean buffer is killed or the frontend + detaches, driving `process.after-tick` issues **no** further + `$/lean/plainGoal` and writes **nothing** to the panel, and any + outstanding request's one-shot has been purged. + + Worded as an observable because it must be: `pmacs.hook` exposes + `add` / `define` / `list` / `run` and **no `remove`**. A subscription + cannot be torn down, only made inert — so "leaves no subscription" + (rev 2's wording) is untestable and, taken literally, unimplementable. + +**Stage 6 — the output channel** + +56. An information-severity diagnostic from the **Lean** server lands in + `*lean-output*` and **not** in the diagnostic store: no squiggle, no + gutter sign, and the modeline info count stays zero. +57. Warning- and error-severity diagnostics from the Lean server are + unaffected and still reach the store. +58. **Cross-language pin:** an information-severity diagnostic from a + **non-Lean** server still squiggles and still counts — the + `LspServerSpec` policy defaults to a no-op. +59. Output is cleared per publish for the owning document, so a + re-elaborated file does not accumulate stale `#eval` results. +60. Output rows appear in source-position order regardless of publish + order. + +**Stage 7 — module hierarchy** + +61. `$/lean/prepareModuleHierarchy` is sent through the Q#LN12 typed path + (position-bearing), pinned against a UTF-16 fake server. +62. `imports` and `importedBy` each render into the listview panel and are + navigable through the existing `on_visit`. +63. An empty result renders an empty panel with its header, not an error. +64. The panel's `q` returns to the originating buffer, not to another + panel (`listview.lua:118`'s existing rule). + +## 8. Prior art in pmacs + +- **#144 (LaTeX)** — the third-party-republish grammar decision and the + vendored-artifact-with-provenance pattern. +- **#146 (HTML+CSS)** — the global capture table, and the requirement to + pin retro-paint in both directions. Q#LN4 is that lesson applied. +- **#123 (JSON/YAML)** — declarative `pmacs.lsp.config` entries with a + fake-server delivery proof plus PATH-gated live smokes. Stage 3 follows + 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. +- **#127 (config registry)** — `pmacs.config.define` and the + source-buffer-resolution correction. Q#LN10's gate follows + `editing.auto-pair` exactly. +- **#129 (mode system)** — mode-scoped keymaps for Stage 5. +- **#155 (bottom panel)** — `pmacs.window.display` and the panel adopter + shape, for stages 5–7. +- **#113 (compile mode)** — the erroring-intercept read-only generated + buffer idiom (stages 5 and 6), and `process.after-tick` as a debounced + cadence source (Q#LN13). +- **#122 (multi-language injections)** — `pmacs.parse.injection_aliases`, + which Q#LN17 registers into. +- **#94/#95 (LSP panels)** — `pmacs.listview.open` and the + references/outline panel shape that Stage 7 reuses wholesale.