Kate

Kate has LSP support built in, but you still need to do some configuration for Lean.

Step 1: Syntax highlighting (& file extension association)

Download the KDE Syntax Highlighting XML file for Lean by Hagb.

mkdir -p ~/.local/share/org.kde.syntax-highlighting/syntax/
cd ~/.local/share/org.kde.syntax-highlighting/syntax/
curl -O https://gist.githubusercontent.com/Hagb/df9044a81525aff0f6b44f4fae3270c0/raw/3e349203ee40f552d84292d26c0b9f8a8bef76f0/lean.xml

For other non-Linux operating systems, see the end of this page.

Step 2: LSP

Let Kate know how to run lspleank. You do this by adding the lspleank lake command to your ~/.config/kate/lspclient/settings.json file, e.g.:

{
    "servers": {
        "lean": {
            "command": ["lspleank", "lake"],
            "highlightingModeRegex": "^Lean$"
        }
    }
}

Alternatively, you can do this through the Kate GUI via:

Settings → Configure Kate ... → LSP Client → User Server Settings

Tip

To use the experimental Webleank, replace ['lspleank', 'lake'] with ['webleank', 'connect'].

Other filesystem locations

Other filesystem locations from the Syntax Highlighting Engine README:

For local user	$HOME/.local/share/org.kde.syntax-highlighting/syntax/
For Flatpak packages	$HOME/.var/app/package-name/data/org.kde.syntax-highlighting/syntax/
For Snap packages	$HOME/snap/package-name/current/.local/share/org.kde.syntax-highlighting/syntax/
On Windows®	%USERPROFILE%\AppData\Local\org.kde.syntax-highlighting\syntax\
On macOS®	$HOME/Library/Application Support/org.kde.syntax-highlighting/syntax/