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) <noreply@anthropic.com>
This commit is contained in:
parent
a38296583b
commit
6ea8d2756e
|
|
@ -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",
|
||||
|
|
|
|||
18
Cargo.toml
18
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).
|
||||
|
|
|
|||
170
src/syntax.rs
170
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
|
||||
|
|
|
|||
Loading…
Reference in New Issue