[Feature] support lean4

[DieracDelta]

Problem

I'd like to index my lean4 codebase to use this tool

Proposed Solution

I think it would be enough to add in https://github.com/Julian/tree-sitter-lean

Alternatives Considered

N/A

Additional Context

Lean4 is a really popular theorem prover (and gpl). LLMs are quite good at it!

[RaghavChamadiya]

Happy to support Lean4. It's a good fit, and you're right that LLMs do well with it. I'd love a PR if you're up for it, and I'm glad to help while you work through it. Here's how it'd come together so you (or anyone who wants to grab this) can scope it out.

repowise has tiered language support (see docs/LANGUAGE_SUPPORT.md). Where Lean4 lands depends on what we can pull out of the grammar:

Full AST tier (symbols, imports, call graph) is the goal, and tree-sitter-lean is what unlocks it. The Adding a New Language section covers it step by step, but the short version is:

1. Add a LanguageSpec module at languages/specs/lean.py and register it in specs/__init__.py.
2. Add "lean" to the LanguageTag literal in ingestion/models.py.
3. Write ingestion/queries/lean.scm using the capture-name conventions (@symbol.def, @symbol.name, @import.statement, @import.module, @call.target). python.scm and typescript.scm are good ones to copy from.
4. Add a LanguageConfig entry in language_configs.py.
5. Add the grammar dependency to pyproject.toml.

Steps 6 to 8 (binding extractor, heritage extractor, import resolver) are optional and additive. The generic stem-map fallback works out of the box, so a first PR can land without them. A proper import/open resolver for Lean would be the most useful follow-up after that.

One thing worth checking before you dig in: the pipeline loads grammars as a Python package (the grammar_package field on LanguageSpec, e.g. tree_sitter_lean), so tree-sitter-lean needs to be pip-installable with usable Python bindings for the AST tier. If that turns out to be painful, there's a smaller fallback. The lightweight regex tier skips AST parsing but still extracts import/open statements with a regex and resolves them against a module-name index, which gives you a real file-to-file dependency graph plus full wiki, search, and dead-code coverage. Elixir, Dart, and Haskell live there today, and it's a much smaller change. Either one is a genuinely useful first step.

To check it locally: pytest tests/ -k "lean or sample_repo" -x, then repowise init /path/to/your-lean-project. Dropping a small Lean fixture under tests/fixtures/lang_samples/lean/ gives the parser something to test against.

No pressure to take it on yourself, but if you do, ping me on the PR and I'll review it quickly. And if you'd rather just dig into whether the grammar ships Python bindings and report back, that alone helps whoever picks it up.