vim support?

Stream: lean4

[Simon Cruanes]

Just wondering if anyone has syntax coloring for vim :smile:
I got the LSP to work, at least:
vim.png

[Sebastian Ullrich]

Hah, that was fast! LSP for the win!

[Sebastian Ullrich]

Sadly I never really went back to vim after being forced to use Emacs for Lean (2), but surely you can borrow the highlighting from the Lean 3 vim extension?

[Gabriel Ebner]

@Julian Berman has been recently improving the vim plugin: https://github.com/Julian/lean.nvim
The "normal" vim plugin has always used LSP for autocompletion/goal view/go-to-definition/etc.: https://github.com/leanprover/lean.vim
EDIT: this is all for lean 3, but you just need to change the server executable path.

[Julian Berman]

Yeah it works for Lean 4 too.

[Julian Berman]

If you want to use both, I made a small thing called frankenlean for myself which contains:

#!/usr/bin/env python3
from pathlib import Path
import os
import sys


if Path("leanpkg.toml").exists():
    argv = ["lean-language-server", "--stdio", "--"]
else:
    argv = ["lean4", "--server"]

os.execvp(argv[0], argv + sys.argv[1:])

and then set that as the LSP command.

[Julian Berman]

@Gabriel Ebner I'm happy to donate that new neovim plugin by the way if that's useful / others care about this at all.

[Julian Berman]

I just added support for crudely adding as many sorrys as there are goals.

[Simon Cruanes]

the LSP server gives me errors/info, but no completions apparently. Like I type Nat. <tab> (which works on other LSPs) and get nothing. Is there a path that needs to be given to the server?

[Julian Berman]

It works here -- what LSP client did you use?

[Julian Berman]

(Tab completion that is)

[Sebastian Ullrich]

There is no auto completion support in the Lean 4 server so far

[Wojciech Nawrocki]

Note that completion isn't implemented for Lean 4 yet, but for Lean 3 it should work.

[Julian Berman]

Oh hm not sure actually -- it is giving some results but.. yeah they don't resolve

[Simon Cruanes]

I actually use neovim and LanguageClient

[Simon Cruanes]

Good to know, that completion isn't there yet! :)

[Julian Berman]

Yeah sorry the results I was getting were from non-LSP returned results (they were from other open buffers).

[Marc Huisinga]

the lean4 server supports the features stated in the README of vscode-lean4: https://github.com/mhuisi/vscode-lean4
i will update the readme as we build support for more requests.