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 (e.g. timeout & memory settings)

If you have a configuration file for lean.nvim like ~/.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,
}

Automatically Moving the Infoview on Screen Resize

You can use the infoview.reposition function to move an infoview window to where it "belongs".

If you do so in an autocmd, specifically on VimResized events, you can move the infoview whenever the screen resizes:

vim.api.nvim_create_autocmd('VimResized', { callback = require('lean.infoview').reposition })

Semantic Highlighting

If you have enabled semantic highlighting (either once support is merged into neovim itself, or else via a plugin), you can map various token types to either your colorscheme or other highlight groups.

For example, putting the below in a file such as ~/.config/nvim/after/syntax/lean.lua will map these groups into equivalent tree-sitter highlighting groups, which should produce reasonable colors as a starting point:

-- See https://github.com/theHamsta/nvim-semantic-tokens/blob/master/doc/nvim-semantic-tokens.txt
local mappings = {
  LspKeyword = "@keyword",
  LspVariable = "@variable",
  LspNamespace = "@namespace",
  LspType = "@type",
  LspClass = "@type.builtin",
  LspEnum = "@constant",
  LspInterface = "@type.definition",
  LspStruct = "@structure",
  LspTypeParameter = "@type.definition",
  LspParameter = "@parameter",
  LspProperty = "@property",
  LspEnumMember = "@field",
  LspEvent = "@variable",
  LspFunction = "@function",
  LspMethod = "@method",
  LspMacro = "@macro",
  LspModifier = "@keyword.function",
  LspComment = "@comment",
  LspString = "@string",
  LspNumber = "@number",
  LspRegexp = "@string.special",
  LspOperator = "@operator",
}

for from, to in pairs(mappings) do
  vim.cmd.highlight('link ' .. from .. ' ' .. to)
end

Session Saving

If you want to save your nvim session to disk to recover upon re-opening nvim, you need to be careful to avoid saving the infoview windows/buffers as part of that session data, as these are handled by the plugin, and doing so will result in extraneous windows being opened when you load the session.

The builtin :mksession command with its 'sessionoptions' unfortunately doesn't seem to provide the ability to filter out such buffers/windows (at least, I wasn't able to figure it out). For that reason, I recommend making use of the resession.nvim plugin, and configuring it like so:

local resession = require('resession')
resession.setup({
  buf_filter = function(bufnr)
    -- filter out infoview windows that start with "lean:" (if you have an existing filter condition then "and" this onto that)
    return not vim.startswith(vim.api.nvim_buf_get_name(bufnr), "lean:")
  end,                                                                                                                                         
  -- good to periodically save your sessions for the time being since this plugin tends to freeze while editing Lean 4 files :(                                                                                                             
  -- (you have to initially save/load your session to activate this)                                                                                
  autosave = {
    enabled = true,
    interval = 60,
    notify = false,
  },
})

vim.keymap.set('n', '<leader>sss', resession.save)
vim.keymap.set('n', '<leader>ssl', resession.load)
vim.keymap.set('n', '<leader>ssd', resession.delete)