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

The binary Lean parser is automatically compiled Cargo if it is missing. If it is missing, you will need these binaries for compilation with Cargo:

• tree-sitter CLI tool for generating Tree-Sitter parsers

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.

AST-Grep

AST-Grep is a tool for quick large refactors. To set it up to use this Lean grammar, add to your flake.nix: Create sgconfig.yml:

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

Now use ast-grep:

nix develop
ast-grep --lang lean --pattern 'def $A := $B' your-file.lean

Development

Read writing the grammar

Use the tree-sitter CLI:

tree-sitter parse TEST.lean

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

You can also debug using AST-Grep with:

ast-grep run -p <PATTERN> --debug-query ast

License

Based on https://github.com/Julian/lean.nvim with better support for parsing the interior of monad do blocks.

MIT