Get started
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.
Tip
After installing lspleanklib, you should be able to run lspleank from the command line.
You may need to start a new shell session, a new desktop session, or adjust how your
PATH environment variable is set when you launch your favorite editor.
There are no required dependencies on Linux and macOS. However, Windows requires the
Python package platformdirs to be installed. pip install lspleanklib[crossplatform]
will add platformdirs as a requirement.
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.