Applications
This page lists some applications that are not editors but are useful to run alongside an editor when writing in the Lean language.
Lean editor sidekick applications
A Lean editor sidekick application is a non-editor tool that detects the caret (text cursor) position in your Lean file within any editor that supports LSP. Lean-TUI is an example of an editor sidekick application.
Lean-TUI
Lean-TUI is a terminal-only (TUI) interactive proof explorer that responds to your cursor position in any editor with LSP support. It is comparable to the InfoView in the Lean 4 VS Code extension.
Danger
Lean-TUI is an early-release, experimental prototype under development.
Generic non-editor applications
System monitor
Wondering if Lean has finished processing your files so that all those LSP features are available in your editor?
You can use the system monitor included with your operating system, such as top or GNOME System Monitor. All major operating systems provide a system monitor program.