Julian / Julian/tree-sitter-lean

Nested `have ... := by` tactic parses with ERROR and consumes following tactic

Open
#18 0 comments 0 reactions 0 assignees View on GitHub
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.