Get started
Warning
Lspleank is under development and, as of March 2026, has only been used by the initial developer (Castedo).
Note
There is little reason to use Lspleank with VS Code or Neovim. The official Lean 4 VS Code extension and the lean.nvim plugin are more stable and full-featured solutions.
1. Install lspleanklib
Lspleanklib is available as a Python package. The standard way to install a Python package is to use pip by running:
python3 -m pip install lspleanklib
There are several alternatives to pip, such as PyInstaller and
uv, each with its own trade-offs. You might prefer one of
these alternative approaches.
2. Set an LSP server command for .lean files
Follow the instructions appropriate for your editor so that the following
command is used to launch an LSP server for .lean files:
lspleank lake
Some notes on how to do this are available on this website for the following editors:
Next steps
Feel free to send a message to castedo@castedo.com, contact Castedo on https://leanprover.zulipchat.com/, or @castedoellerman:matrix.org.
For reference information, including CLI help, see the repository README.