Zulip Chat Archive

Stream: lean4

Topic: vim support?


view this post on Zulip Simon Cruanes (Jan 05 2021 at 21:14):

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

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 21:15):

Hah, that was fast! LSP for the win!

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 21:18):

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?

view this post on Zulip Gabriel Ebner (Jan 05 2021 at 21:27):

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

view this post on Zulip Julian Berman (Jan 05 2021 at 21:34):

Yeah it works for Lean 4 too.

view this post on Zulip Julian Berman (Jan 05 2021 at 21:35):

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.

view this post on Zulip Julian Berman (Jan 05 2021 at 21:36):

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

view this post on Zulip Julian Berman (Jan 05 2021 at 21:36):

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

view this post on Zulip Simon Cruanes (Jan 05 2021 at 21:37):

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?

view this post on Zulip Julian Berman (Jan 05 2021 at 21:38):

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

view this post on Zulip Julian Berman (Jan 05 2021 at 21:38):

(Tab completion that is)

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 21:39):

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

view this post on Zulip Wojciech Nawrocki (Jan 05 2021 at 21:39):

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

view this post on Zulip Julian Berman (Jan 05 2021 at 21:39):

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

view this post on Zulip Simon Cruanes (Jan 05 2021 at 21:45):

I actually use neovim and LanguageClient

view this post on Zulip Simon Cruanes (Jan 05 2021 at 21:46):

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

view this post on Zulip Julian Berman (Jan 05 2021 at 21:46):

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

view this post on Zulip Marc Huisinga (Jan 05 2021 at 21:46):

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.


Last updated: May 07 2021 at 12:15 UTC