Configuring & Extending

This page collects a number of additional links or snippets which may be helpful for Lean.

Feel free to add your own, or add links to your dotfiles.

Preventing the Progress Bars from Horizontally Shifting Your File

By default, (neo)vim will automatically show and hide the "sign column", which is where lean.nvim shows progress information (in highly technical terms, "orange bars").

If you prefer that the sign column be shown always, even when no orange bars are shown indicating progress, the vim option to do so is:

vim.opt.signcolumn = "yes"

which you can put in your configuration.

Mathlib Style Linting

The below configuration for nvim-lint:

local lint = require('lint')

lint.linters.mathlib = {
  cmd = 'scripts/lint-style.py',
  stdin = false,
  stream = 'stdout',
  ignore_exitcode = true,
  parser = require('lint.parser').from_errorformat('::%trror file=%f\\,line=%l\\,code=ERR_%[A-Z]%\\+::ERR_%[A-Z]\\*:%m'),
}

lint.linters_by_ft = { lean3 = {'mathlib'} }

should work for showing mathlib style lint errors inline:

Live Grep

Configuration

Passing arguments to the lean server (timeout and memory settings)

If you have a configuration file for lean.nvim like ~/.config/neovim/plugin/lean.lua or ~/.config/nvim/plugin/lean.lua (as described in these getting started instructions), you can have nvim pass arguments to the lean server on startup. This can be used to set lean options like timeout and memory.

In that file, find the block like

require('lean').setup{
   ... = ...,
}

and add a field cmd to the value for lsp3 (or lsp) like so:

require('lean').setup{
  -- whatever other options you set
  lsp3 = {
    cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '3000000' },
    -- on_attach = on_attach or whatever else you set here
  },
}

resulting in e.g.

require('lean').setup{
    abbreviations = { builtin = true },
    lsp = { on_attach = on_attach },
    lsp3 = { on_attach = on_attach,
             cmd = { 'lean-language-server', '--stdio', '--', '-M', '4096', '-T', '3000000' },
             },
    mappings = true,
}