There is a famous Vim plugin for Coq integration - Coquille but it seems abandoned - no reaction to pull requests for years already. Note, it is also uses Python 2 which will be EOL in a few months. So the switch strongly encouraged. Would be awesome if maintainers quickly check the PRs, merge the worthy ones, and write to unmergeable ones what should be changed or closed. Note, I found a better updated plugin at framagit. Maybe it makes sense to synchronize them, or at least mark the GitHub repo as deprecated/abandoned?
It is worth noting that there is a well maintained Vim plugin as of today, it is called Coqtail, and it was partly inspired from / adapted from Coquille.
I am not a Vim user myself, but the feedback I got was good, so this is the Vim plugin I choose to advertise here: https://github.com/coq/coq/blob/master/CONTRIBUTING.md#contributing-to-the-editor-support-packages. We should probably also advertise all the amazing UI that are available today on the official website.
2 Likes
Having watched the Coquille repo for a couple of years now, I’m pretty confident that the project was abandoned by the developer a long time ago.
Having said that I decided a while back to jump into emacs+evil (or rather spacemacs) with Proof General and the transition is rather smooth. Nowadays I came to appreciate how the emacs environment allows me to have all my different coding environment / keybindings in one place.
I’m the author of Coqtail, which as @Zimmi48 mentioned (thanks for the plug) was originally a fork of Coquille. It supports Python 2 and 3 and Coq 8.4-8.9 (8.10 soon). I’m still actively working on it and would be happy to have more issue reports and pull requests.
3 Likes
Thanks, I will try it!