Julian / Julian/tree-sitter-lean
Nested `have ... := by` tactic parses with ERROR and consumes following tactic
- Dominant language
- JavaScript
- Stars
- 58
- Forks
- 25
- Avg merge
- 48m
- Merged PRs (30d)
- 1
Description
### Reproduction
With current `main` (`dc5997b`), this valid Lean tactic block parses with an `ERROR` node:
```lean
example : True := by
have h : True := by
exact trivial
exact h
```
Run:
```sh
tree-sitter parse --grammar-path . repro.lean
```
### Actual parse shape
The nested `by` is wrapped in `ERROR`, and the following sibling tactic `exact h` is consumed as the `have` value:
```scheme
stmt: (have
name: (identifier)
type: (true_const)
(ERROR
(by
stmt: (app
fn: (identifier)
arg: (identifier))))
value: (app
fn: (identifier)
arg: (identifier)))
```
### Expected parse shape
The `have` value should be the nested `by` block, and `exact h` should remain a sibling statement:
```scheme
stmt: (have
name: (identifier)
type: (true_const)
value: (by
stmt: (app
fn: (identifier)
arg: (identifier))))
stmt: (app
fn: (identifier)
arg: (identifier))
```
### Why this matters
This affects declaration range discovery through `queries/locals.scm` and downstream tools. In a larger theorem, the erroneous recovery can extend the previous theorem node far enough to swallow the next top-level theorem, so the next declaration is not captured as its own node.
I first saw this on a file where a long `calc` proof was followed by another theorem; the second theorem was valid Lean and checkable, but tree-sitter's recovered range attached it to the previous theorem.
### Notes
I also tried two small grammar directions locally:
- adding a conflict for `_lead_term` / `have`
- increasing precedence for `by` as a lead term
The first did not change the parse; the second made parser generation much heavier. I am opening the issue rather than sending an unvalidated grammar patch.
Contributor guide
No contributing guide indexed for this repository
Research direction
Start by reproducing the issue with tree-sitter parse --grammar-path . repro.lean and inspect the grammar entry points for have and nested by terms. Review queries/locals.scm to understand the affected declaration ranges. Done means the nested by block is the have value, exact h remains a sibling statement, and the ERROR node is gone.
Written by the indexing model from the issue text.
Assessment
- Domain
- compilers
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100