Zed Lean 4

A Lean(4) Theorem Prover extension for Zed.

• Tree-sitter: tree-sitter-lean
• Language Server: Lean Language Server

Lean Toolchain

The Lean Language Server is integrated with the Lean toolchain. It is recommended to manage Lean toolchain versions via elan. For example, you can install the stable Lean version by running:

elan default stable
lean --version

Features

Highlight

• For optimal highlighting, set "semantic_tokens" to "combined", which will enable LSP semantic tokens highlight in Zed.

Abbreviation

• Abbreviation (unicode character) insertion is supported by snippets.

Installation

• Firstly, the extension will check path and arguments in lsp.lean4-lsp.binary settings. Then it will search lake in $PATH, try $ELAN_HOME and default directory.
• If Lean 4 is not detected, this extension can automatically install elan with default toolchain. To enable this feature, you must set "elan_auto_install" to true. You can also specify the default toolchain by setting "elan_default_toolchain" to "stable", "nightly" or "v4.28.0".
• During installation, the extension will automatically add ~/.elan to your $PATH. The Lean toolchain can be completely removed by running elan self uninstall.

settings.json Sample

{
  "semantic_tokens": "combined",
  "lsp": {
    "lean4-lsp": {
      "binary": {
        "path": "/path/to/your/.elan/bin/lake",
        "arguments": ["serve", "--"]
      },
      "settings": {
        "elan_auto_install": true,
        "elan_default_toolchain": "stable"
      }
    }
  }
}

TODO list

• Implement infoview like VSCode and Neovim
• Tree-sitter-lean is experimental and needs improvement
• Update and uninstall elan

Development

To develop this extension, see the Developing Extensions section of the Zed docs.