Get started

Danger

Webleank is experimental and in the early stages of development.

Note

There is little reason to use Webleank with VS Code or Neovim. The official Lean 4 VS Code extension and the lean.nvim plugin are more stable and full featured solutions.

Tip

Consider starting with Lspleank first. It does not provide proof state interactivity, but it is more stable and solves a number of interoperability issues between the official Lean LSP server and LSP-compatible editors in general.

1. Install webleank

Webleank is available as a Python package. The traditional approach to installing a Python package is to use pip by running:

python3 -m pip install webleank

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 webleank as your LSP server 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:

webleank connect

3. Open your favorite sidekick app

When you have a .lean file open in your editor, open a Lean editor sidekick app such as p.lean.castedo.com.

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.