Lspleank
Lspleank is an LSP server that enables interoperability between:
- the official Lean LSP (Language Server Protocol) server (
lake serve) and - LSP-compatible editors without Lean-specific enhancements beyond standard LSP.
By itself, lspleank does not provide support for proof state interactivity, such as that found
in the Infoview of the official Lean 4 VS Code
extension or the
lean.nvim plugin.
Webleank provides Lean-specific features like proof state interactivity,
but is in very early stages of development and not yet ready for general use.
Webleank interoperates with lspleank and uses the lspleanklib package.
For reference information, including CLI help, see the lspleanklib repository
README.