lean.vim

A Vim9-native Lean 4 environment. lean.vim began as a port of lean.nvim and keeps its command names, mapping conventions, and configuration shape, so shared dotfiles and muscle memory carry over — but the two projects have since diverged: this one is self-contained where lean.nvim composes with the Neovim ecosystem, adds some behavior of its own, and deliberately stops short of the interactive widget UI provided by lean.nvim. See Relationship to lean.nvim for the specifics.

It runs Lean's language server directly over Vim jobs and channels; Neovim and an external LSP client are not required.

This project owes an enormous debt to Julian Berman and the lean.nvim community. See Acknowledgements for our thanks and the specific upstream work that made the original port possible.

The initial port was reviewed against lean.nvim main at e05c0f821412337259b98cc732ff0cf6ac7afe0c (2026-07-30); development has been independent since. The most recent upstream review covered ba5663698b76677c22f5602cdbb37ab4bade1072 (2026-10-15). The October update incorporates its Unicode data, infoview folding, and sign-column improvements; exact source revisions remain recorded in NOTICE.

New here? Start with the usage guide for a task-oriented tour, or :help lean-vim9 for the full reference.

Requirements

• Vim 9.2, or a late Vim 9.1 that provides uri_encode(), built with +vim9script, +job, +channel, +popupwin, +textprop, +signs, and +timers (the plugin checks at startup and reports clearly when a build is too old)
• Lean 4 on PATH (normally installed with elan)
• lake on PATH for Lake projects

The live suite is checked against Lean 4.33.1, 4.34.1, and the current stable release (4.35.0 at this update), using Vim 9.2.0850. Lint, the offline suite, and live Lean 4.35.0 checks also pass with Vim 9.2.1202.

Installation

Put this checkout on Vim's runtimepath. Vim's native package layout is the simplest option:

mkdir -p ~/.vim/pack/plugins/start
git clone https://github.com/SamuelSchlesinger/lean.vim.git ~/.vim/pack/plugins/start/lean.vim

Enable filetype plugins and syntax in .vimrc if they are not already enabled:

filetype plugin indent on
syntax enable

Opening a *.lean file starts lake serve for a Lake project and lean --server for a standalone file. The project root is the nearest lakefile.toml, lakefile.lean, lean-toolchain, or .git marker.

Configuration

Set g:lean_config before the plugin loads. Suggested mappings are opt-in:

let g:lean_config = {
      \ 'mappings': v:true,
      \ 'infoview': {
      \   'autoopen': v:true,
      \   'orientation': 'auto',
      \   'width': 50,
      \   'height': 12,
      \ },
      \ 'abbreviations': {
      \   'leader': '\',
      \   'extra': {'wknight': '♘'},
      \ },
      \ }

The main options are:

Option	Default	Meaning
mappings	v:false	Enable the suggested buffer-local mappings
abbreviations.enable	v:true	Expand Lean Unicode abbreviations
abbreviations.leader	\	Single-character prefix used for abbreviations
completion.enable	v:true	Install the LSP omnifunc for Lean buffers
completion.autotrigger	v:false	As-you-type popup completion (identifier characters and .); off by default to spare the server while typing
completion.set_completeopt	v:true	Apply completeopt=menuone,noinsert,noselect,popup buffer-locally
inlay_hints.enable	v:true	Render LSP inlay hints as virtual text over the visible range
infoview.autoopen	v:true	Open the plain-text infoview for Lean buffers
infoview.orientation	auto	auto, vertical, or horizontal
infoview.update_cooldown	50	Throttle cursor-driven refreshes in milliseconds (0 disables throttling)
infoview.no_goals_text	Goals accomplished 🎉	Text shown when the goal list is empty
loogle.enable	v:false	Allow the Loogle commands to query loogle.lean-lang.org (the only network feature)
lsp.enable	v:true	Start the built-in Lean-specific LSP client
lsp.command	[]	Override server argv, or supply a root-to-argv function
lsp.change_delay	50	Trailing debounce for edit bursts; isolated edits flush immediately
progress_bars.enable	v:true	Show processing ranges in the sign column
semantic_highlighting.enable	v:true	Render LSP semantic tokens as text properties
semantic_highlighting.links	{}	Per-token-type highlight overrides; variable and property are unstyled by default
signs.enable	v:true	Render diagnostic and Lean goal signs

The original infoview.update_delay name remains accepted as an alias for infoview.update_cooldown.

Run :help lean-vim9-configuration for all accepted keys.

Daily use

The usage guide walks through all of this in workflow order; the highlights follow.

The default suggested mappings follow lean.nvim where there is an equivalent:

Mapping	Action
<LocalLeader>i	Toggle the infoview
<LocalLeader>p	Pause or resume infoview updates
<LocalLeader>x / <LocalLeader>c	Add / clear goal pins
<LocalLeader>dx / <LocalLeader>dc	Set / clear a textual diff pin
<LocalLeader>dd	Toggle automatic diff pins
<LocalLeader><Tab>	Move between source and infoview
<LocalLeader>\	Reverse-lookup the symbol under the cursor
<LocalLeader>r	Restart elaboration for the current file
<LocalLeader>g	Show the current goal in a popup
<LocalLeader>a	Select a code action
K	Show hover information

All mappings target <Plug> names, so users can bind their own keys without enabling the suggested set.

The most useful commands are:

• :LeanGoal, :LeanTermGoal, :LeanLineDiagnostics, :LeanDiagnosticsList, :LeanHover
• :LeanInfoviewToggle, :LeanInfoviewAddPin, :LeanInfoviewClearPins
• :LeanRestartFile, :LeanRestartServer, :LeanStatus, :LeanHealth
• :LeanDefinition, :LeanDeclaration, :LeanReferences, :LeanRename
• :LeanCodeAction, :LeanSorryFill, :LeanOutline, :LeanWorkspaceSymbols
• :LeanModuleImports, :LeanModuleImportedBy, :LeanSearchPaths
• :LeanInlayHintsToggle, :LeanLoogle / :LeanLooglePopup (opt-in), :LeanAbbreviationsReverseLookup

Completion works out of the box with <C-x><C-o>. Enable completion.autotrigger for identifier and dot completion as you type. Both modes run asynchronously, load documentation for the selected item, and apply its text edits as one undoable change. Theorems are tagged t in the menu. Inlay hints render as virtual text over the visible portion of the file and follow scrolling.

Inside the infoview, <CR> jumps the source window to the entry under the cursor (position header, pin, or diagnostic), and the view is syntax highlighted. A statusline component is available with set statusline+=%{lean#StatuslineProgress()}.

Unicode abbreviations expand on Space, Tab, Enter, or leaving Insert mode. The full abbreviation table is synchronized from lean.nvim's VS Code data. While an abbreviation is in progress, completion stays out of the way. Lean buffers reserve a sign column to keep diagnostics from shifting the text. The infoview uses manual folding, so source-window folding rules cannot hide goals or diagnostics.

Relationship to lean.nvim

lean.vim began as a faithful port and stays compatible on the surface: command names, <LocalLeader> mapping conventions, and configuration keys mirror lean.nvim wherever both projects implement a feature. Core editing is implemented directly in Vim9: server lifecycle, document synchronization, completion, inlay hints, goals, term goals, diagnostics, progress, semantic tokens, hover/navigation, code actions, workspace edits, pins, abbreviations, syntax, indentation, snippets, document/workspace symbols, and module queries.

Since the initial port the projects have diverged in both directions.

Where lean.vim goes its own way:

• Self-contained where lean.nvim delegates. Completion (async omnifunc plus as-you-type popup) and inlay hints are built in; lean.nvim relies on Neovim's LSP client and a completion plugin for those. The LSP transport itself is a small, auditable Vim9 client rather than vim.lsp.
• Rendering scaled for large files. Progress signs and inlay hints decorate only the visible range and follow scrolling, and a failed server start backs off instead of retrying on every window switch.
• Additions without an upstream equivalent: :LeanHealth, a Telescope-free opt-in Loogle commands, and lean#StatuslineProgress().

Where lean.nvim remains ahead — deliberately not emulated here:

• ProofWidgets, clickable subexpressions, widget tooltips, and terminal graphics need Neovim's extmark and Lua UI substrate. The infoview uses Lean's stable $/lean/plainGoal and $/lean/plainTermGoal requests, with plain text, syntax highlighting, and <CR> jumps instead of an interactive render tree. Live pins track source edits and refresh their goals through the same plain-goal interface.
• Telescope and satellite.nvim integrations are replaced by quickfix, location lists, and the sign column.

Widget commands exist for command-name compatibility and explain this boundary when invoked.

Architecture

The transport is intentionally self-contained — depending on a second Vim LSP plugin would tie goal requests, restart behavior, and Lean-specific notifications to a third party's extension hooks.

• autoload/lean/lsp.vim: transport, project sessions, document synchronization, and the stable client API.
• documents.vim and requests.vim: document lifetimes, revision snapshots, request cancellation, and checks before delivering asynchronous results.
• decorations.vim, semantic.vim, and workspace.vim: diagnostic/progress rendering, semantic highlighting, and checked workspace-edit transactions.
• infoview.vim, infoview_render.vim, and pins.vim: view state and windows, pure text rendering, and live source anchors.
• completion.vim, inlayhints.vim, abbreviations.vim, and editor.vim: editing features; health.vim and loogle.vim: diagnostics and opt-in search.
• autoload/lean.vim: commands, mappings, and feature lifecycle coordination.

The import graph is acyclic and checked by make lint. See ARCHITECTURE.md for ownership rules and extension points.

Validation

make lint       # compile every Vim9 module
make test       # fake-server transport and editor integration
make test-live  # end-to-end check against the installed Lean server
make license-check # verify pinned third-party files and required notices
make hooks      # run lint and the offline suite before commits and pushes

CI runs make lint, make test, and make test-live on Linux and macOS for every push and pull request, with Lean 4.33.1, 4.34.1, and stable (.github/workflows/test.yml). The stable job picks up new Lean releases without changing a project's lean-toolchain. make hooks points core.hooksPath at .githooks/ so the same lint, license, and headless test checks run locally before every commit and push (skip with --no-verify when needed). Local hooks keep the live tests optional, since they need an installed Lean toolchain.

Use ELAN_TOOLCHAIN=leanprover/lean4:v4.35.0 make test-live to select an installed toolchain. Set LEAN_VIM_TEST_VIM=/path/to/vim to check another Vim build, or LEAN_VIM_TEST_TIMEOUT to override the per-script timeout in seconds. For an uninstalled Vim source build, also set VIMRUNTIME to its runtime/ directory.

The fake server supports named scenarios and explicit release of held replies; asynchronous tests can choose delivery order without server sleeps. The headless runner catches script errors and limits each test to two minutes, terminating the test's process group on Linux and macOS. See test/support/README.md for the harness.

The headless tests cover split JSON-RPC frames, full pipes in both directions, file reloads, initialization and graceful shutdown, request cancellation, failed-start backoff, diagnostics, progress (including large-file sign capping), goals, term goals, semantic tokens, completion (async popup, UTF-16 textEdits, cancellation, resolve, abbreviation interplay), inlay hints, infoview jumping, document and workspace symbols, UTF-16 incremental changes, restart races, workspace-edit preflight, live pin tracking, paused pins, stale-edit rejection, crash recovery across buffers, tab and ftplugin lifecycle, indentation, and Unicode abbreviation insertion. The live test checks tactic and term goals (including Unicode lambda proofs and edits during document debouncing), live pin movement and goal refresh, completion acceptance, diagnostic updates, Lake startup, and search paths against real Lean processes.

License

The port and the retained lean.nvim syntax/snippet material are MIT-licensed. The Unicode abbreviation data is Apache-2.0. See NOTICE for exact file provenance and ACKNOWLEDGEMENTS.md for project credit.