Tree-Sitter-Lean4

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

This project contains:

Tree-Sitter grammar for parsing Lean 4 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.

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 this:

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 too many 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

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

License

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