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.
neovim of course has a large amount of non-Lean specific functionality whose use may not be familiar to all.
Here are some examples of functionality you may want to be aware of, along with how you might use it in your Lean workflow:
It can be hard to see the contents of floating windows (such as those shown when hitting K to hover over something) without window borders.
If you prefer having them (which is recommended) you want to set:
vim.lsp.handlers['textDocument/hover'] = vim.lsp.with(vim.lsp.handlers.hover, { border = "single" })once globally somewhere in your neovim configuration, which will apply it to all languages.
There is a similar option for diagnostic floating windows which is set via e.g.:
vim.diagnostic.config{ severity_sort = true, float = { border = 'rounded' } }You will often want to move forward (or back) to the nearest error or warnings in your files.
The mechanism for doing so is vim.diagnostic.goto_next() (respectively vim.diagnostic.goto_prev()).
See the help for further details, though if you want a slightly cleverer improvement, you can find an example of how to combine jumping to the next diagnostic with opening a float only if the virtual text doesn't already show you the full error here.
When jumping back and forth to view definitions of Lean declarations (via gd) you should be aware of a few built-in features:
- Hit
<C-w>]to open definitions in a split instead of in the current buffer (see:h CTRL-W_]for further details) - You also may be interested in a plugin which opens them in floating windows, such as rmagatti/goto-preview, or to do so inline in your own configuration. See here for an example.
The jumplist (:h jumplist) is also very much your friend!
Neovim keeps a record each time you "jump" the cursor, and going to a definition is a jump.
What this means in practice is that after you hit gd, you can use <C-o> to jump back to where you were previously!
A fuzzy finder is arguably completely indispensable for modern editing with neovim.
It allows you to type subsections of "thing"s and "act" on the result.
Most simply, the "things" are often paths, and "acting" is "jumping to the file" -- so one can type something as short as alrinba<enter> and immediately jump to Mathlib/Algebra/Ring/Basic.lean.
Telescope is the most commonly used fuzzy finder for neovim at this point, so you're highly encouraged to use it.
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.
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:
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,
}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 })Lean and Neovim have joint support for semantic highlighting. This means the Lean server can tell Neovim information about what things you see in your Lean files represent, allowing for better syntax highlighting.
You can find brief information on semantic highlighting in the Lean Manual some of which is VSCode-specific (but some which is not).
In particular, you can tweak similar settings in Neovim if you do not find that variables, particularly autoImplicit ones, are well differentiated from "real" terms.
You can use e.g. vim.print(vim.lsp.semantic_highlighting.get_at_pos()) to see what semantic highlighting tokens the Lean server has sent for whatever is under your cursor.
You also should look at your own chosen Neovim theme to decide which highlight groups, if any, are ones you want to link highlights to -- in other words, if your theme has a Variable highlight group, you may want to link @lsp.type.variable to this group, making them the same color.
You likely will not need to map all of the LSP highlight groups, as Neovim maps many LSP groups to things your theme will likely color correctly by default, but it will depend on the theme.
See :h lsp-semantic-highlight for a list of available groups, and the default mapping to other highlight groups.
To parallel what's in the Lean documentation, putting the below in a file such as ~/.config/nvim/after/syntax/lean.lua will map Lean variables to the Identifier highlight group (which should make them a different color than other terms):
local mappings = {
['@lsp.type.variable'] = 'Identifier',
}
for from, to in pairs(mappings) do
vim.cmd.highlight('link ' .. from .. ' ' .. to)
endFeel free to add additional entries to the above if you notice other mis-highlighted syntax using your own theme.
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)If telescope.nvim is installed you can run :Telescope loogle
to use https://loogle.lean-lang.org from within your editor:
Pressing enter is going to insert the name of the theorem or definition you are hovering on at the current
position of your cursor.