Lean for vim9

[castedo]

In vim9, I have replicated some the functionality of the lean-nvim plugin.

Are there any projects or efforts to backport lean-nvim functionality to vim9? I did not find anything online.

I have tentative plans to document this vim9 configuration and replicate more of the lean-nvim functionality into vim9. Although I am currently using neovim to learn Lean, I'm hoping to eventually use just vim.

[Julian]

Hi. No, I have no plans to do so personally and have not seen any other mentions of vim in the ecosystem.

[castedo]

I have packaged the Vim 9 LSP setup I'm using with Lean at
https://gitlab.com/castedo/vim9-lean with mirror https://github.com/castedo/vim9-lean.

Online documentation is at https://castedo.gitlab.io/vim9-lean/.

@Julian Does the warning and pointer to lean.nvim at the top of this new online documentation look appropriate to you?

I figure I'll announce it soon in the Zulip channel.

At the moment, I think the only important feature I'm missing is proof state shown in an Infoview window. At the moment this seems like it will be hard to implement. But I'm hoping there is some clever way to approximate it from Vim 9.

[Julian]

(the doc link is private which may not be intended but I can see the message in the source)

Being able to see the infoview is pretty essential, Lean is near unusable without it -- adding support for it was essentially the first thing I did for lean.nvim. There's some more info here which you might find helpful.

That being said I certainly have no concerns (the link to here is certainly good with me) --, everyone should use the setup they like, and me stubbornly deciding I wanted a Neovim plug-in was how this one was born!

[castedo]

My current plan is to not implement InfoView within vim 9 and instead find or make an "Editor-decoupled file-watching proof-state-outputing tool" as described in this Zulip topic.

I haven't learned enough Lean yet to know whether this is a dumb idea or not. 🤣

This is in a similar spirit to how I do not plan on implementing Unicode input in vim 9 because that feature need not be coupled to editors.