lean.nvim

neovim support for the Lean Theorem Prover.

lean.nvim.Demo.mp4

Prerequisites

lean.nvim requires neovim 0.5 (or newer).

Installation

Install via your favorite plugin manager. E.g., with vim-plug via:

Plug 'Julian/lean.nvim'
Plug 'neovim/nvim-lspconfig'
Plug 'nvim-lua/plenary.nvim'

" Optional Dependencies:

Plug 'hrsh7th/nvim-compe'  " For LSP completion
Plug 'hrsh7th/vim-vsnip'   " For snippets
Plug 'andrewradev/switch.vim'  " For Lean switch support

lean.nvim already includes syntax highlighting and Lean filetype support, so installing the lean.vim (i.e. non-neovim) plugin is not required or recommended.

lean.nvim supports both Lean 3 as well as the emerging Lean 4.

Lean 3

For Lean 3 support, in addition to the instructions above, you should:

Install lean-language-server, which can be done via e.g.:
$ npm install -g lean-language-server

Lean 4

For Lean 4 support, a recent Lean 4 nightly build is recommended (one at least from mid-June 2021).

In addition to the instructions above, there is experimental nvim-treesitter support being developed in https://github.com/Julian/tree-sitter-lean which can be used for enhanced indentation (TODO), text object (TODO), syntax highlighting and querying but which is still very nascent.

If you wish to try it, it can be installed by adding e.g.:

Plug 'nvim-treesitter/nvim-treesitter'
Plug 'nvim-treesitter/nvim-treesitter-textobjects'

if you do not already have tree sitter installed.

As above, many simple syntactical things are not yet implemented (help is of course welcome). You likely will want to flip back and forth between it and the standard syntax highlighting via :TSBufDisable highlight whenever encountering misparsed terms. Bug reports (to the aforementioned repository) are also welcome.

Features

abbreviation (unicode character) insertion, can also provide a nvim-compe or snippets.nvim source.
Initial implementations of some editing helpers (note: no mappings are associated with these by default unless you call lean.use_suggested_mappings() or set mappings = true in the configuration)
- <LocalLeader>i: toggle infoview
- <LocalLeader>p: pause infoview
- <LocalLeader>x: place pin
- <LocalLeader>c: clear all current pins
- <LocalLeader>s: sorry insertion corresponding to the number of open goals
- <LocalLeader>t: "try this:" suggestion replacement
- <LocalLeader>3: force a buffer into Lean 3 mode
- <LocalLeader>\: show what abbreviation would produce the symbol under the cursor
A basic infoview which can show persistent goal, term & tactic state
Hover (preview) commands:
- :LeanPlainGoal for showing goal state in a preview window
- :LeanPlainTermGoal for showing term-mode type information in a preview window
switch.vim base definitions for Lean
Simple snippets (in VSCode-compatible format, so usable with e.g. vim-vsnip)
Lean library search path access via lean.current_search_path(), suitable for use with e.g. telescope.nvim for live grepping. See the wiki for a sample configuration.

Configuration & Usage

In e.g. your init.lua:

-- If you don't already have a preferred neovim LSP setup, you may want
-- to reference the nvim-lspconfig documentation, which can be found at:
-- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-- For completeness (of showing this plugin's settings), we show
-- a barebones LSP attach handler (which will give you Lean LSP
-- functionality in attached buffers) here:
local function on_attach(client, bufnr) {
    local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
    local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
    buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
    buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
    buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')
}

require('lean').setup{
  -- Enable the Lean language server(s)?
  --
  -- false to disable, otherwise should be a table of options to pass to
  --  `leanls` and/or `lean3ls`.
  --
  -- See https://github.com/neovim/nvim-lspconfig/blob/master/CONFIG.md#leanls for details.

  -- Lean 4
  lsp = { on_attach = on_attach },

  -- Lean 3
  lsp3 = { on_attach = on_attach },

  -- Abbreviation support
  abbreviations = {
    -- Set one of the following to true to enable abbreviations
    builtin = false, -- built-in expander
    compe = false, -- nvim-compe source
    snippets = false, -- snippets.nvim source
    -- additional abbreviations:
    extra = {
      -- Add a \wknight abbreviation to insert ♘
      --
      -- Note that the backslash is implied, and that you of
      -- course may also use a snippet engine directly to do
      -- this if so desired.
      wknight = '♘',
    },
    -- Change if you don't like the backslash
    -- (comma is a popular choice on French keyboards)
    leader = '\\',
  },

  -- Enable suggested mappings?
  --
  -- false by default, true to enable
  mappings = false,

  -- Infoview support
  infoview = {
    -- Automatically open an infoview on entering a Lean buffer?
    autoopen = true,
    -- Set the infoview windows' widths
    width = 50,
  },

  -- Progress bar support
  progress_bars = {
    -- Enable the progress bars?
    enable = true,
    -- Use a different priority for the signs
    priority = 10,
  },
}

If you're using an init.vim-only configuration setup, simply surround the above with:

lua <<EOF
    require('lean').setup{
        ...
    }
EOF

Other 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)

lsp-status.nvim for showing LSP information in your status bar

lsp-trouble for showing a grouped view of diagnostics to pair with the "infauxview"

Contributing

Contributions are most welcome, as is just letting me know you use this at this point :)

Running the tests can be done via the Makefile:

$ make test

which will execute against a minimal vimrc isolated from your own setup.

Some linting and style checking is done via pre-commit, which once installed (via the linked instructions) can be run via:

$ make lint

or on each commit automatically by running pre-commit install in your repository checkout.

AlexDikelsky/lean.nvim