Tree-Sitter-Lean4

Lean4 is a programming language, commonly used for mathematical theorem proving as a proof assistant.

This project contains a Lean parser definition:

• Tree-Sitter grammar for parsing Lean 4 source code.
• Tree-Sitter queries for usage in the modal text editor Helix.
• Rust library pushed to Crates.io for parsing Lean in a Rust program

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.

Usage

Rust

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

cargo add tree-sitter-lean4

During the first build, you need these binaries in your path:

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

Then instantiate the parser:

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.

Nix Flake

This is the recommended approach for reproducible builds.

{
  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 for more Tree-Sitter with Nix examples.

Push build cache to public cache server:

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

Development

Read writing the grammar. Be careful of adding conflicts in the grammar as they cause exponential growth of the state space.

Use the tree-sitter CLI:

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

Tests

Add tests for the Tree-Sitter grammar to ./test/corpus.

Tests are run with

tree-sitter test

Check the amount of failures with:

tree-sitter test --overview-only | grep ✗ | lines | length

Tests can be updated automatically when you change the grammar:

tree-sitter test --update

See writing tests

You should also test the queries from ./queries:

tree-sitter query higlights.scm Test.lean

This will report any errors such as incorrect node names in the query file.

License

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

MIT