1468 lines
75 KiB
Markdown
1468 lines
75 KiB
Markdown
# 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 `<pkg>/.lake/packages/*`,
|
||
and each vendored package carries its own `lean-toolchain`. Opening
|
||
`<pkg>/.lake/packages/batteries/Batteries/Data/List.lean` must serve
|
||
from `<pkg>`, 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<String>` 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
|
||
`<pkg>/.lake/packages/dep/…` whose ancestor chain contains two
|
||
`lean-toolchain` files resolves to `<pkg>`, 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.
|