-
Notifications
You must be signed in to change notification settings - Fork 29
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 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 portions below, but if you aren't, you might find what's here useful to alert you to functionality you might be interested in regardless of how specific it is to Lean. 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.
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.
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.
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.
lean.nvim
can be used in GitPod in a manner somewhat 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/#https://github.com/leanprover-community/Mathlib4.
If your intention is to use lean.nvim
and not VSCode in any form, you should pick Terminal
as your desired editor:
which will immediately drop you 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/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.
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
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!