Getting Started From the Ground Up

If whilst getting started with lean.nvim you don't already have a preferred neovim setup that includes things like (auto)completion and language server interaction, you may find a complete (but minimalistic) example helpful. Below is such an example which should give you enough to get started (or take and modify).

Install neovim

Install a recent neovim (one newer than 0.10.x, or a nightly).

On Linux, if your distribution's package manager ships this version, install it from there. Otherwise, do so from the neovim releases page. Ensure if you download it from the releases page that you put it somewhere on your shell's PATH, and that it is executable.

On macOS, the best way to do so is instead via Homebrew, which will definitely give you a new enough version. After installing Homebrew, in a terminal, run:

brew install neovim

to install the stable version.

Install lean.nvim and its dependencies

If you do not already use a plugin manager for neovim, download vim-plug following its installation instructions. The correct configuration path for neovim is likely ~/.config/nvim/init.vim on your system, so add:

call plug#begin()
Plug 'Julian/lean.nvim'
Plug 'neovim/nvim-lspconfig'
Plug 'nvim-lua/plenary.nvim'

Plug 'hrsh7th/cmp-nvim-lsp'
Plug 'hrsh7th/cmp-buffer'
Plug 'hrsh7th/cmp-path'
Plug 'hrsh7th/nvim-cmp'
call plug#end()

to your ~/.config/nvim/init.vim following the vim-plug example.

Configuration Files

Create a new file, ~/.config/nvim/plugin/lean.lua, whose contents are:

-- Always show sign column.
-- The sign column is used by the LSP support to show diagnostics
-- (the E, W, etc. characters on the side)
-- as well as by the Lean plugin to show the orange bars.
-- By default the sign column is only shown if there are signs to show,
-- which means the buffer will constantly jump right and left.
vim.opt.signcolumn = "yes:1"

-- Enable nvim-cmp, with 3 completion sources, including LSP
local cmp = require'cmp'
cmp.setup{
    mapping = cmp.mapping.preset.insert({
      ['<C-b>'] = cmp.mapping.scroll_docs(-4),
      ['<C-f>'] = cmp.mapping.scroll_docs(4),
      ['<C-Space>'] = cmp.mapping.complete(),
      ['<C-e>'] = cmp.mapping.abort(),
      ['<CR>'] = cmp.mapping.confirm({ select = true }),
    }),
    sources = cmp.config.sources({
      { name = 'nvim_lsp' },
      { name = 'path' },
      { name = 'buffer' },
    })
}

-- You may want to reference the nvim-cmp documentation for further
-- configuration of completion: https://github.com/hrsh7th/nvim-cmp#recommended-configuration

-- Configure the language server:

-- You may want to reference the nvim-lspconfig documentation, found at:
-- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
-- The below is just a simple initial set of mappings which will be bound
-- within Lean files.
local function on_attach(_, bufnr)
    local function cmd(mode, lhs, rhs)
      vim.keymap.set(mode, lhs, rhs, { noremap = true, buffer = true })
    end

    -- Autocomplete using the Lean language server
    vim.api.nvim_buf_set_option(bufnr, 'omnifunc', 'v:lua.vim.lsp.omnifunc')

    -- Support for triggering code actions (e.g. "Try this:" suggestions from `simp?`)
    cmd('n', '<leader>a', vim.lsp.buf.code_action)
    cmd('i', '<C-a>', vim.lsp.buf.code_action)

    -- <leader>n will jump to the next Lean line with a diagnostic message on it
    -- <leader>N will jump backwards
    cmd('n', '<leader>n', function() vim.diagnostic.goto_next{popup_opts = {show_header = false}} end)
    cmd('n', '<leader>N', function() vim.diagnostic.goto_prev{popup_opts = {show_header = false}} end)

    -- <leader>K will show all diagnostics for the current line in a popup window
    cmd('n', '<leader>K', function() vim.diagnostic.open_float(0, { scope = "line", header = false, focus = false }) end)

    -- <leader>q will load all errors in the current lean file into the location list
    -- (and then will open the location list)
    -- see :h location-list if you don't generally use it in other vim contexts
    cmd('n', '<leader>q', vim.diagnostic.setloclist)
end

-- Enable lean.nvim, and enable abbreviations and mappings
require('lean').setup{
    lsp = { on_attach = on_attach },
    mappings = true,
}

-- Update error messages even while you're typing in insert mode
vim.lsp.handlers["textDocument/publishDiagnostics"] = vim.lsp.with(
  vim.lsp.diagnostic.on_publish_diagnostics, {
    underline = true,
    virtual_text = { spacing = 4 },
    update_in_insert = true,
  }
)

Install

The first time you start up nvim, you may now need to run :PlugInstall to install the aforementioned plugins you configured.

You may see errors during this startup which you can ignore, they come from not having installed lean.nvim or its dependencies, but the next time you start nvim up after running :PlugInstall, they should disappear.