Collaborate?

[Julian]

Hello! Hope you don't mind me opening this.

I (and thankfully others) maintain a neovim plugin for the Lean theorem prover here. The README has a quick demo for how it looks (but outdated fortunately, there's been lots of improvements since then).

I see this plugin is written in vimscript -- not sure if you have intentions for a Lua-based one for neovim (which offers lots of IMHO indispensable things for interactive theorem proving).

If you do, I suspect we'd love to collaborate on some cross-applicable functionality.

If that's ever the case feel free to reach out.

Best, -Julian

[whonore]

Hi, thanks for reaching out.

not sure if you have intentions for a Lua-based one for neovim

I don't at the moment for a couple reasons:

• I want to maintain compatibility with plain Vim.
• I'm not very knowledgeable about NeoVim or Lua and I don't have a lot of time currently to work on large-scale changes.

That being said, I would definitely be open to discussing adding some NeoVim-only features in Lua as long as someone else writes most of it and it doesn't result in having to essentially maintain two versions of the code.

which offers lots of IMHO indispensable things for interactive theorem proving

What kind of thing do you have in mind? Are they things that could be done in Python as well? I've tried to separate as much as possible the vimscript code for displaying stuff to the user (putting text in buffers, highlighting, etc) and Python code for communicating with Coq. So if what you're talking about is more to do with the latter it might not be too difficult to translate Lua into Python or vice-versa.

If you do, I suspect we'd love to collaborate on some cross-applicable functionality.

I'm definitely interested in some sort of collaboration even if that just means sharing ideas for what kinds of features to provide, and how best to take advantage of Vim/NeoVim's features to display information to the user and help them interact with it.

Maybe a good first step is to take some time to study what the main differences are between our plugins and see if there's any low-hanging fruit to bring them closer together.

[Julian]

All makes sense completely on maintenance burden :)

What kind of thing do you have in mind?

A lot of things are in-editor features, so yeah writing plugins in Python is way better than vimscript and probably got most of the way -- but things like neovim's extmarks (which let us add virtual text to the buffer which tracks through editing changes), being able to rely on built-in LSP, and floating windows (though I don't know how advanced vanilla vim's are at this point so it may have caught up) were all very useful.

I'm definitely interested in some sort of collaboration even if that just means sharing ideas for what kinds of features to provide, and how best to take advantage of Vim/NeoVim's features to display information to the user and help them interact with it.

Yes great! Glad we're in touch then at least -- I'll close this to not litter your issue tracker but your proposed step sounds like a decent idea to me. Will try to have a look through what's here myself, since I've not had the pleasure of using it yet.

[cormacrelf]

Just dropping this here, seems like a good enough spot instead of filing a new issue: I made a version of Coqtail with support for EasyCrypt. https://github.com/cormacrelf/Coqtail-EasyCrypt

It's a very hacky fork but it works. It turns out the EasyCrypt program is not all that difficult to write a client for, it's parseable line by line and emits a prompt after each operation. There are no complicated features to have difficulty with. If you wanted to support it in lean.nvim it would be similarly easy. It might be an easier way to explore making a proof-assistant-independent version of the plugin than starting with Coq. The same goes for the other way round.

[Julian]

@cormacrelf very cool, will have a look!

[whonore]

@cormacrelf That's cool that you were able to get something working so quickly. Do you plan to get it to a state where it could potentially be merged back into Coqtail or just leave it as a separate fork for now?

[cormacrelf]

I know right, literally a couple of hours! I've been at the ANU's excellent Logic Summer School, I asked the lecturer if you could use Vim for doing EasyCrypt, no, so I just dropped this in the chat the next day.

And yeah I see no reason why not. Maybe I'll make it a draft PR so it's a bit more visible and you can see the diff progress as I go.