Lean 4 analyzer: needs tree-sitter-language-pack 1.x (only source of a usable Lean grammar) #154

Summary

I want to add a Lean 4 analyzer. The only usable Lean grammar is in tree-sitter-language-pack 1.x, but pyproject.toml caps the pack below 0.9. #130 added the cap because "the Dart grammar/API in 0.9 is not yet verified". Do you accept a move to 1.x for this? I can send the bump, with the Dart verification below, and the analyzer as two stacked PRs.

Grammar options

I compared the candidates on 300 real Lean 4 files (programs and proofs, not Mathlib), sampled from a private corpus of about 1,000 files:

get_parser("lean") fails on pack 0.8.0, 0.9.1 and 0.13.0, and works on 1.23.1.

What the 1.x bump changes

I made the change on a branch and ran the suite:

• With only the pin changed, 2 Dart tests fail: test_call_resolution_rules and test_riverpod_and_router_edges. The 1.x Dart grammar parses Foo<T>(x) as a call whose argument_part holds type_arguments, not as a relational_expression. So the Garage.open -> Item and carProvider -> Car type-argument edges are lost.
• An 11-line change in _process_chain reads those type arguments from the call. After it, all 654 tests pass, and ruff check and ruff format --check are clean.
• 1.x downloads each grammar on first use and caches it under cache_dir(). The pack grammars that CodeWiki uses are dart, go, javascript, typescript, vue and zig. So the first run needs network access. I can add a t.download([...]) step to docker/Dockerfile, so that the image runs offline.

This is the Dart verification that #130 asked for. I found no other issue or PR about updating the pack.

Proposed analyzer design

The grammar alone is not enough. It fails on #eval, #guard, #[...], ¬, ←, using, with and user notation. Also, end is a flat top-level node, so the tree does not give namespace nesting. I propose two layers:

1. Structure, from a header scanner. The scanner reads Lean commands from the source, with comments and strings masked. It gives declaration names (def, theorem/lemma, abbrev, instance, structure, class, inductive, axiom, opaque), the namespace/section/end stack, open (including open X in), import, spans and /-- -/ docstrings. It does not depend on ERROR regions.
2. References, from tree-sitter. For a declaration whose node has no error (76.7% in the sample), take the identifier nodes and drop binder, let, field and pattern names. For the other declarations, use tokens from the masked text.

Each reference resolves only to an exact fully qualified name. The analyzer tries the namespace chain, the open namespaces and the declarations of the imported files (transitively, cached by mtime, like zig.py does). It drops a reference that has no match, and it never guesses by a bare name. A lean branch in _resolve_callee keeps this authoritative, like the Go and Dart branches.

Other parts:

• Component types: structure → struct, class → interface, inductive → class, and the rest → function. node_type keeps the Lean keyword.
• .lake/ and lake-packages/ go in the ignore patterns. lakefile.lean and lakefile.toml become build artifacts, and lake-manifest.json and lean-toolchain become manifests.
• Tests use synthetic Lean only.

Known limits:

• Generalized field notation (v.norm for Vec.norm) needs type information, so it does not resolve.
• References from user notation/macro are lost.
• The scanner assumes that each command starts a line, which is the usual Lean style.

Tools that use Lean itself (doc-gen4, jixia) give exact data, but they need a built project, and jixia must match the project's Lean version. I propose to keep them out of scope.

Related

• Added flutter/dart support #130 added the <0.9.0 cap for Dart.
• fix(analyzers): a class's constructor is a component like any method #149 found that the requirements.txt pins (tree-sitter 0.23.2) could not load the C# grammar (ABI 15). 1b4af43 fixed this with tree-sitter 0.26.0. Pack 1.23.1 declares tree-sitter>=0.23, so the current pin already works with it.
• analyzers: add tree-sitter based Go analyzer #140 and Add Zig and Vue SFC analyzers, Autotools build artifacts #142 (Go, Zig, Vue) take their grammars from the pack, so the 1.x move affects them too. Their tests pass on 1.23.1.

Questions

1. Do you accept the move to tree-sitter-language-pack>=1.23.1,<2.0.0, with the Dart fix, as a separate PR?
2. Do you accept that grammars download on first use, if the Docker image fetches them at build time?
3. Is the two-layer design acceptable, or do you want a tree-sitter-only analyzer, with fewer declarations and no namespace nesting?