From a38296583b81c83848c0217e8d76765b4173e8c7 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:44:53 -0400 Subject: [PATCH 1/6] 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. From 6ea8d2756e551dc1b33015c53b0b1e792ca53f5c Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:49:01 -0400 Subject: [PATCH 2/6] feat(syntax): bundle the Lean 4 grammar (Arc 8 Stage 1, Q#LN1-3) Adds `arborium-lean` 2.18 and one `BUILTIN_LANGUAGES` entry, closing the framing's open verification obligation on the crate choice. Why this crate and not `tree-sitter-lean4` (Q#LN1): the latter depends on `tree-sitter = "0.25"` directly rather than the shared `tree-sitter-language` ABI crate, and `^0.25` excludes our 0.26, so it would fork the graph exactly as the dead `tree-sitter-dockerfile` does. It also exports only `pub fn language()` while its README advertises a `LANGUAGE` const that does not exist, and its package `include` omits `queries/` so it ships no highlights at all. `arborium-lean` uses `tree-sitter-language 0.1` as its sole runtime dep, ships a pre-generated ABI-15 parser plus scanner, and exports real query constants. `cargo tree -d` reports no duplicate `tree-sitter`. The entry is named `lean4`, not `lean` (Q#LN2): `ensure_server` passes `LanguageEntry.name` through as the `didOpen` language_id, and the Lean ecosystem's id is `lean4` -- `lean` is Lean 3, which is end-of-life. It claims `.lean` only; `.olean` is a compiled binary and `.ilean` is JSON metadata (Q#LN3). Four tests. The load-bearing one is `lean4_grammar_loads_and_parses`, which discharges the half of Q#LN1 that could not be settled by reading: `arborium-lean` exports `const fn language() -> LanguageFn` rather than the `LANGUAGE` const every other entry uses, and its README demonstrates usage against a patched tree-sitter core. Neither is supposed to matter, but "supposed to" is not evidence. The fixture parses without error, and -- the part that actually guards a misbuild -- its Unicode operators produce structure rather than degrading silently: the grammar must see a `(arrow)` for the arrow, a `(forall)` for the universal quantifier, and a `(comparison)` for the inequality. The error-free claim is deliberately scoped to the committed fixture. Lean's syntax is user-extensible via macros, so a static grammar mis-parses some legal input by construction; the framing scores that as bet 3 rather than the doc overselling it. Co-Authored-By: Claude Opus 5 (1M context) --- Cargo.lock | 33 ++++++++++ Cargo.toml | 18 ++++++ src/syntax.rs | 170 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 221 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index d7caff6..498f267 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -169,6 +169,27 @@ dependencies = [ "x11rb", ] +[[package]] +name = "arborium-lean" +version = "2.18.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "80b795046d03aae5780c58e746ddaf780f683e36d9efa8f67abbe9bc01299eb5" +dependencies = [ + "arborium-sysroot", + "cc", + "tree-sitter-language", +] + +[[package]] +name = "arborium-sysroot" +version = "2.18.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "59d99d80550b726f9dec7ee6d07118c31e08b10e729ac488eabd4c10603dc841" +dependencies = [ + "cc", + "dlmalloc", +] + [[package]] name = "arrayref" version = "0.3.9" @@ -747,6 +768,17 @@ dependencies = [ "libloading", ] +[[package]] +name = "dlmalloc" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" +dependencies = [ + "cfg-if", + "libc", + "windows-sys 0.61.2", +] + [[package]] name = "document-features" version = "0.2.12" @@ -2538,6 +2570,7 @@ checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" name = "pmacs" version = "1.0.0" dependencies = [ + "arborium-lean", "codebook-tree-sitter-latex", "crossbeam", "crossterm", diff --git a/Cargo.toml b/Cargo.toml index 589ccaf..4e21592 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -241,6 +241,24 @@ codebook-tree-sitter-latex = "0.6" # engine (see `crate::syntax::BUILTIN_LANGUAGES`). tree-sitter-html = "0.23" tree-sitter-css = "0.25" +# Lean 4 (`.lean`) — Arc 8 Stage 1 (`docs/lean4-mode-framing.md`, Q#LN1). +# `leanprover` ships no tree-sitter grammar (Lean parses with its own +# kernel), so both candidates are third-party. The obvious-looking +# `tree-sitter-lean4` is NOT usable: it depends on `tree-sitter = "0.25"` +# DIRECTLY rather than the shared `tree-sitter-language` ABI crate, which +# `^0.25` makes incompatible with our 0.26 and would fork the graph (the +# same defect that rules out `tree-sitter-dockerfile` above); it exports +# only `pub fn language()` while its README advertises a `LANGUAGE` const +# that does not exist; and its package `include` omits `queries/`, so it +# ships no highlights at all. `arborium-lean` is a republish from the +# arborium grammar collection that does it correctly: `tree-sitter-language +# 0.1` as its sole runtime dep, a pre-generated ABI-15 `parser.c` plus +# `scanner.c` (no CLI at build time), and `HIGHLIGHTS_QUERY` / +# `INJECTIONS_QUERY` / `LOCALS_QUERY` constants. Note the shape: it exports +# `const fn language() -> LanguageFn`, so the entry in +# `crate::syntax::BUILTIN_LANGUAGES` reads `arborium_lean::language().into()` +# rather than the `LANGUAGE.into()` every other entry uses. +arborium-lean = "2.18" # T M4.4 process supervisor: signal sending without `unsafe`. Keep # the feature surface tight to keep build time low. `poll` feeds the # compile-mode group readers (cancellable poll-based reads, Q#CM3). diff --git a/src/syntax.rs b/src/syntax.rs index efbbd4d..edec588 100644 --- a/src/syntax.rs +++ b/src/syntax.rs @@ -1130,6 +1130,33 @@ pub const BUILTIN_LANGUAGES: &[LanguageEntry] = &[ locals_query: &[], injections_query: &[], }, + // Lean 4 (framing `docs/lean4-mode-framing.md`, Arc 8 Stage 1). + // + // The entry is named `lean4`, not `lean` (Q#LN2): this name becomes the + // `language_id` sent in `didOpen` — `ensure_server` at + // `builtin/runtime/lsp.lua:540` passes it straight through — and the + // Lean ecosystem's id is `lean4` (`lean` is Lean 3, which is + // end-of-life). The grammar's own C symbol is `tree_sitter_lean`; that + // is arborium's business, not ours. Stage 3 adds + // `pmacs.lsp.config.lean4` against this name. + // + // Note the loader shape: `arborium-lean` exports `const fn language() -> + // LanguageFn` rather than a `LANGUAGE` const, so this is the one entry + // that calls a function to get the `LanguageFn` before `.into()`. + // + // `.olean` (compiled artifacts) and `.ilean` (JSON metadata) are + // deliberately unclaimed (Q#LN3). Locals and injections are empty + // because the crate ships both as empty strings — Lean has no embedded + // sublanguage worth injecting, and its scoping is far beyond what a + // tree-sitter locals query could model. + LanguageEntry { + name: "lean4", + extensions: &["lean"], + loader: || arborium_lean::language().into(), + highlights_query: &[arborium_lean::HIGHLIGHTS_QUERY], + locals_query: &[], + injections_query: &[], + }, ]; /// LaTeX highlights overlay (framing Q#LX2). The chosen grammar crate @@ -2394,6 +2421,149 @@ mod tests { } } + #[test] + fn builtin_languages_include_lean4() { + // Framing acceptance 1/3 (`docs/lean4-mode-framing.md`). The entry is + // named `lean4` because that name becomes the `didOpen` language_id + // (Q#LN2), and it claims `.lean` ONLY: `.olean` is a compiled binary + // artifact and `.ilean` is JSON metadata (Q#LN3). + let lean = BUILTIN_LANGUAGES + .iter() + .find(|l| l.name == "lean4") + .expect("`lean4` language entry must be present"); + assert!(lean.extensions.contains(&"lean"), "`lean4` claims `.lean`"); + for unclaimed in ["olean", "ilean"] { + assert!( + !lean.extensions.contains(&unclaimed), + "`lean4` must not claim `.{unclaimed}`" + ); + } + assert!( + lean.highlights_query + .contains(&arborium_lean::HIGHLIGHTS_QUERY), + "`lean4` drives highlighting from the crate's query constant, not an overlay" + ); + assert!( + lean.locals_query.is_empty() && lean.injections_query.is_empty(), + "`lean4` ships neither locals nor injections (Q#LN1)" + ); + } + + #[test] + fn lean4_grammar_loads_and_parses() { + // Framing acceptance 2 and the open half of Q#LN1: `arborium-lean` + // exports `const fn language() -> LanguageFn` (not the `LANGUAGE` + // const every other entry uses) over `tree-sitter-language 0.1`, and + // its README demonstrates usage against a `tree_sitter_patched_ + // arborium` core. Neither is supposed to matter — the LanguageFn ABI + // is shared — but "supposed to" is not evidence, so this pins that + // OUR `tree-sitter` 0.26 core accepts it and produces a real tree. + // + // The fixture exercises the grammar's external scanner (`scanner.c` + // supplies a NEWLINE token, so layout-sensitive `def`/`theorem` + // bodies depend on it) and the Unicode operators that make Lean + // Lean — `→`, `∀`, `≥` — which a byte-oriented misbuild would shred. + let reg = SyntaxRegistry::new(); + let language = reg + .language("lean4") + .expect("`lean4` language loads from BUILTIN_LANGUAGES"); + let mut buf = fresh_buffer("Basic.lean"); + buf.apply_edit(EditOp::Insert { + pos: 0, + bytes: "-- a comment\n\ + def fibonacci : Nat → Nat\n\ + \x20 | 0 => 0\n\ + \x20 | n + 1 => n\n\ + \n\ + theorem fib_nonneg : ∀ n, fibonacci n ≥ 0 := by\n\ + \x20 intro n\n\ + \x20 exact Nat.zero_le _\n" + .as_bytes(), + }) + .unwrap(); + let view = ParseView::new(&buf, language, "lean4".to_owned()); + let handle = view.handle(); + let _vid = buf.attach_view(Box::new(view)); + let bundle = parse_synchronously(&handle); + assert_eq!( + bundle.root_tree().root_node().kind(), + "module", + "Lean grammar roots at module" + ); + let sexp = bundle.root_tree().root_node().to_sexp(); + // This specific committed fixture parses cleanly. The claim is + // scoped to the fixture on purpose: Lean's syntax is user-extensible + // via macros, so a static grammar necessarily mis-parses some legal + // input (the upstream grammar says so itself, and the framing scores + // it as bet 3). What a clean parse HERE proves is that the crate is + // wired correctly, not that Lean is fully parseable. + assert!( + !bundle.root_tree().root_node().has_error(), + "the fixture parses without error; got {sexp}" + ); + // `def` and `theorem` sit under a `declaration` wrapper, not directly + // under `module`. + for expected in ["(comment)", "(def ", "(theorem "] { + assert!( + sexp.contains(expected), + "expected `{expected}` in the tree; got {sexp}" + ); + } + // The load-bearing part of this test. A grammar built against a + // mismatched core, or one whose scanner mis-handles multibyte input, + // does not fail loudly — it produces a tree that silently degrades on + // exactly the characters Lean is made of. `→` must become an `arrow`, + // `∀` a `forall`, and `≥` a `comparison`; if these three hold, the + // UTF-8 path through the parser is sound. + for expected in ["(arrow ", "(forall ", "(comparison "] { + assert!( + sexp.contains(expected), + "Unicode operator did not produce `{expected}`; got {sexp}" + ); + } + } + + #[test] + fn lean4_highlights_resolve() { + // The crate's 213-line query must COMPILE against the grammar it + // ships with — the node-name compatibility gate. A query referencing + // a node this grammar version lacks fails here rather than silently + // producing no spans at runtime. + let reg = SyntaxRegistry::new(); + let query = reg + .highlights_query("lean4") + .expect("lean4 highlights compile against the grammar"); + let names = query.capture_names(); + // The four capture names Q#LN4 adds to the GLOBAL theme table are + // present here — this is the forward direction of that decision; the + // reverse direction (what they do to other languages) is pinned in + // `highlight.rs`. + for expected in ["constructor", "character", "keyword.conditional", "warning"] { + assert!( + names.contains(&expected), + "lean4 query uses `@{expected}`, which Q#LN4 adds to the theme; got {names:?}" + ); + } + } + + #[test] + fn language_for_path_resolves_lean_extension() { + let reg = SyntaxRegistry::new(); + assert_eq!( + reg.language_name_for_path("Mathlib/Data/Nat/Basic.lean") + .as_deref(), + Some("lean4"), + "`.lean` resolves to the lean4 grammar" + ); + for unclaimed in ["Basic.olean", "Basic.ilean"] { + assert_ne!( + reg.language_name_for_path(unclaimed).as_deref(), + Some("lean4"), + "{unclaimed} must not resolve to lean4" + ); + } + } + #[test] fn builtin_languages_include_html_and_css() { // Both crate grammars export their query constants (no overlay). HTML From 5207d40cafb633aa994b17ebf251694a76e4ce0c Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:51:27 -0400 Subject: [PATCH 3/6] feat(theme): add the four Lean 4 capture entries (Arc 8 Stage 1, Q#LN4) `constructor`, `character`, `keyword.conditional`, and `warning` are the captures the Lean query uses that the global theme table lacked. Three of them are not Lean-only, so this is a deliberate retro-paint of already shipped languages -- the #146 lesson applied on purpose rather than discovered afterwards. The blast radius, measured rather than assumed: * `constructor` reaches SEVEN language entries, not four. The emitting crates are rust, lua, python and javascript, but `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated base-first into javascriptreact, typescript and typescriptreact as well. * Its shape is not "constructors". rust/python/javascript tag every capitalized identifier (`#match? "^[A-Z]"`); lua tags every table-constructor brace. So this recolors `None`, every class-cased name, and every Lua `{}` -- all of which rendered as unstyled default text before. * `character` reaches zig only; `keyword.conditional` reaches cmake and zig, which previously flattened it to `keyword`; `warning` reaches no other grammar and exists for Lean's `sorry`. The alternative was an in-repo overlay renaming the captures (the #144 LaTeX pattern), which forks a 213-line query we would then own and hand-merge on every crate bump. There is no middle option: styling Lean's constructors without touching the other seven entries requires renaming the capture, which requires the overlay. Pinned in both directions, per #146: * the positive breadth pin asserts all seven entries emit `@constructor` at the QUERY level -- chosen over per-fixture checks because the base-query composition is the fragile part; if someone stops concatenating the JS base into `typescript`, this fails while any single-language fixture still passes; * two grid pins prove the theme entry reaches painted cells, and a third records that a variant in CALL position keeps `@function` -- the difference between "capitalized identifiers recolor" and "enum variants recolor", only the first of which is true; * the negative pin asserts ten languages (markdown, json, yaml, html, css, c, cpp, go, toml, bash) emit none of the four names, with a non-vacuity check that the same predicate finds each name where it does occur. Rev 1 of the framing named Lua and Python in that negative pin, which was a self-contradiction -- both are retro-painted by `constructor`, so the assertion would have been vacuous in the #155 R2 shape. Review round 1 caught it. Full lib suite (1,824) and the required-GPU gate (152) pass unchanged, so no existing assertion depended on these captures being unstyled. Co-Authored-By: Claude Opus 5 (1M context) --- src/highlight.rs | 193 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 193 insertions(+) diff --git a/src/highlight.rs b/src/highlight.rs index 2c7369f..633ec6f 100644 --- a/src/highlight.rs +++ b/src/highlight.rs @@ -174,6 +174,41 @@ impl Theme { // prefix-walks to `tag`. ("tag", fg(5)), ("attribute", fg(3)), + // Lean 4 (framing Q#LN4). These four are the captures the Lean + // query uses that the set above lacks — but three of them are + // NOT Lean-only, and adding them here changes languages that + // already ship. That is the #146 lesson (`attribute`, above, + // retro-painted rust/lua/yaml) and it is deliberate, not + // incidental: + // + // * `constructor` reaches SEVEN entries — rust, lua, python, + // javascript, and (because `tree_sitter_javascript:: + // HIGHLIGHT_QUERY` is concatenated base-first into them) + // javascriptreact, typescript, typescriptreact. Its shape is + // not "constructors": rust/python/javascript tag every + // capitalized identifier (`#match? "^[A-Z]"`), and lua tags + // every table-constructor brace. So this recolors `Some`, + // `None`, `Ok`, `Err`, every class-cased name, and every Lua + // `{}`. All of those render as unstyled default text today. + // * `character` reaches zig only. + // * `keyword.conditional` reaches cmake and zig, which + // currently flatten it to `keyword`; giving it + // `keyword.control`'s style makes their conditionals read the + // way rust's already do. + // * `warning` reaches no other grammar. It exists for Lean's + // `sorry` — an unproved goal, the single most important thing + // to see in a proof file. + // + // The alternative was an in-repo query overlay renaming these + // into the existing vocabulary (the #144 LaTeX pattern), which + // would fork a 213-line query we would then own and hand-merge + // on every crate bump. There is no middle option: styling Lean's + // constructors without touching the other seven entries requires + // renaming the capture, which requires the overlay. + ("constructor", fg(11)), + ("character", fg(2)), + ("keyword.conditional", fg_bold(13)), + ("warning", fg_bold(1)), ]; let by_capture = entries .iter() @@ -1484,6 +1519,164 @@ mod tests { ); } + /// Paint `src` as `language` into a one-row grid and return the style + /// at column `col`. Shared by the Q#LN4 retro-paint pins below. + fn painted_fg_at( + language_name: &str, + file: &str, + src: &str, + col: u32, + ) -> pmacs_protocol::cell::Color { + use crate::buffer::{Buffer, BufferId, EditOp}; + use crate::cell::{Cell, CellSize}; + use crate::syntax::{ParseView, SyntaxRegistry}; + + let reg = SyntaxRegistry::new(); + let language = reg.language(language_name).expect("grammar loads"); + let mut buf = Buffer::new(BufferId::next(), file); + buf.apply_edit(EditOp::Insert { + pos: 0, + bytes: src.as_bytes(), + }) + .unwrap(); + let view = ParseView::new(&buf, language, language_name.to_owned()); + let handle = view.handle(); + let _vid = buf.attach_view(Box::new(view)); + let mut req = handle.make_request(); + req.injection_aliases = reg.injection_alias_snapshot(); + let bundle = crate::syntax::run_parse(req).expect("parse"); + handle.install(reg.resolve_layer_queries(&bundle)); + + let mut hv = SyntaxHighlightView::new(handle, reg.theme()); + let (rows, cols) = (1usize, 40usize); + let mut backing: Vec = vec![Cell::default(); rows * cols]; + let mut grid = CellGrid { + cells: &mut backing, + stride: cols as u32, + size: CellSize::new(rows as u32, cols as u32), + }; + let viewport = Viewport { + buffer_start: 0, + buffer_end: u64::MAX, + cell_origin: CellCoord::new(0, 0), + cell_size: CellSize::new(rows as u32, cols as u32), + gutter_w: 0, + folds: None, + }; + hv.render(&buf, viewport, &mut grid); + grid.get(CellCoord::new(0, col)).style.fg + } + + /// Does `language`'s compiled highlight query use `capture`? + fn query_uses_capture(language: &str, capture: &str) -> bool { + let reg = crate::syntax::SyntaxRegistry::new(); + let Some(query) = reg.highlights_query(language) else { + panic!("{language} has no highlights query"); + }; + query.capture_names().contains(&capture) + } + + #[test] + fn lean4_constructor_capture_retro_paints_the_whole_javascript_family() { + // Framing acceptance 7 (Q#LN4), the breadth half. `constructor` was + // added for Lean, but four crates emit it — and because + // `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated + // base-first into the react/typescript entries + // (`src/syntax.rs`), it reaches SEVEN language entries, not four. + // + // Asserted at the query level rather than per-fixture precisely + // because the composition is the fragile part: if someone stops + // concatenating the JS base query into `typescript`, this fails + // while any single-language fixture would still pass. + for language in [ + "rust", + "lua", + "python", + "javascript", + "javascriptreact", + "typescript", + "typescriptreact", + ] { + assert!( + query_uses_capture(language, "constructor"), + "`{language}` emits @constructor, so Q#LN4's entry retro-paints it" + ); + } + } + + #[test] + fn lean4_capture_additions_paint_rust_constructors_and_lua_braces() { + // Framing acceptance 7, the "actually reaches painted cells" half — + // a query-name check alone would not prove the theme entry resolves. + // Both of these rendered as unstyled default text before Q#LN4. + use pmacs_protocol::cell::Color; + + // `None` at col 8 — a bare capitalized identifier, which is what the + // rust query's `#match? "^[A-Z]"` tags. Note that `Some(1)` does NOT + // work here: in call position a narrower `@function` pattern wins and + // paints fg 4. The distinction is worth keeping in the test, because + // it is the difference between "capitalized identifiers recolor" and + // "enum variants recolor" — only the former is true. + assert_eq!( + painted_fg_at("rust", "a.rs", "let x = None;\n", 8), + Color::Indexed(11), + "a bare Rust capitalized identifier paints the shared @constructor style" + ); + // `Some` in pattern position (col 10) does reach @constructor. + assert_eq!( + painted_fg_at("rust", "a.rs", "match v { Some(z) => z, None => 0 };\n", 10), + Color::Indexed(11), + "a Rust pattern-position variant paints the shared @constructor style" + ); + // ...but in CALL position the narrower @function pattern wins. Pinned + // so the blast radius recorded in the framing stays accurate. + assert_eq!( + painted_fg_at("rust", "a.rs", "let e = Err(1);\n", 8), + Color::Indexed(4), + "a called variant keeps @function, not @constructor" + ); + // Lua tags the table-constructor BRACES, not a name: `{` at col 8. + assert_eq!( + painted_fg_at("lua", "a.lua", "local t = {}\n", 10), + Color::Indexed(11), + "a Lua table brace paints the shared @constructor style" + ); + } + + #[test] + fn lean4_capture_additions_do_not_reach_unrelated_languages() { + // Framing acceptance 8 — the negative pin, redrawn in review round 1. + // + // Rev 1 named Lua and Python here, which was a self-contradiction: + // both are retro-painted by `constructor`, so a "nothing moved" + // assertion over them would have been vacuous — the #155 R2 shape. + // These ten emit NONE of the four names, verified by grep over the + // crate queries in the dependency graph. + // + // Stated at the query level, which is stronger than a fixture + // snapshot: it holds for every construct in the language, not just + // the one a fixture happened to exercise. + const ADDED: [&str; 4] = ["constructor", "character", "keyword.conditional", "warning"]; + for language in [ + "markdown", "json", "yaml", "html", "css", "c", "cpp", "go", "toml", "bash", + ] { + for capture in ADDED { + assert!( + !query_uses_capture(language, capture), + "`{language}` must not emit @{capture}; Q#LN4 would silently restyle it" + ); + } + } + + // Non-vacuity: the same predicate must find each name where it DOES + // occur. Without this, a `query_uses_capture` that always returned + // false would pass the loop above. + assert!(query_uses_capture("lean4", "constructor")); + assert!(query_uses_capture("zig", "character")); + assert!(query_uses_capture("cmake", "keyword.conditional")); + assert!(query_uses_capture("lean4", "warning")); + } + #[test] fn web_grid_paints_html_tag_and_attribute() { // Q#WEB4 acceptance: the two capture entries this lane adds (`tag`, From 0c922682c0d575cc6e270c393382fe9de0364a70 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:59:48 -0400 Subject: [PATCH 4/6] feat(lean4): editing surface + Stage 1 acceptance (Q#LN5, LN6, LN17) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes Arc 8 Stage 1: the Lua-side tables that turn a recognized grammar into a usable mode, plus the acceptance suite for all twelve framing criteria. comment.lua -- `lean4 = "--"` (Q#LN5). Line comments only; Lean's block comment `/- -/` and docstring `/-- -/` belong to the comment arc's own named deferral and this lane does not front-run it. pair.lua -- `⟨⟩`, `⦃⦄`, `⟮⟯` alongside the ASCII brackets (Q#LN6). The anonymous constructor is among the most-typed constructs in Lean; omitting it would make the pair set feel broken. The other two ride along because the Stage 4 input method can produce them, and a bracket the pair set does not understand is worse than one it does. All three sit outside the nine built-in pair chars, so per Q#AP1 their undo is cross-peer-degraded -- the documented, pre-existing limitation of user-extended pairs. No `''`: Lean uses the prime as an identifier suffix (`h'`, `foo'`), the same reason Rust excludes it. syntax.lua -- the `lean` -> `lean4` modeline alias (Q#LN2), so an Emacs `-*- mode: lean -*-` or a Vim `ft=lean` line is not stranded by the entry being named `lean4`. syntax.rs -- the `lean` -> `lean4` injection alias (Q#LN17), so both ```lean and ```lean4 fences highlight. The Lean 3 spelling is mapped forward deliberately: a ```lean fence is overwhelmingly Lean 4 in practice. highlight.rs -- `warning` moves from bold red to bold BRIGHT red. Writing the test found the collision: `number` is plain `fg(1)`, so `sorry` and the literal `42` beside it were the same colour, differing only in the bold flag. `sorry` means "admitted, not proved" and is the one token in a proof file a reader must never skim past, so it now gets the loudest entry in the table and the test asserts the full style rather than the colour. Twelve criteria, seventeen tests. Notes on the ones that could have been vacuous: * acc4 uses a `.txt` fixture, not `.lean` -- on a `.lean` path the extension alone yields `lean4` and the assertion would pass with the alias table empty. acc4b removes the alias and pins that the raw name survives, so acc4 cannot silently stop testing anything. * acc11 goes through the real `_parse_now` injection path and asserts a `lean4` CHILD LAYER appears. `pmacs.parse.injection_aliases` is a documented write-only proxy, so an alias-table read would have proven nothing about the parser; acc11b pins that a misspelled fence still resolves to nothing. * acc12 asserts through the process supervisor and the server list that opening a Lean buffer spawns nothing. This is not decorative: the machine this arc was scouted on has elan installed with no default toolchain, where `lake --version` itself fails, and Stage 1 must be unaffected by that. Gates: fmt and strict workspace clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1 9, comment toggle 14, auto-pair 45, injection 4; M4 121; required GPU 152; isolated-config workspace sweep 3,150 across 90 suites; `git diff --check` clean. Co-Authored-By: Claude Opus 5 (1M context) --- builtin/runtime/comment.lua | 4 + builtin/runtime/pair.lua | 16 ++ builtin/runtime/syntax.lua | 5 + src/highlight.rs | 106 +++++++++- src/syntax.rs | 6 + tests/lean4_stage1_acceptance.rs | 320 +++++++++++++++++++++++++++++++ 6 files changed, 455 insertions(+), 2 deletions(-) create mode 100644 tests/lean4_stage1_acceptance.rs diff --git a/builtin/runtime/comment.lua b/builtin/runtime/comment.lua index 7ee91e8..a9912d6 100644 --- a/builtin/runtime/comment.lua +++ b/builtin/runtime/comment.lua @@ -39,6 +39,10 @@ pmacs.comment.strings = { sh = "#", toml = "#", yaml = "#", + -- Lean 4 (framing Q#LN5). `--` only: Lean's block comment is `/- -/` and + -- its docstring `/-- -/`, but block-comment toggling is the comment arc's + -- own named deferral and this lane does not front-run it. + lean4 = "--", } -- Start of the line containing `pos`: chunked backward scan for the diff --git a/builtin/runtime/pair.lua b/builtin/runtime/pair.lua index 6d014d4..9ed9d1f 100644 --- a/builtin/runtime/pair.lua +++ b/builtin/runtime/pair.lua @@ -62,6 +62,22 @@ pmacs.pair.sets = { markdown = { "()", "[]", "{}", '""', "``" }, sh = { "()", "[]", "{}", '""', "''" }, bash = { "()", "[]", "{}", '""', "''" }, + -- Lean 4 (framing Q#LN6). `⟨⟩` (anonymous constructor) is among the + -- most-typed constructs in Lean and omitting it would make the pair set + -- feel broken; `⦃⦄` (strict implicit binder) and `⟮⟯` ride along because + -- the Stage 4 input method can produce them (`\{{}}`, `\([])'`) and a + -- bracket the pair set does not understand is worse than one it does. + -- + -- All three are OUTSIDE the nine built-in pair chars, so per Q#AP1 their + -- opener is a source-peer op and their closer a daemon-peer op: their undo + -- is cross-peer-degraded. That is the documented, pre-existing limitation + -- of user-extended pairs, whose general fix is chronological cross-peer + -- undo arbitration (named substrate work). + -- + -- No `''`: Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so + -- pairing it would fight the user constantly. Same reasoning that excludes + -- it for Rust. + lean4 = { "()", "[]", "{}", "⟨⟩", "⦃⦄", "⟮⟯", '""' }, } -- Length of the well-formed UTF-8 sequence starting at `s[i]`, or nil diff --git a/builtin/runtime/syntax.lua b/builtin/runtime/syntax.lua index 812e621..50dad82 100644 --- a/builtin/runtime/syntax.lua +++ b/builtin/runtime/syntax.lua @@ -227,6 +227,11 @@ local default_modeline_aliases = { yml = "yaml", makefile = "make", docker = "dockerfile", + -- Lean 4 (framing Q#LN2). The grammar entry is named `lean4` because that + -- name becomes the `didOpen` language_id, but an Emacs `-*- mode: lean -*-` + -- or a Vim `ft=lean` line is what people actually write, so neither + -- spelling strands a file. + lean = "lean4", } for name, language in pairs(default_modeline_aliases) do if pmacs.parse.modeline_aliases[name] == nil then diff --git a/src/highlight.rs b/src/highlight.rs index 633ec6f..642b0a0 100644 --- a/src/highlight.rs +++ b/src/highlight.rs @@ -208,7 +208,12 @@ impl Theme { ("constructor", fg(11)), ("character", fg(2)), ("keyword.conditional", fg_bold(13)), - ("warning", fg_bold(1)), + // Bold BRIGHT red, deliberately the loudest entry in the table + // and deliberately distinct from `number`'s plain `fg(1)`: in a + // proof file `sorry` means "this is admitted, not proved", which + // is the one thing a reader must never skim past. Plain `fg(1)` + // would have collided with every numeric literal on colour alone. + ("warning", fg_bold(9)), ]; let by_capture = entries .iter() @@ -1527,6 +1532,17 @@ mod tests { src: &str, col: u32, ) -> pmacs_protocol::cell::Color { + painted_style_at(language_name, file, src, col).fg + } + + /// As [`painted_fg_at`], but returns the whole style — needed where a + /// colour alone does not discriminate (Lean's `warning` vs `number`). + fn painted_style_at( + language_name: &str, + file: &str, + src: &str, + col: u32, + ) -> pmacs_protocol::cell::Style { use crate::buffer::{Buffer, BufferId, EditOp}; use crate::cell::{Cell, CellSize}; use crate::syntax::{ParseView, SyntaxRegistry}; @@ -1564,7 +1580,7 @@ mod tests { folds: None, }; hv.render(&buf, viewport, &mut grid); - grid.get(CellCoord::new(0, col)).style.fg + grid.get(CellCoord::new(0, col)).style } /// Does `language`'s compiled highlight query use `capture`? @@ -1576,6 +1592,92 @@ mod tests { query.capture_names().contains(&capture) } + #[test] + fn lean4_grid_paints_comment_keyword_name_operator_and_number() { + // Framing acceptance 5: the grammar plus the crate query plus the + // theme table actually produce distinct styles on a painted grid. + // Asserted end-to-end rather than at the query level because a + // capture that resolves to `Style::default()` is indistinguishable + // from no capture at all to a reader. + use pmacs_protocol::cell::Color; + + // `-- c` — the whole comment run. + assert_eq!( + painted_fg_at("lean4", "a.lean", "-- c\n", 0), + Color::Indexed(8), + "a Lean line comment paints the comment style" + ); + + // `def foo : Nat := 42` + let src = "def foo : Nat := 42\n"; + assert_eq!( + painted_fg_at("lean4", "a.lean", src, 0), + Color::Indexed(5), + "`def` paints the keyword style" + ); + assert_eq!( + painted_fg_at("lean4", "a.lean", src, 4), + Color::Indexed(4), + "the definition's name paints the function style" + ); + assert_eq!( + painted_fg_at("lean4", "a.lean", src, 14), + Color::Indexed(6), + "`:=` paints the operator style" + ); + assert_eq!( + painted_fg_at("lean4", "a.lean", src, 17), + Color::Indexed(1), + "a numeric literal paints the number style" + ); + + // A string literal, and `theorem` as a second declaration keyword. + assert_eq!( + painted_fg_at("lean4", "a.lean", "def s := \"hi\"\n", 9), + Color::Indexed(2), + "a string literal paints the string style" + ); + assert_eq!( + painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 0), + Color::Indexed(5), + "`theorem` paints the keyword style" + ); + assert_eq!( + painted_fg_at("lean4", "a.lean", "theorem t : True := trivial\n", 8), + Color::Indexed(4), + "the theorem's name paints the function style" + ); + } + + #[test] + fn lean4_sorry_paints_the_warning_style_distinctly_from_a_number() { + // Framing acceptance 6. `sorry` admits a goal without proving it — + // in a proof file it is the single most important token to notice, + // and it is why Q#LN4 adds a `warning` entry at all. + // + // The style is asserted in FULL, not by colour: `number` and the + // first-choice `warning` colour were both indexed red, so a + // colour-only assertion would have passed with `sorry` painted + // exactly like the literal `42` beside it. That is the whole failure + // this test exists to prevent. + use pmacs_protocol::cell::Color; + + let sorry = painted_style_at("lean4", "a.lean", "theorem t : True := sorry\n", 20); + assert_eq!( + sorry.fg, + Color::Indexed(9), + "`sorry` paints the warning colour" + ); + assert!(sorry.bold, "`sorry` is bold"); + + let number = painted_style_at("lean4", "a.lean", "def n := 42\n", 9); + assert_ne!( + (sorry.fg, sorry.bold), + (number.fg, number.bold), + "`sorry` must be visually distinct from a numeric literal" + ); + } + #[test] fn lean4_constructor_capture_retro_paints_the_whole_javascript_family() { // Framing acceptance 7 (Q#LN4), the breadth half. `constructor` was diff --git a/src/syntax.rs b/src/syntax.rs index edec588..bc6acf9 100644 --- a/src/syntax.rs +++ b/src/syntax.rs @@ -251,6 +251,12 @@ pub fn default_injection_aliases() -> HashMap { ("golang", "go"), ("yml", "yaml"), ("md", "markdown"), + // Lean 4 (framing Q#LN17). A ```lean fence is overwhelmingly Lean 4 + // in practice, so the Lean 3 spelling is deliberately mapped forward + // rather than left unresolved. `lean4` needs no alias — it is the + // entry name. `lean4-mode` does the equivalent through + // `markdown-code-lang-modes`. + ("lean", "lean4"), ] .into_iter() .map(|(a, b)| (a.to_owned(), b.to_owned())) diff --git a/tests/lean4_stage1_acceptance.rs b/tests/lean4_stage1_acceptance.rs new file mode 100644 index 0000000..ae65545 --- /dev/null +++ b/tests/lean4_stage1_acceptance.rs @@ -0,0 +1,320 @@ +//! Lean 4 mode, Stage 1 acceptance (Arc 8, `docs/lean4-mode-framing.md`). +//! +//! Covers the framing's Stage 1 criteria that live above the Rust +//! substrate — major mode, modeline aliasing, comment toggle, the pair +//! set, and markdown fence injection. Criteria 1, 2, and the Q#LN4 +//! retro-paint pins (7, 8) are unit tests in `src/syntax.rs` and +//! `src/highlight.rs`, where the theme table and grammar registry live. +//! +//! Dispatch-driven, following `comment_toggle_acceptance`: `M-;` and +//! typed characters go through `dispatch_key` so the real command +//! boundary and typed-edit provenance are exercised. Buffers are +//! file-backed (language detection needs a path); each editor gets a +//! private tempdir `StateDir` and an emptied `pmacs.lsp.config` so +//! nothing spawns a language server — Stage 1 has no LSP at all. +//! +//! Criterion 12 is the reason this suite touches no process: it must +//! pass on a machine with no `lean`, no `lake`, and no configured elan +//! toolchain. That is not hypothetical — the machine this arc was +//! scouted on has elan installed with no default toolchain, where +//! `lake --version` itself fails. + +use crossterm::event::{KeyCode, KeyEvent, KeyEventKind, KeyEventState, KeyModifiers}; +use pmacs::editor::EditorState; +use pmacs::lua_bindings::StateDir; +use pmacs::protocol::FrontendId; +use std::path::PathBuf; +use std::sync::atomic::{AtomicUsize, Ordering}; + +fn fresh_state_dir() -> PathBuf { + static SEQ: AtomicUsize = AtomicUsize::new(0); + let dir = std::env::temp_dir().join(format!( + "pmacs-lean4-{}-{}", + std::process::id(), + SEQ.fetch_add(1, Ordering::Relaxed) + )); + std::fs::create_dir_all(&dir).unwrap(); + dir +} + +fn editor(state_dir: &std::path::Path) -> EditorState { + let s = EditorState::new(); + s.lua_host.lua().remove_app_data::(); + s.lua_host + .lua() + .set_app_data(StateDir(state_dir.to_path_buf())); + exec(&s, "pmacs.lsp.config = {}"); + s +} + +fn write_file(dir: &std::path::Path, name: &str, body: &str) -> String { + let p = dir.join(name); + std::fs::write(&p, body).unwrap(); + p.display().to_string() +} + +fn key(code: KeyCode, mods: KeyModifiers) -> KeyEvent { + KeyEvent { + code, + modifiers: mods, + kind: KeyEventKind::Press, + state: KeyEventState::NONE, + } +} + +fn alt(s: &mut EditorState, c: char) { + s.dispatch_key(FrontendId::LOCAL, key(KeyCode::Char(c), KeyModifiers::ALT)); +} + +fn type_str(s: &mut EditorState, text: &str) { + for ch in text.chars() { + s.dispatch_key( + FrontendId::LOCAL, + key(KeyCode::Char(ch), KeyModifiers::NONE), + ); + } +} + +fn exec(s: &EditorState, src: &str) { + s.lua_host.lua().load(src.to_string()).exec().unwrap(); +} + +fn eval(s: &EditorState, src: &str) -> T { + s.lua_host.lua().load(src.to_string()).eval().unwrap() +} + +fn buffer_text(s: &EditorState) -> String { + let b: mlua::String = eval( + s, + "local b = pmacs.window.buffer(); return b:slice(0, b:len())", + ); + String::from_utf8_lossy(&b.as_bytes()).into_owned() +} + +fn cursor(s: &EditorState) -> i64 { + eval(s, "return pmacs.editor.cursor()") +} + +/// Fresh editor visiting `name` (created in the state tempdir) with +/// `body` on disk, cursor at 0. +fn editor_visiting(name: &str, body: &str) -> EditorState { + let dir = fresh_state_dir(); + let s = editor(&dir); + let f = write_file(&dir, name, body); + exec(&s, &format!("pmacs.buffer.find_or_open({f:?})")); + exec(&s, "pmacs.editor.goto_byte(0)"); + s +} + +fn major_mode(s: &EditorState) -> Option { + eval(s, "return pmacs.buffer.major_mode(pmacs.window.buffer())") +} + +// --------------------------------------------------------------------------- +// Criterion 3 — major mode +// --------------------------------------------------------------------------- + +#[test] +fn acc3_opening_a_lean_file_sets_the_lean4_major_mode() { + let s = editor_visiting("Basic.lean", "def x : Nat := 1\n"); + assert_eq!( + major_mode(&s).as_deref(), + Some("lean4"), + "a .lean file carries the lean4 major mode" + ); +} + +// --------------------------------------------------------------------------- +// Criterion 4 — modeline aliasing (Q#LN2) +// --------------------------------------------------------------------------- + +#[test] +fn acc4_emacs_and_vim_modelines_spelling_lean_resolve_to_lean4() { + // The grammar entry is `lean4`, but `-*- mode: lean -*-` and `ft=lean` + // are what people write. Both must land on the same mode, or a file + // with an explicit modeline is stranded with no grammar. + // + // Deliberately on a `.txt` path: if the fixture were `.lean`, the + // extension alone would produce `lean4` and the assertion would pass + // with the alias table empty — the vacuous shape. + for body in [ + "-- -*- mode: lean -*-\ndef x : Nat := 1\n", + "-- vim: ft=lean\ndef x : Nat := 1\n", + ] { + let s = editor_visiting("modeline.txt", body); + assert_eq!( + major_mode(&s).as_deref(), + Some("lean4"), + "modeline {body:?} resolves through the alias to lean4" + ); + } +} + +#[test] +fn acc4b_the_lean_alias_is_load_bearing() { + // Non-vacuity guard for acc4: with the alias removed, the same + // fixture resolves to the raw `lean` name instead. If this ever + // reports `lean4`, acc4 is proving nothing. + let s = editor_visiting("modeline.txt", "x\n"); + exec(&s, "pmacs.parse.modeline_aliases.lean = nil"); + let dir = fresh_state_dir(); + let f = write_file(&dir, "other.txt", "-- -*- mode: lean -*-\ndef x := 1\n"); + exec(&s, &format!("pmacs.buffer.find_or_open({f:?})")); + assert_eq!( + major_mode(&s).as_deref(), + Some("lean"), + "without the alias the modeline name is not normalized" + ); +} + +// --------------------------------------------------------------------------- +// Criterion 9 — comment toggle (Q#LN5) +// --------------------------------------------------------------------------- + +#[test] +fn acc9_comment_toggle_round_trips_with_the_dash_dash_prefix() { + let mut s = editor_visiting("Basic.lean", "def x : Nat := 1\ndef y : Nat := 2\n"); + exec(&s, "pmacs.editor.goto_byte(0)"); + alt(&mut s, ';'); + assert_eq!( + buffer_text(&s), + "-- def x : Nat := 1\ndef y : Nat := 2\n", + "M-; comments a Lean line with `-- `" + ); + // Round trip, including the padding space. + exec(&s, "pmacs.editor.goto_byte(0)"); + alt(&mut s, ';'); + assert_eq!( + buffer_text(&s), + "def x : Nat := 1\ndef y : Nat := 2\n", + "M-; uncomments it exactly" + ); +} + +// --------------------------------------------------------------------------- +// Criterion 10 — pairs (Q#LN6) +// --------------------------------------------------------------------------- + +#[test] +fn acc10_lean_bracket_pairs_close_and_the_prime_does_not() { + // The three Unicode brackets are the reason this decision exists: all + // are outside the nine built-in pair chars, so they exercise the + // user-extended pair path rather than the frontends' optimistic + // classifier. + for (opener, expected) in [("⟨", "⟨⟩"), ("⦃", "⦃⦄"), ("⟮", "⟮⟯")] { + let mut s = editor_visiting("Basic.lean", ""); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, opener); + assert_eq!( + buffer_text(&s), + expected, + "typing {opener} inserts the closing half" + ); + assert_eq!( + cursor(&s), + i64::try_from(opener.len()).expect("opener length fits"), + "the point sits between the pair" + ); + } +} + +#[test] +fn acc10b_the_prime_suffix_does_not_pair_in_lean() { + // Lean uses `'` as a primed-identifier suffix (`h'`, `foo'`), so + // pairing it would fight the user on nearly every proof. + let mut s = editor_visiting("Basic.lean", ""); + exec(&s, "pmacs.editor.goto_byte(0)"); + type_str(&mut s, "h'"); + assert_eq!( + buffer_text(&s), + "h'", + "the prime is a suffix in Lean, not an opener" + ); +} + +// --------------------------------------------------------------------------- +// Criterion 11 — markdown fences (Q#LN17) +// --------------------------------------------------------------------------- + +/// Parse `src` as markdown and return the child layer language names. +/// +/// Goes through the real `_parse_now` injection path rather than reading +/// the alias table: `pmacs.parse.injection_aliases` is a documented +/// WRITE-ONLY proxy (the canonical map lives Rust-side), so an +/// alias-table read would prove nothing about what the parser does. +fn markdown_layer_languages(src: &[u8]) -> Vec { + let state = EditorState::new(); + let buf_id = state + .lua_host + .registry() + .borrow_mut() + .create_from_bytes("doc.md".to_owned(), src); + state + .lua_host + .lua() + .globals() + .set("BUF", pmacs::lua_bindings::BufferIdLua(buf_id)) + .expect("bind BUF"); + state + .lua_host + .lua() + .load("pmacs.parse._parse_now(BUF, 'markdown')") + .exec() + .expect("synchronous parse"); + let bundle = state + .syntax_registry + .view(buf_id) + .and_then(|h| h.current()) + .expect("installed bundle"); + bundle + .layers + .iter() + .map(|l| l.language_name.clone()) + .collect() +} + +#[test] +fn acc11_lean_and_lean4_markdown_fences_both_inject_the_lean_grammar() { + // Both spellings must resolve to the same grammar: `lean4` is the entry + // name and `lean` goes through the injection alias. A ```lean fence is + // overwhelmingly Lean 4 in practice, which is why the Lean 3 spelling + // is mapped forward rather than left unresolved (Q#LN17). + for fence in ["lean", "lean4"] { + let src = format!("# Doc\n\n```{fence}\ndef x : Nat := 1\n```\n"); + let langs = markdown_layer_languages(src.as_bytes()); + assert!( + langs.iter().any(|l| l == "lean4"), + "```{fence} injects a lean4 child layer; got {langs:?}" + ); + } +} + +#[test] +fn acc11b_an_unknown_fence_name_still_injects_nothing() { + // Non-vacuity guard for acc11: the alias must be what resolves `lean`, + // not some catch-all that would light up any fence name. + let langs = markdown_layer_languages(b"# Doc\n\n```leen\ndef x := 1\n```\n"); + assert!( + !langs.iter().any(|l| l == "lean4"), + "a misspelled fence must not reach the lean4 grammar; got {langs:?}" + ); +} + +// --------------------------------------------------------------------------- +// Criterion 12 — no toolchain required +// --------------------------------------------------------------------------- + +#[test] +fn acc12_stage1_spawns_no_process_and_needs_no_lean_toolchain() { + // Stage 1 is grammar + Lua tables only. Opening a Lean file must not + // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and + // even then it is fallible by design (Q#LN7). + // + // Asserted through the process supervisor rather than by inspection: + // opening the file leaves the child-process list exactly as it was. + let s = editor_visiting("Basic.lean", "def x : Nat := 1\n"); + let procs: i64 = eval(&s, "return #pmacs.process.list()"); + assert_eq!(procs, 0, "opening a Lean buffer spawns no child process"); + let servers: i64 = eval(&s, "return #pmacs.lsp.list()"); + assert_eq!(servers, 0, "Stage 1 attaches no language server"); +} From 34767d332d30b8a8c42176fc63e9a93b35f02a21 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 10:18:27 -0400 Subject: [PATCH 5/6] fix(test): make acc12 pin the claim it names (review round 1) Review finding: acc12's server-list assertion could not fail for the regression class it was written to catch. The shared `editor()` helper runs `pmacs.lsp.config = {}` before any buffer opens, so `#pmacs.lsp.list() == 0` holds for every language regardless of what Stage 1 ships -- a Stage-3 front-run that added `pmacs.lsp.config.lean4` in a builtin runtime file would have slipped straight past it. The same vacuous-assertion shape as #155 R2. acc12 now asserts the actual claim against a PRISTINE `EditorState`, before any config wipe: no builtin runtime file defines `pmacs.lsp.config.lean4`. A non-vacuity check pins that the same lookup finds `pmacs.lsp.config.rust`, so this cannot pass merely because the table is empty or absent. Bite-verified: adding `pmacs.lsp.config.lean4 = ... { command = "lake", args = { "serve" } }` to `builtin/runtime/lsp.lua` fails the test; the stub was reverted. The process-list half is kept and its comment now says why it survives the wipe: a direct probe spawn from a future `lean.lua` shows up there whatever `pmacs.lsp.config` contains. Also fixes a stale column in a `highlight.rs` comment -- the Lua table brace in `local t = {}` is at col 10, which is what the code already used. Gates rerun: fmt and strict workspace clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1 9/9; M4 121; required GPU 152; isolated-config workspace sweep 3,150 across 90 suites; diff check clean. Co-Authored-By: Claude Opus 5 (1M context) --- src/highlight.rs | 3 ++- tests/lean4_stage1_acceptance.rs | 32 ++++++++++++++++++++++++++------ 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/highlight.rs b/src/highlight.rs index 642b0a0..de8ffe0 100644 --- a/src/highlight.rs +++ b/src/highlight.rs @@ -1737,7 +1737,8 @@ mod tests { Color::Indexed(4), "a called variant keeps @function, not @constructor" ); - // Lua tags the table-constructor BRACES, not a name: `{` at col 8. + // Lua tags the table-constructor BRACES, not a name: `{` at col 10 + // of `local t = {}`. assert_eq!( painted_fg_at("lua", "a.lua", "local t = {}\n", 10), Color::Indexed(11), diff --git a/tests/lean4_stage1_acceptance.rs b/tests/lean4_stage1_acceptance.rs index ae65545..d48a86c 100644 --- a/tests/lean4_stage1_acceptance.rs +++ b/tests/lean4_stage1_acceptance.rs @@ -305,16 +305,36 @@ fn acc11b_an_unknown_fence_name_still_injects_nothing() { // --------------------------------------------------------------------------- #[test] -fn acc12_stage1_spawns_no_process_and_needs_no_lean_toolchain() { +fn acc12_stage1_ships_no_lsp_config_and_spawns_no_process() { // Stage 1 is grammar + Lua tables only. Opening a Lean file must not // reach for `lake`, `lean`, or `elan` — the LSP arrives in Stage 3, and // even then it is fallible by design (Q#LN7). - // - // Asserted through the process supervisor rather than by inspection: - // opening the file leaves the child-process list exactly as it was. + + // The load-bearing assertion, and it must run against a PRISTINE editor. + // The shared `editor()` helper wipes `pmacs.lsp.config` before any + // buffer opens, so an assertion about the server list under that harness + // holds for every language regardless of what Stage 1 ships — it could + // not fail for the regression it names. This checks the real claim + // directly: no builtin runtime file defines a Lean server config. A + // Stage-3 front-run adding `pmacs.lsp.config.lean4` fails here. + let pristine = EditorState::new(); + let no_lean_config: bool = eval(&pristine, "return pmacs.lsp.config.lean4 == nil"); + assert!( + no_lean_config, + "Stage 1 defines no `pmacs.lsp.config.lean4`; the LSP is Stage 3" + ); + // Non-vacuity: the same lookup finds the configs that DO ship, so this + // is not passing because `pmacs.lsp.config` is empty or absent. + let rust_config_exists: bool = eval(&pristine, "return pmacs.lsp.config.rust ~= nil"); + assert!( + rust_config_exists, + "the config table is populated, so the lean4 absence above is meaningful" + ); + + // And nothing is spawned by opening the file. This half retains its + // value under the wiped config: a direct probe spawn from `lean.lua` + // would show up here whatever `pmacs.lsp.config` contains. let s = editor_visiting("Basic.lean", "def x : Nat := 1\n"); let procs: i64 = eval(&s, "return #pmacs.process.list()"); assert_eq!(procs, 0, "opening a Lean buffer spawns no child process"); - let servers: i64 = eval(&s, "return #pmacs.lsp.list()"); - assert_eq!(servers, 0, "Stage 1 attaches no language server"); } From 1a5805366a4b317dca2ed81e5a436c54bbb0c17f Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 10:18:38 -0400 Subject: [PATCH 6/6] docs: record the Lean 4 lane in the active-work ledger MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review round 1 flagged that neither ledger knew about this branch, and `docs/active-work.md`'s stated job is exactly the volatile open lanes. Records the branch, base, framing revision, what Stage 1 ships, the discharged Q#LN1 obligation, the Q#LN4 blast radius, and the four implementation findings that are not in the framing (the `warning` colour collision with `number`, `Some(1)` resolving to `@function` rather than `@constructor`, the `module > declaration > def` nesting, and `injection_aliases` being a write-only proxy). Also carries forward the two Stage 2 corrections the framing already holds, since that lane starts next. Deliberately ADDITIVE ONLY -- one new section, zero deleted lines. PR #156 is open against both this file and `docs/agent-handoff.md` and owns the snapshot header, the canonical-base line, and the bottom-panel lane's status. Touching those here would collide with a PR already in review, which is the "frozen reviewed PRs do not absorb moving overlapping work" lesson from #135/#137. `docs/agent-handoff.md` is deliberately untouched: its §1 snapshot describes what is ON `main`, so it gets updated when this merges, not while it is in review. Co-Authored-By: Claude Opus 5 (1M context) --- docs/active-work.md | 70 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) diff --git a/docs/active-work.md b/docs/active-work.md index fb835a6..f55627e 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -54,6 +54,76 @@ git status --short --branch The `git log` command must expose `0dd16a5` or a newer intentional main. If it does not, stop and repair the remote/fetch configuration. +## Lean 4 lane (Arc 8) — Stage 1 IN REVIEW (PR #160) + +- Portable branch: `githubsucks/lean4-stage1`, worked in the shared + checkout (no sibling worktree), based on `githubsucks/main` @ `e745068`. +- Approved framing: `docs/lean4-mode-framing.md` revision 4, committed as + the branch's first commit (`a382965`) after three review rounds. **Seven + stages**, 19 decisions (Q#LN1–19), 64 acceptance criteria. North star: + match or exceed VS Code's Lean support. +- **Stage 1 implemented; no wire change (protocol stays v20), no LSP, no + frontend change.** Four commits: framing, grammar, theme captures, + editing surface + acceptance. + - `Cargo.toml` + `src/syntax.rs`: `arborium-lean` 2.18 and one + `BUILTIN_LANGUAGES` entry named **`lean4`** (Q#LN2 — the name becomes + the `didOpen` language_id), claiming `.lean` only. + - `src/highlight.rs`: four capture entries — `constructor`, `character`, + `keyword.conditional`, `warning`. + - `builtin/runtime/{comment,pair,syntax}.lua`: `--` comments, the + `⟨⟩ ⦃⦄ ⟮⟯` pair set, the `lean` → `lean4` modeline alias. + - `tests/lean4_stage1_acceptance.rs` plus unit tests in `syntax.rs` / + `highlight.rs`: 12 criteria, 17 tests. +- **Q#LN1's open obligation is discharged.** `tree-sitter-lean4` is + unusable (depends on `tree-sitter ^0.25` directly against our 0.26, + exports no `LANGUAGE` const despite its README, packages no queries); + `arborium-lean` rides `tree-sitter-language 0.1` with a pre-generated + ABI-15 parser. `cargo tree -d` shows no duplicate core. The parse smoke + pins the failure mode that matters: `→`/`∀`/`≥` must produce + `(arrow)`/`(forall)`/`(comparison)`, since a mismatched-core build + degrades silently on exactly those characters rather than failing loudly. +- **Q#LN4 is a deliberate retro-paint of seven language entries**, not + four: `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated + base-first into javascriptreact/typescript/typescriptreact. Its shape is + "every capitalized identifier" (`#match? "^[A-Z]"`) plus every Lua table + brace — not "constructors". Pinned in both directions per #146. +- Implementation findings not in the framing: + - `warning` had to move from bold red to bold **bright** red: `number` + is plain `fg(1)`, so `sorry` and an adjacent numeric literal were the + same colour. Found by writing the test. + - `Some(1)` is **not** `@constructor` — in call position a narrower + `@function` pattern wins. Only bare or pattern-position capitalized + identifiers reach it. Pinned so the blast-radius claim stays honest. + - Lean node kinds nest: `module > declaration > def|theorem`. + - `pmacs.parse.injection_aliases` is a documented **write-only** Lua + proxy (canonical map is Rust-side), so fence tests must drive + `_parse_now` and inspect layer languages, never read the table back. +- **Review round 1 addressed.** The finding: acc12's server-list assertion + could not fail for the regression it named — the shared `editor()` + helper wipes `pmacs.lsp.config` before any buffer opens, so + `#pmacs.lsp.list() == 0` holds for every language regardless of what + Stage 1 ships. It now asserts against a **pristine** `EditorState` that + `pmacs.lsp.config.lean4` is nil, with a non-vacuity check that the same + lookup finds `rust`; bite-verified by adding a `lean4` config to + `lsp.lua` and watching it fail. Also fixed a stale column in a + `highlight.rs` comment. +- Verification on this branch: `cargo fmt --check` clean; strict workspace + Clippy clean; 1,826 default + 2,003 CRDT library tests; lean4 Stage 1 + 9/9; comment toggle 14; auto-pair 45; injection 4; M4 121; required GPU + 152; **isolated-config workspace sweep 3,150 across 90 suites**; + `git diff --check` clean. The sweep needs an isolated `XDG_CONFIG_HOME` + for the reason recorded in the bottom-panel lane below. +- **Stage 2 is multi-root LSP server affinity** — pure substrate, no Lean + content, and it changes `ensure_server`, which every LSP language + shares. It is sequenced next because Lean is the language that makes its + absence a correctness failure rather than an inconvenience. Two + corrections the framing already carries for it: `root` is computed at + `lsp.lua:537`, **after** the reuse loop, so the fix must hoist it; and + `project_root_for` never returns nil for a file with a path, so the + affinity key must be the root only when a root was actually *detected*, + or markerless scratch files fragment into one server per directory for + every language. + ## Bottom-panel lane (window placement + side windows) — Stage 1 IN REVIEW - Portable branch: `githubsucks/bottom-panel`, worktree