Quickstart for Lean 4 and vim

When it comes to the latest technology I am a bit of an old stick in the mud. I like old, boring programming languages and old, boring programming tools. I get that times are changing, and that's why when I am hiring, mentoring, or coaching junior software engineers I encourage them to use Microsoft VS Code. But for myself, I use vim, a text editor first released back in 1991.

I know there are a few others like me who use vim or eschew VS Code for ideological reasons or just 'cause. So I was a bit dismayed to see that the official instructions for a Quickstart with Lean 4 begin with:

1. Install VS Code

Fortunately, Lean comes out of the box with support for the language server protocol (a great open source contribution by Microsoft coming from the VS Code project, actually), and vim has several plugins for language servers. So, in theory, it shouldn't be too hard to get some Lean 4 support, right?

Now, at this point I should pause to point out prior art. There's vim-lean which hasn't been touched since 2017 (Lean 4 was released in 2021). And there's lean.nvim, which includes many more useful features then what you'll see here. But for some reason I am entirely unable to type

sudo dnf install neovim -y

so we will persist with the OG vim. So let's proceed with installing Lean 4 and getting it to work with vim...

Installing Lean 4, no VS Code

We'll install

Lean 4
vim-plug (a plugin managed for vim)
vim-lsp (an async language server protocol plugin for vim)

1. Install elan, the Lean version manager.

You should be able to check the install was successful by doing:


	$ elan
	elan 3.1.1 ....

	$ lean --version
	Lean (version 4.10.0, x86_64-unknown-linux-gnu, commit c375e19f6b65, Release)

	$ lake --version
	Lake version 5.0.0-c375e19 (Lean version 4.10.0)

You may need to restart your shell or do something like

source ~/.bash_profile

to update the changes to your local PATH.

2. Install vim-plug.

3. Install vim-lsp.

Edit your ~/.vimrc file to add in

 Plug 'prabirshrestha/vim-lsp'

Overall you should have a section that looks like this:

call plug#begin()
# ... your other plugins
plug 'prabirshrestha/vim-lsp'
call plug#end()

Reboot vim and then run ":PlugInstall".

4. Add Lean 4 Language Server support.

Alas vim-lsp-settings does not support Lean out of the box, so we'll have to improvise a bit.
Edit your ~/.vimrc again and after the `call plug#end()` add the following:

    if executable('lake')
 au User lsp_setup call lsp#register_server({
     \ 'name': 'lean4-lsp',
     \ 'cmd': {server_info->['lake', 'serve']},
     \ 'allowlist': ['lean'],
     \ })
endif

Note that you must have lean (and lake) in your PATH for this to work, see step 1.

And there you have it! You can create an empty project with `lake init` and try it out. Here is me using language server features on the empty lean project:

Note: if you'd like syntax highlighting, try adding `Plug 'Julian/lean.vim'` before the `vim-lsp` line.