tree-sitter-lean4 0.2.0

Tree-sitter grammar for Lean 4 (generates parser at build time)
Documentation 
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

# Tree-Sitter-Lean4

Lean4 is a programming language, commonly used for mathematical theorem proving as a [proof assistant](https://en.wikipedia.org/wiki/Proof_assistant).

This project contains:

- Tree-Sitter grammar for parsing [Lean 4](github.com/leanprover/lean4) source code.
- Rust crate that can be used in combination with `tree-sitter` crate with bindings for parsing Lean
- Nix flake for using the compiled parser in other tools in the Tree-Sitter ecosystem such as AST-Grep

**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).

## Usage

### Rust

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

```bash
cargo add tree-sitter-lean4
```

During the first build, you need this:

- C code generator `tree-sitter` (only if the `src/parser.c` is missing)
- C compiler `cc`

Then instantiate the parser:

```rust
use tree_sitter::{InputEdit, Language, Parser, Point};

let mut parser = Parser::new();
parser.set_language(&tree_sitter_lean4::LANGUAGE.into()).expect("Error loading Rust grammar");
```

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

### Nix Flake

This is the recommended approach for reproducible builds.

```nix
{
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
    tree-sitter-lean.url = "github:wvhulle/tree-sitter-lean";
  };

  outputs = { nixpkgs, tree-sitter-lean, ... }:
    let
      system = "x86_64-linux";
      pkgs = nixpkgs.legacyPackages.${system};
    in
    {
      devShells.${system}.default = pkgs.mkShell {
        # If you want to use ast-grep (see next section)
        packages = [ pkgs.ast-grep ];
        shellHook = ''
          # Create a symlink in the working directory for easy access (add to .gitignore)
          ln -sf ${tree-sitter-lean.packages.${system}.grammar}/parser tree-sitter-lean.so
        '';
      };
    };
}
```

See [`nixpkgs` tree-sitter documentation](https://nixos.org/manual/nixpkgs/stable/#tree-sitter) for more Tree-Sitter with Nix examples.

Push build cache to public cache server:

```bash
nix build . --print-out-paths | cachix push wvhulle
```

## Development

Read [writing the grammar](https://tree-sitter.github.io/tree-sitter/creating-parsers/3-writing-the-grammar.html). Be careful of adding too many conflicts in the grammar as they cause exponential growth of the state space.

Use the `tree-sitter` CLI:

```bash
tree-sitter generate # Re-run this after every grammar rule change
tree-sitter parse Test.lean # A long Lean file that needs to be parsed correctly
```

Add tests for the Tree-Sitter grammar to [./test/corpus](./test/corpus).
See [writing tests](https://tree-sitter.github.io/tree-sitter/creating-parsers/5-writing-tests.html)

## License

Based on <https://github.com/Julian/lean.nvim>. Grammar was completely rewritten to be simpler.

MIT