From 6ea8d2756e551dc1b33015c53b0b1e792ca53f5c Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sat, 25 Jul 2026 09:49:01 -0400 Subject: [PATCH] feat(syntax): bundle the Lean 4 grammar (Arc 8 Stage 1, Q#LN1-3) Adds `arborium-lean` 2.18 and one `BUILTIN_LANGUAGES` entry, closing the framing's open verification obligation on the crate choice. Why this crate and not `tree-sitter-lean4` (Q#LN1): the latter depends on `tree-sitter = "0.25"` directly rather than the shared `tree-sitter-language` ABI crate, and `^0.25` excludes our 0.26, so it would fork the graph exactly as the dead `tree-sitter-dockerfile` does. It also exports only `pub fn language()` while its README advertises a `LANGUAGE` const that does not exist, and its package `include` omits `queries/` so it ships no highlights at all. `arborium-lean` uses `tree-sitter-language 0.1` as its sole runtime dep, ships a pre-generated ABI-15 parser plus scanner, and exports real query constants. `cargo tree -d` reports no duplicate `tree-sitter`. The entry is named `lean4`, not `lean` (Q#LN2): `ensure_server` passes `LanguageEntry.name` through as the `didOpen` language_id, and the Lean ecosystem's id is `lean4` -- `lean` is Lean 3, which is end-of-life. It claims `.lean` only; `.olean` is a compiled binary and `.ilean` is JSON metadata (Q#LN3). Four tests. The load-bearing one is `lean4_grammar_loads_and_parses`, which discharges the half of Q#LN1 that could not be settled by reading: `arborium-lean` exports `const fn language() -> LanguageFn` rather than the `LANGUAGE` const every other entry uses, and its README demonstrates usage against a patched tree-sitter core. Neither is supposed to matter, but "supposed to" is not evidence. The fixture parses without error, and -- the part that actually guards a misbuild -- its Unicode operators produce structure rather than degrading silently: the grammar must see a `(arrow)` for the arrow, a `(forall)` for the universal quantifier, and a `(comparison)` for the inequality. The error-free claim is deliberately scoped to the committed fixture. Lean's syntax is user-extensible via macros, so a static grammar mis-parses some legal input by construction; the framing scores that as bet 3 rather than the doc overselling it. Co-Authored-By: Claude Opus 5 (1M context) --- Cargo.lock | 33 ++++++++++ Cargo.toml | 18 ++++++ src/syntax.rs | 170 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 221 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index d7caff6..498f267 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -169,6 +169,27 @@ dependencies = [ "x11rb", ] +[[package]] +name = "arborium-lean" +version = "2.18.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "80b795046d03aae5780c58e746ddaf780f683e36d9efa8f67abbe9bc01299eb5" +dependencies = [ + "arborium-sysroot", + "cc", + "tree-sitter-language", +] + +[[package]] +name = "arborium-sysroot" +version = "2.18.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "59d99d80550b726f9dec7ee6d07118c31e08b10e729ac488eabd4c10603dc841" +dependencies = [ + "cc", + "dlmalloc", +] + [[package]] name = "arrayref" version = "0.3.9" @@ -747,6 +768,17 @@ dependencies = [ "libloading", ] +[[package]] +name = "dlmalloc" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad5208a115eaba24916f7456929832e310a81518c641f93fee4f89aa93aa3675" +dependencies = [ + "cfg-if", + "libc", + "windows-sys 0.61.2", +] + [[package]] name = "document-features" version = "0.2.12" @@ -2538,6 +2570,7 @@ checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" name = "pmacs" version = "1.0.0" dependencies = [ + "arborium-lean", "codebook-tree-sitter-latex", "crossbeam", "crossterm", diff --git a/Cargo.toml b/Cargo.toml index 589ccaf..4e21592 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -241,6 +241,24 @@ codebook-tree-sitter-latex = "0.6" # engine (see `crate::syntax::BUILTIN_LANGUAGES`). tree-sitter-html = "0.23" tree-sitter-css = "0.25" +# Lean 4 (`.lean`) — Arc 8 Stage 1 (`docs/lean4-mode-framing.md`, Q#LN1). +# `leanprover` ships no tree-sitter grammar (Lean parses with its own +# kernel), so both candidates are third-party. The obvious-looking +# `tree-sitter-lean4` is NOT usable: it depends on `tree-sitter = "0.25"` +# DIRECTLY rather than the shared `tree-sitter-language` ABI crate, which +# `^0.25` makes incompatible with our 0.26 and would fork the graph (the +# same defect that rules out `tree-sitter-dockerfile` above); it exports +# only `pub fn language()` while its README advertises a `LANGUAGE` const +# that does not exist; and its package `include` omits `queries/`, so it +# ships no highlights at all. `arborium-lean` is a republish from the +# arborium grammar collection that does it correctly: `tree-sitter-language +# 0.1` as its sole runtime dep, a pre-generated ABI-15 `parser.c` plus +# `scanner.c` (no CLI at build time), and `HIGHLIGHTS_QUERY` / +# `INJECTIONS_QUERY` / `LOCALS_QUERY` constants. Note the shape: it exports +# `const fn language() -> LanguageFn`, so the entry in +# `crate::syntax::BUILTIN_LANGUAGES` reads `arborium_lean::language().into()` +# rather than the `LANGUAGE.into()` every other entry uses. +arborium-lean = "2.18" # T M4.4 process supervisor: signal sending without `unsafe`. Keep # the feature surface tight to keep build time low. `poll` feeds the # compile-mode group readers (cancellable poll-based reads, Q#CM3). diff --git a/src/syntax.rs b/src/syntax.rs index efbbd4d..edec588 100644 --- a/src/syntax.rs +++ b/src/syntax.rs @@ -1130,6 +1130,33 @@ pub const BUILTIN_LANGUAGES: &[LanguageEntry] = &[ locals_query: &[], injections_query: &[], }, + // Lean 4 (framing `docs/lean4-mode-framing.md`, Arc 8 Stage 1). + // + // The entry is named `lean4`, not `lean` (Q#LN2): this name becomes the + // `language_id` sent in `didOpen` — `ensure_server` at + // `builtin/runtime/lsp.lua:540` passes it straight through — and the + // Lean ecosystem's id is `lean4` (`lean` is Lean 3, which is + // end-of-life). The grammar's own C symbol is `tree_sitter_lean`; that + // is arborium's business, not ours. Stage 3 adds + // `pmacs.lsp.config.lean4` against this name. + // + // Note the loader shape: `arborium-lean` exports `const fn language() -> + // LanguageFn` rather than a `LANGUAGE` const, so this is the one entry + // that calls a function to get the `LanguageFn` before `.into()`. + // + // `.olean` (compiled artifacts) and `.ilean` (JSON metadata) are + // deliberately unclaimed (Q#LN3). Locals and injections are empty + // because the crate ships both as empty strings — Lean has no embedded + // sublanguage worth injecting, and its scoping is far beyond what a + // tree-sitter locals query could model. + LanguageEntry { + name: "lean4", + extensions: &["lean"], + loader: || arborium_lean::language().into(), + highlights_query: &[arborium_lean::HIGHLIGHTS_QUERY], + locals_query: &[], + injections_query: &[], + }, ]; /// LaTeX highlights overlay (framing Q#LX2). The chosen grammar crate @@ -2394,6 +2421,149 @@ mod tests { } } + #[test] + fn builtin_languages_include_lean4() { + // Framing acceptance 1/3 (`docs/lean4-mode-framing.md`). The entry is + // named `lean4` because that name becomes the `didOpen` language_id + // (Q#LN2), and it claims `.lean` ONLY: `.olean` is a compiled binary + // artifact and `.ilean` is JSON metadata (Q#LN3). + let lean = BUILTIN_LANGUAGES + .iter() + .find(|l| l.name == "lean4") + .expect("`lean4` language entry must be present"); + assert!(lean.extensions.contains(&"lean"), "`lean4` claims `.lean`"); + for unclaimed in ["olean", "ilean"] { + assert!( + !lean.extensions.contains(&unclaimed), + "`lean4` must not claim `.{unclaimed}`" + ); + } + assert!( + lean.highlights_query + .contains(&arborium_lean::HIGHLIGHTS_QUERY), + "`lean4` drives highlighting from the crate's query constant, not an overlay" + ); + assert!( + lean.locals_query.is_empty() && lean.injections_query.is_empty(), + "`lean4` ships neither locals nor injections (Q#LN1)" + ); + } + + #[test] + fn lean4_grammar_loads_and_parses() { + // Framing acceptance 2 and the open half of Q#LN1: `arborium-lean` + // exports `const fn language() -> LanguageFn` (not the `LANGUAGE` + // const every other entry uses) over `tree-sitter-language 0.1`, and + // its README demonstrates usage against a `tree_sitter_patched_ + // arborium` core. Neither is supposed to matter — the LanguageFn ABI + // is shared — but "supposed to" is not evidence, so this pins that + // OUR `tree-sitter` 0.26 core accepts it and produces a real tree. + // + // The fixture exercises the grammar's external scanner (`scanner.c` + // supplies a NEWLINE token, so layout-sensitive `def`/`theorem` + // bodies depend on it) and the Unicode operators that make Lean + // Lean — `→`, `∀`, `≥` — which a byte-oriented misbuild would shred. + let reg = SyntaxRegistry::new(); + let language = reg + .language("lean4") + .expect("`lean4` language loads from BUILTIN_LANGUAGES"); + let mut buf = fresh_buffer("Basic.lean"); + buf.apply_edit(EditOp::Insert { + pos: 0, + bytes: "-- a comment\n\ + def fibonacci : Nat → Nat\n\ + \x20 | 0 => 0\n\ + \x20 | n + 1 => n\n\ + \n\ + theorem fib_nonneg : ∀ n, fibonacci n ≥ 0 := by\n\ + \x20 intro n\n\ + \x20 exact Nat.zero_le _\n" + .as_bytes(), + }) + .unwrap(); + let view = ParseView::new(&buf, language, "lean4".to_owned()); + let handle = view.handle(); + let _vid = buf.attach_view(Box::new(view)); + let bundle = parse_synchronously(&handle); + assert_eq!( + bundle.root_tree().root_node().kind(), + "module", + "Lean grammar roots at module" + ); + let sexp = bundle.root_tree().root_node().to_sexp(); + // This specific committed fixture parses cleanly. The claim is + // scoped to the fixture on purpose: Lean's syntax is user-extensible + // via macros, so a static grammar necessarily mis-parses some legal + // input (the upstream grammar says so itself, and the framing scores + // it as bet 3). What a clean parse HERE proves is that the crate is + // wired correctly, not that Lean is fully parseable. + assert!( + !bundle.root_tree().root_node().has_error(), + "the fixture parses without error; got {sexp}" + ); + // `def` and `theorem` sit under a `declaration` wrapper, not directly + // under `module`. + for expected in ["(comment)", "(def ", "(theorem "] { + assert!( + sexp.contains(expected), + "expected `{expected}` in the tree; got {sexp}" + ); + } + // The load-bearing part of this test. A grammar built against a + // mismatched core, or one whose scanner mis-handles multibyte input, + // does not fail loudly — it produces a tree that silently degrades on + // exactly the characters Lean is made of. `→` must become an `arrow`, + // `∀` a `forall`, and `≥` a `comparison`; if these three hold, the + // UTF-8 path through the parser is sound. + for expected in ["(arrow ", "(forall ", "(comparison "] { + assert!( + sexp.contains(expected), + "Unicode operator did not produce `{expected}`; got {sexp}" + ); + } + } + + #[test] + fn lean4_highlights_resolve() { + // The crate's 213-line query must COMPILE against the grammar it + // ships with — the node-name compatibility gate. A query referencing + // a node this grammar version lacks fails here rather than silently + // producing no spans at runtime. + let reg = SyntaxRegistry::new(); + let query = reg + .highlights_query("lean4") + .expect("lean4 highlights compile against the grammar"); + let names = query.capture_names(); + // The four capture names Q#LN4 adds to the GLOBAL theme table are + // present here — this is the forward direction of that decision; the + // reverse direction (what they do to other languages) is pinned in + // `highlight.rs`. + for expected in ["constructor", "character", "keyword.conditional", "warning"] { + assert!( + names.contains(&expected), + "lean4 query uses `@{expected}`, which Q#LN4 adds to the theme; got {names:?}" + ); + } + } + + #[test] + fn language_for_path_resolves_lean_extension() { + let reg = SyntaxRegistry::new(); + assert_eq!( + reg.language_name_for_path("Mathlib/Data/Nat/Basic.lean") + .as_deref(), + Some("lean4"), + "`.lean` resolves to the lean4 grammar" + ); + for unclaimed in ["Basic.olean", "Basic.ilean"] { + assert_ne!( + reg.language_name_for_path(unclaimed).as_deref(), + Some("lean4"), + "{unclaimed} must not resolve to lean4" + ); + } + } + #[test] fn builtin_languages_include_html_and_css() { // Both crate grammars export their query constants (no overlay). HTML