Merge pull request #160 from levineuwirth/lean4-stage1

feat(lean4): Arc 8 Stage 1 — grammar, major mode, and the editing table stakes

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",

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).

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

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

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

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

src/highlight.rs

@@ -174,6 +174,46 @@ 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)),
+            // 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()
@@ -1484,6 +1524,262 @@ 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 {
+        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};
+
+        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<Cell> = 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
+    }
+
+    /// 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_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
+        // 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 10
+        // of `local t = {}`.
+        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`,

src/syntax.rs

@@ -251,6 +251,12 @@ pub fn default_injection_aliases() -> HashMap<String, String> {
         ("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()))
@@ -1130,6 +1136,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 +2427,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

tests/lean4_stage1_acceptance.rs

@@ -0,0 +1,340 @@
+//! 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::<StateDir>();
+    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<T: mlua::FromLuaMulti>(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<String> {
+    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<String> {
+    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_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).
+
+    // 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");
+}