tree-sitter-lean4 0.0.4

Tree-sitter grammar for Lean 4 (generates parser at build time)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

# Tree-Sitter-Lean4

Language bindings for Rust programs to parse [Lean 4](github.com/leanprover/lean4) source code. Lean4 is a programming language, commonly used for mathematical theorem proving as a [proof assistant](https://en.wikipedia.org/wiki/Proof_assistant).

## Installation

### Cargo

Add this crate as a normal dependency in your `Cargo.toml` file.

The parser is automatically generated by the build script in [`build.rs`](./build.rs) if it is missing. This requires `tree-sitter` and a C compiler installed.

## Usage

### Rust

See [Tree-Sitter-Rust](https://github.com/tree-sitter/tree-sitter/tree/master/lib/binding_rust).

**Important**: Lean is a very extensible language. Therefore, the Tree-Sitter grammar is of limited use. For parsing advanced Lean programs you will need to use the Lean kernel. See also [Metaprogramming in Lean](https://github.com/leanprover-community/lean4-metaprogramming-book).

### Nix Flake

This grammar is available as a Nix flake with the following outputs:

- `packages.<system>.grammar` - The tree-sitter grammar
- `overlays.default` - Adds grammar to `pkgs.tree-sitter.builtGrammars.tree-sitter-lean`
- `devShells.<system>.default` - Development environment with `tree-sitter`, `ast-grep`, etc.

See [Nixpkgs tree-sitter documentation](https://nixos.org/manual/nixpkgs/stable/#tree-sitter) for integration examples.

### AST-Grep

[AST-Grep](https://ast-grep.github.io/reference/sgconfig.html) is a tool for quick large refactors. To set it up to use this Lean grammar, add to your `flake.nix`:

```nix
{
  inputs.tree-sitter-lean.url = "github:yourusername/tree-sitter-lean";

  outputs = { self, nixpkgs, tree-sitter-lean }: {
    devShells.x86_64-linux.default = nixpkgs.legacyPackages.x86_64-linux.mkShell {
      packages = [ nixpkgs.legacyPackages.x86_64-linux.ast-grep ];
      shellHook = ''
        ln -sf ${tree-sitter-lean.packages.x86_64-linux.grammar}/parser tree-sitter-lean.so
      '';
    };
  };
}
```

Create `sgconfig.yml`:

```yaml
customLanguages:
  lean:
    libraryPath: tree-sitter-lean.so
    extensions: [lean]
    expandoChar: _
```

Now use ast-grep:

```bash
nix develop
ast-grep --lang lean --pattern 'def $_x := $_body' your-file.lean
```

Note that you can't just use write any expression in the `-p` argument. Expression are not valid at the top-level in Lean program in general.

## Development

Based on <https://github.com/Julian/lean.nvim>.

## License

MIT