lean.nvim

Neovim support for the Lean Theorem Prover

demo.mp4

Sponsors

A portion of lean.nvim's development is graciously sponsored by the Lean FRO. It is undoubtedly the case that lean.nvim would not be as featureful without the support, for which we owe sincere thanks.

Installation

lean.nvim can be installed via your favorite plugin manager. Here's an example doing so with lazy.nvim:

{
  'Julian/lean.nvim',
  event = { 'BufReadPre *.lean', 'BufNewFile *.lean' },

  dependencies = {
    -- optional dependencies:

    -- a completion engine
    --    hrsh7th/nvim-cmp or Saghen/blink.cmp are popular choices

    -- 'nvim-telescope/telescope.nvim', -- for Lean-specific pickers
    -- 'andymass/vim-matchup',          -- for enhanced % motion behavior
    -- 'andrewradev/switch.vim',        -- for switch support
    -- 'tomtom/tcomment_vim',           -- for commenting
  },

  ---@type lean.Config
  opts = { -- see the manual for full configuration options
    mappings = true,
  }
}

lean.nvim supports the latest stable neovim release (currently >=0.11.5) as well as the latest nightly. If you are on an earlier version of neovim, e.g. 0.10.2, you can have your plugin manager install the nvim-0.10 tag until you upgrade.

Features

• Abbreviation (unicode character) insertion (in insert mode & the command window accessible via q/)

• An infoview which can show persistent goal, term & tactic state, as well as interactive widget support (for most widgets renderable as text)

• User commands for interacting with infoviews, goals, diagnostics, and the Lean server (e.g. :LeanGoal, :LeanInfoviewToggle, :LeanRestartFile)

• File progress information for visible lines in the sign column. If satellite.nvim is present, a satellite extension is registered for showing progress information for the whole document within its floating window.

• vim-matchup definitions for Lean

• switch.vim base definitions for Lean

• If telescope.nvim is present, a :Telescope loogle command is available as a frontend for the Loogle JSON API.

• Semantic highlighting support -- see the manual for full details and the wiki for a sample color scheme setup

• Simple snippets (in VSCode-compatible format, usable with e.g. vim-vsnip)

• Lean library search path access via lean.current_search_path(), which you might find useful as a set of paths to grep (or live grep) within See the wiki for a sample configuration.

Configuration & Usage

The short version -- if you followed the instructions above for lazy.nvim, you likely simply want opts = { mappings = true } to call lean.setup and enable its default key mappings.

This is all you need if you already have something registered to run on the LspAttach autocmd which defines any language server key mappings you like, e.g. if you use Neovim with any other language. In particular your LspAttach handler should likely bind things like vim.lsp.buf.code_action (AKA "the lightbulb") to ensure that you have easy access to code actions in Lean buffers. Lean uses code actions for replacing "Try this:" suggestions, which you will almost certainly want to be able to perform.

If you do not already have a preferred setup which includes LSP key mappings and (auto)completion, you may find the fuller example here in the wiki helpful.

If you are using another plugin manager (such as vim-plug), after following the installation instructions, add the below to ~/.config/nvim/plugin/lean.lua or an equivalent:

require('lean').setup{ mappings = true }

For more detail on the full list of supported configuration options, key mappings, and commands, see the manual.

(If you find you can't modify your source files due to the nvim E21 error, this might be due to lean.nvim's effort prevent users from accidentally shooting themselves in the foot by modifying the Lean standard library. See the nomodifiable option in the full configuration.)

Other Useful Plugins

Particularly if you're also a VSCode user, there may be other plugins you're interested in. Below is a (hopelessly incomplete) list of a few:

• nvim-lightbulb for signalling when code actions are available

• goto-preview for peeking definitions (instead of jumping to them)

• neominimap.nvim if you really like minimaps

Contributing

Contributions are most welcome. Feel free to send pull requests for anything you'd like to see, or open an issue if you'd like to discuss. See CONTRIBUTING.md for details on running tests, linting, and manual testing.