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.

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.nvim assuming you're generally familiar with Neovim functionality outside of use with Lean
• lean.nvim being a hobby project

While there is certainly no desire to make things obtuse, 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 presuming a fully standard setup across 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 of the above being said, there's certainly a need to point towards what features or functionality are likely to be useful for a pleasant user experience. Inspired somewhat by the VSCode Manual, this page attempts to collect a number of these tips. In doing so it is a bit more prescriptive; if you are an experienced user, or if you have strong personal preference, you certainly may ignore it, but if you aren't, the hope is you might find it useful at least to alert you to functionality you might be interested in. Please feel free to send feedback or additional questions if there's something you had hoped would be answered here. You are also welcome to directly edit this page.

Installing Lean

Configuring lean.nvim

lean.nvim configures two filetypes:

• lean for Lean source code files
• leaninfo for Lean infoview windows

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.

FAQ

Should I use lean.nvim?

While 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.

Nonetheless, lean.nvim still has going for it that you are likely already interested or invested in Neovim, which arguably can be nimbler and more powerful of an editor. And there definitely are a group of people using it to do productive work in Lean!

Key Mappings

Telescope and Workspace Navigation

Ignoring Infoviews

oleans and ileans

Language Server Functionality

Handling Lean Restarts & Refreshing Dependencies

Configuring End-Of-Line Behavior

Window & Text Widths

Code Actions

Jumping Into & Out of the Infoview