search

whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 35 forks source link

Coq v8.9 support #13

Closed tchajed closed 4 years ago

tchajed commented 5 years ago

I'd love to try using this plugin, and especially to recommend it to vim users, but we prefer to support only the latest release of Coq and Coq master, which is now Coq 8.9 and 8.10+alpha.

What is needed to support Coq 8.9 and above?

whonore commented 5 years ago

Probably very little as long as the XML interface hasn't changed much. I'll take a look at it soon.

whonore commented 5 years ago

It turns out there were only a couple minor changes that affected Coqtail so I pushed a version that should support 8.9 on this branch: https://github.com/whonore/Coqtail/tree/v8.9. I tested it a bit but I want to do a little more before I merge it back into master. In the meantime if you could also try it out and let me know if you find any problems that would be much appreciated. As for 8.10 alpha, that also looks like it should be pretty easy to support so I'll try that out soon too.

tchajed commented 5 years ago

I'm using neovim and I get an error: "Request from non-main thread. Requests from different threads should be wrapped with nvim.async_call(cb, ...)").

I'm not sure how you make plugins that are compatible with Vim8 and neovim, but if it's something simple neovim support would be great!

whonore commented 5 years ago

I'm not very experienced with neovim but it looks like the main thing preventing Coqtail from being compatible is how I'm handling certain asynchronous calls. I probably won't have time to make the necessary changes for a little while, but I was planning on reworking the asynchronous bits in the not-too-distant-future anyway because I'm not too happy with what I have now, so when I start making those changes I'll keep neovim in mind and see if I can support it then.

andreypopp commented 5 years ago

This patch against 8.9 makes it work with neovim — https://gist.github.com/a9c4e937ca86060e2b367b02b1e57d63

The issue is that neovim executes python plugins in a separate process and then some synchronisation is needed to make this work correctly. Also I think code could be simplified a but using python's new concurrent stdlib module. What's the stance on py2 compat with this plugin?

whonore commented 5 years ago

Thanks, I'm glad to see that the changes needed to support neovim are fairly small. My plan is to switch to using Vim8's channels and jobs at which time something like your solution might work for both vim and neovim.

As for py2 I originally wanted to continue supporting it until it's officially retired (https://pythonclock.org/) but it's becoming annoying enough to have both versions that I'm thinking of choosing an earlier time to tag some stable release and then drop support in future commits and point py2 users to the old version.

andreypopp commented 5 years ago

Heh, unfortunately these changes break keybaord interrupt handling :-).

Good to hear about the plans to use Vim's job API!