Helix

Tip

The author of Lean-TUI uses Helix, and Lean-TUI implements a concept similar to an editor sidekick with Webleank.

Helix has built-in LSP support, but to try Lspleank, you need to configure the LSP command to run for .lean files.

Edit your ~/.config/helix/languages.toml (or equivalent) with the following override:

[language-server.lean]
command = "lspleank"
args = ["lake"]

In older versions of Helix, you might need to add more configuration, such as:

[[language]]
name = "lean"
language-servers = ["lean"]