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

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

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

Publish to Crates.io with:

cargo publish --allow-dirty

Debug using AST-Grep with:

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

Add tests to ./test/corpus.

License

MIT