Using Coqtail to setup the Coq interactive theorem prover in Vim or Neovim

Besides using Coq in the Coqide or with Proof General in Emacs, you can also set it up on Vim/Neovim with the Coqtail extension. I had some difficulties while setting it up and there weren’t that many resources for it, so I’m documenting the steps here.

We’ll have to:

  1. Set up Vim / Neovim with Python support
  2. Install coq for command line
  3. Add the coqtail plugin / setup colors or colorscheme

1. Setting up Vim / Neovim with Python

On Vim

If you use Vim, you will have to compile it yourself with the --enable-python3interp flag. I haven’t tried this myself because I use Neovim, but this seems to be the way. I found out about the flag from this stackoverflow answer.

On Neovim

On Neovim, it is much easier. You must have the pynvim package installed on your system’s Python3.

$ python3 -m pip install pynvim

Once done, check that the Python interpreter setup in your Neovim is same as the one for which you installed pynvim. You can check that in Neovim by running :checkhealth provider. Make sure that the python3_host_prog mentioned in the logs is the same as the interpreter where you installed pynvim ( $ which python3). If not you can set let g:python3_host_prog = "/path/to/python3" in your init.vim or init.lua.

2. Install coq for the command line

If you install directly from the website, you’ll get CoqIDE and an interactive command line program. But you need the coqc command to be there in $PATH for coqtail to use. You can set that up by installing Coq with a package manager.

For me it was brew.

$ brew install coq

And then check that coqc works.

$ coqc --version

3. Install whonore/coqtail plugin

I use vim-plug with an init.vim, so for me it was adding this line to init.vim:

Plug 'whonore/Coqtail'

and running nvim +PlugInstall.

You can find instructions for other plugin managers in coqtail repository’s README.

coqtail should now be setup. Open any Coq file (.v extension), try entering <leader> cc. This should start Coqtail in a split view. These are some shortcuts that I found useful:

Shortcut Description
<leader>cc Start coq
<leader>cj Go ahead by one step
<leader>ck Go back by one step
<leader>cl Run all steps until the current line

One more thing: if you use dark mode, Coqtail’s highlighting color probably won’t match well with the background. I simply switched to light mode when using Coq (relax, only for Coq). But, if you want to put in some more effort, you can set that up and it is mentioned in the repository’s readme here.