-
Notifications
You must be signed in to change notification settings - Fork 28
The lean.nvim Manual
lean.nvim's goal is to provide a full-featured experience using Lean and to enable combining this experience with the wider ecosystem of Neovim plugins.
Many of us already use Neovim across other programming languages, and hope to carry over what we are familiar with when using Lean.
Inspired somewhat by the VSCode Manual, this page documents how to use lean.nvim.
In doing so it is somewhat prescriptive in how you use the plugin; if you are an experienced (Neo)vim user with strong personal preferences, you certainly can ignore sections below, but if you aren't, you might find what's here useful regardless of whether it is Lean-specific or not.
Please feel free to send feedback or additional questions if there's something you had hoped would be answered here, or to simply edit the page!
Neovim is available for every major operating system. You should install it via your package manager, unless it provides only an out of date version. If that is the case, you can find binaries provided on the Neovim releases page which should work for you. See also Neovim's own short installation documentation.
lean.nvim does not currently assist in installing Lean itself.
You should proceed with installing Lean's version manager elan or proceed with installation via the community-built installation script for your operating system.
There are a number of plugin managers for Neovim whose purpose is to make it easier to install third party plugins for the editor.
Every few years someone invents a new one, and many people move over to it.
Neovim even ships with a small internal one which is based on the venerable pathogen.vim.
Subjectively, most users still use some plugin manager beyond :packadd, with the most popular currently seemingly being lazy.nvim.
Other examples are pckr.nvim or vim-plug.
In general, lean.nvim should work with any of the above, as after all any plugin manager ultimately works by modifying the runtimepath within Neovim in essentially similar ways.
If you have no preference, lazy.nvim is well designed, fast, reasonably simple to configure, well documented and has a responsive maintainer.
It's what I (@Julian) currently use.
Separate from a plugin manager is a distribution of Neovim, which will typically package up some opinionated way of laying out configuration along with tweaks to the editor defaults and most often a recommended set of third party plugins.
Here, there are two philosophies. Using a distribution (of neovim or any piece of complex software) is attractive to those getting started because they get you up and running quickly, because they generally save upfront time in figuring out the basics of a configuration layout, and because they often come with lots of additional functionality which you would anyways be looking for.
The disadvantage is that distributions often contain lots of things you won't use, and worse, make debugging much harder as they change default behavior in a way that often leads to "how do I make Neovim stop doing XYZ" when in fact Neovim does not do XYZ by default in the first place.
If you want opinionated advice, I (@Julian) would recommend you perhaps copy the layout of a distribution, but not actually install any additional plugins until/unless you find one which solves a real problem -- in other words, install plugins one at a time as you find them, not in bulk.
All the above being said LazyVim (not to be confused with the package manager it uses, lazy.nvim) and kickstart.nvim both seem like good options for new users, and from what I (@Julian) have seen do not ship with lots of cruft. So use them if they suit you.
Neovim will set endofline by default, ensuring that files always end with a line terminator.
You generally shouldn't modify this setting, particularly if you are contributing to Mathlib, which ensures that VSCode has the behavior Neovim has by default in this manner.
The infoview is the main interactive component of Lean. It displays information about any current proof state, and can render additional interactive elements which Lean calls "widgets".
lean.nvim's infoview is a rich neovim buffer -- it contains interactive elements beyond what is typical in a file.
It also automatically updates as you move through a Lean file.
If you haven't configured lean.nvim to do otherwise, whenever you enter a Lean file, an infoview will automatically be opened.
If you wish to close it, you can call require('lean.infoview').close() or require('lean.infoview').toggle() (the latter of course can also be used to reopen it).
When mappings are enabled, toggling the infoview is bound to <LocalLeader>i.
There are a number of settings you can configure to slightly tweak what you see in lean.nvim's infoview.
These view options can be interactively tweaked by calling require('lean.infovew').select_view_options() which will open a floating window inside the infoview window.
When mappings are enabled, you can also use <LocalLeader>v to bring this window up from within any Lean window.
With the view options window open, use the <Tab> key to toggle any of the options from selected to unselected or vice versa.
Press <Enter> to confirm your selections and the infoview will update, or <Esc> will cancel your selection and leave the options as they were.
You can also use the K key on top of any option to get more information about what it configures.
You can jump into the current infoview using the require('lean.infoview').go_to() function should you wish to navigate around it, copy things out of it, etc.
When mappings are enabled, this function is also bound to <LocalLeader><Tab> in normal mode from any Lean file.
lean.nvim configures three filetypes:
-
leanfor Lean source code files -
leaninfofor Lean infoview windows -
leanstderrfor windows opened to show error messages emitted on standard error by the Lean language server (this is much less common to interact with than the first two)
For any Neovim filetype, including the above, you can customize the behavior of buffers with the given filetype by adding your customizations to an ftplugin file.
For example, if you want to enable spell checking in Lean buffers, you might add the line vim.wo.spell = true to a file you can create at ~/.config/nvim/after/ftplugin/lean.lua, which will run any time a buffer of type lean is opened.
Lean will often send back code actions, which are small activatable editing operations that can be triggered to insert or change some text in your Lean file[^1].
Examples of tactics which often suggest code action are the ? family of tactics, (simp?, exact?, rw?, etc.) which suggest a replacement for themselves (and the code action will perform the replacement):
Screen.Recording.2024-07-21.at.17.16.24.mov
This functionality isn't specific to Lean as a language, it works across any language server which sends code actions, so lean.nvim does not specifically interact or modify any functionality on your behalf here.
The relevant neovim function is called vim.lsp.buf.code_action.
So, how do you use them? The upcoming Neovim v0.11 will add default key mappings for this function (and a few others).
Specifically, the mapping is likely to be gra (see https://github.com/neovim/neovim/pull/28650).
If however you're not on a nightly version of neovim, or even if you are but dislike the default mapping, you should create your own mapping which simply calls this function.
Mine (@Julian)'s for instance is bound to <leader>a in normal mode and <C-a> in insert mode.
You might also be interested in using the actions-preview.nvim plugin which can show a preview of what the code action will change before you have necessarily decided on one.
Furthermore, in VSCode these show up as visually indicated yellow lightbulbs. If you are a fan of these indicators you can mirror the VSCode functionality with nvim-lightbulb.
lean.nvim can be used in Gitpod in a manner similar to VSCode.
In particular, you can use lean.nvim to contribute to Mathlib.
The Mathlib GitPod support will already install the latest stable release of Neovim for you anytime you open a Mathlib workspace in GitPod by visiting https://gitpod.io/new/?editor=xterm#https://github.com/leanprover-community/Mathlib4.
The link above should automatically select Terminal (as opposed to VSCode) as your preferred editor, which is what you should use if you intend to use lean.nvim. After starting the workspace, you'll be dropped into a terminal with Mathlib cloned and where nvim will of course open Neovim.
The key additional requirement is to ensure you have your own dotfiles being installed on GitPod workspaces, and that your own dotfiles include a Neovim setup which depends on lean.nvim!
This setting is a GitPod-wide setting, with documentation here on the GitPod site.
Set this setting once to a repository which contains your dotfiles, including a Neovim setup.
For example, for me (@Julian) I set this to https://github.com/Julian/dotfiles and thereby have these files cloned into every GitPod workspace.
If you are maintaining a project downstream of Mathlib, or if you simply wish to ensure that GitPod support is present for your repository, be sure to install Neovim in your GitPod image.
You can simply copy paste the entire Mathlib GitPod Dockerfile or you should at least ensure your own image runs the equivalent of the installation command shown there:
# install neovim (for any lean.nvim user), via tarball since the appimage doesn't work for some reason, and jammy's version is ancient
RUN curl -s -L https://github.com/neovim/neovim/releases/download/stable/nvim-linux64.tar.gz | tar xzf - && sudo mv nvim-linux64 /opt/nvimWhile an unanswerable personal question in general, we certainly hope the answer is yes!
The main thing to be aware of is that lean.nvim is a hobby project maintained externally from Lean's core development, whereas the Lean VSCode extension is used by orders of magnitude more people and maintained by the same team developing the language itself.
The experience using lean.nvim isn't quite the same as it is using VSCode.
Besides fundamental differences in the editors (notably VSCode essentially embedding a full browser, which Lean widgets are free to rely on), lean.nvim also differs a bit in how fully polished it can feel.
This is due to all three of:
- neovim plugins generally favoring programmatic configuration over graphical elements more typical in graphical IDEs
-
lean.nvimassuming you're generally familiar with Neovim functionality outside of use with Lean -
lean.nvimbeing a hobby project
lean.nvim may require a bit more digging in order to make it work how you like.
If you are familiar with other Neovim plugins, this should be nothing terribly out of the ordinary.
If you aren't, this manual may help point you towards some of what you may want to know.
lean.nvim also leaves a bit more room for user customization, rather than trying to be a uniform setup for all users.
This is consistent with the idea that Neovim is a bit more like an editor framework rather than a fully baked editor.
Users often heavily customize it to fit the way they think.
All the above being said, there definitely are a group of people using lean.nvim to do productive work in Lean!