Lean.nvim

<div align="center"> <div> <div><img alt="lean.nvim" src="https://github.com/user-attachments/assets/727b689d-56f6-48e8-8fe5-a7a5d82b91c5" width="400px"/></div> <div><h1>lean.nvim</h1></div> </div> <table> <tr> <td> <strong><a href="https://neovim.io">Neovim</a> support for the <a href="https://lean-lang.org/">Lean Theorem Prover</a></strong> </td> </tr> </table>

<a href="https://dotfyle.com/plugins/Julian/lean.nvim"> <img alt="dotfiles using lean.nvim" src="https://dotfyle.com/plugins/Julian/lean.nvim/shield?style=for-the-badge" /> </a>

</div>

https://github.com/user-attachments/assets/d17554ae-bcce-4f73-ac34-38ae556caf45

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 = {
    'nvim-lua/plenary.nvim',

    -- optional dependencies:

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

    -- 'nvim-telescope/telescope.nvim', -- for 2 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 below 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)

• Hover (preview) commands:

  • :LeanGoal for showing goal state in a preview window

  • :LeanTermGoal for showing term-mode type information in a preview window

• 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.

• 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 }

More detail on the full list of supported configuration options can be found below.

(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 definition of nomodifiable below.)

Semantic Highlighting

Lean supports semantic highlighting, in which the Lean server itself will signal how to highlight terms and symbols within the editor using information available to it.

Note that even though neovim supports this highlighting, you still will want to map the semantic highlighting groups to your color scheme appropriately. For a sample setup, see the wiki.

Mappings

If you've set mappings = true in your configuration (or have called lean.use_suggested_mappings() explicitly), a number of keys will be mapped either within Lean source files or within Infoview windows:

In Lean Files

The key binding <LocalLeader> below refers to a configurable prefix key within neovim. You can check what this key is set to within neovim by running the command :echo maplocalleader. An error like E121: Undefined variable: maplocalleader indicates that it may not be set to any key. This can be configured by putting a line at the top of your ~/.config/nvim/init.lua of the form vim.g.maplocalleader = ' ' (in this example, mapping <LocalLeader> to hitting the space key twice).

| Key | Function | | -------------------- | ------------------------------------------------------------------- | | <LocalLeader>i | toggle the infoview open or closed | | <LocalLeader>p | pause the current infoview | | <LocalLeader>r | Restart the Lean server for the current file. | | <LocalLeader>v | interactively configure infoview view options | | <LocalLeader>x | place an infoview pin | | <LocalLeader>c | clear all current infoview pins | | <LocalLeader>dx | place an infoview diff pin | | <LocalLeader>dc | clear current infoview diff pin | | <LocalLeader>dd | toggle auto diff pin mode | | <LocalLeader>dt | toggle auto diff pin mode without clearing diff pin | | <LocalLeader><Tab> | jump into the infoview window associated with the current lean file | | <LocalLeader>\\ | show what abbreviation produces the symbol under the cursor |

[!TIP] See :help <LocalLeader> if you haven't previously interacted with the local leader key. Some nvim users remap this key to make it easier to reach, so you may want to consider what key that means for your own keyboard layout. My (Julian's) <Leader> is set to <Space>, and my <LocalLeader> to <Space><Space>, which may be a good choice for you if you have no other preference.

[!TIP] If you are also looking for a way to restart the Lean server entirely (rather than just refresh the current file), the current Neovim way to do so is to run vim.lsp.enable('leanls', false) followed by vim.lsp.enable('leanls'), which stops the LSP client and then restarts it respectively. You may wish to bind one of these to a key if you find yourself doing it often; these operations work for any language server and any language, not just Lean.

In Infoview Windows

| Key | Function | | -------------------- | ----------------------------------------------------------------- | | <CR> | click a widget or interactive area of the infoview | | K | click a widget or interactive area of the infoview | | gK | "select" a widget or interactive area ("shift+click") | | <Tab> | jump into a tooltip (from a widget click) | | <Shift-Tab> | jump out of a tooltip and back to its parent | | <Esc> | clear all open tooltips | | J | jump into a tooltip (from a widget click) | | C | clear all open tooltips | | gd | go-to-definition of what is under the cursor | | gD | go-to-declaratio