docs.rs failed to build tree-sitter-lean4-0.0.4
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.

Visit the last successful build: tree-sitter-lean4-0.2.1

Tree-Sitter-Lean4

Language bindings for Rust programs to parse Lean 4 source code. Lean4 is a programming language, commonly used for mathematical theorem proving as a proof assistant.

Installation

Cargo

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

The parser is automatically generated by the build script in build.rs if it is missing. This requires tree-sitter and a C compiler installed.

Usage

Rust

See Tree-Sitter-Rust.

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.

Nix Flake

This grammar is available as a Nix flake with the following outputs:

packages.<system>.grammar - The tree-sitter grammar
overlays.default - Adds grammar to pkgs.tree-sitter.builtGrammars.tree-sitter-lean
devShells.<system>.default - Development environment with tree-sitter, ast-grep, etc.

See Nixpkgs tree-sitter documentation for integration 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:

{
  inputs.tree-sitter-lean.url = "github:yourusername/tree-sitter-lean";

  outputs = { self, nixpkgs, tree-sitter-lean }: {
    devShells.x86_64-linux.default = nixpkgs.legacyPackages.x86_64-linux.mkShell {
      packages = [ nixpkgs.legacyPackages.x86_64-linux.ast-grep ];
      shellHook = ''
        ln -sf ${tree-sitter-lean.packages.x86_64-linux.grammar}/parser tree-sitter-lean.so
      '';
    };
  };
}

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 $_x := $_body' your-file.lean

Note that you can't just use write any expression in the -p argument. Expression are not valid at the top-level in Lean program in general.

Development

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

License

MIT

tree-sitter-lean4 0.0.4