The Coq mailing list

[Anders Lundstedt <a AT anderslundstedt.se>]

On Thu, Jan 24, 2019 at 11:11 AM Théo Zimmermann 
<theo.zimmi AT gmail.com>
 wrote:
>
> I just discovered https://framagit.org/manu/coq-au-vim which apparently 
> supports talking with Coq using the asychronous XML protocol (like CoqIDE 
> and the corresponding Proof General branch).
> Are some vim people using it? Is it good?
>
> Of course, there is also the older coquille which also provides vim 
> support, in the style of Proof General. I don't know if it kept working 
> with recent Coq version though: the last commit is quite old.

I have not been using Coq much the last couple of years, but when I
did I was using Vim exclusively. So for what it is worth, here are
some additional advice.


There is Coqtail which seems to be well maintained and which was what
I used last:

https://github.com/whonore/Coqtail


As for Coquille some of the forks might be more up to date, check:

https://github.com/the-lambda-church/coquille/network


What I did some years ago when looking for a Coq plugin for Vim was to
search "coq vim" on Github. When none of the results seemed to work
out of the box I managed to find something by looking through their
forks. So that might be an option of last resort.



Best,

Anders