Coqtail

Interactive Coq Proofs in Vim

Coqtail enables interactive Coq proof development in Vim similar to CoqIDE or ProofGeneral.

It supports:

• Coq 8.4 - 8.13
• Python 2¹ and 3
• Vim >=7.4 and Neovim >=0.3
• Simultaneous Coq sessions in different buffers
• Non-blocking communication between Vim and Coq (Vim >=8.0 and NeoVim only)

Installation and Requirements

As a vim package:

mkdir -p ~/.vim/pack/coq/start
git clone https://github.com/whonore/Coqtail.git ~/.vim/pack/coq/start/Coqtail
vim +helptags\ ~/.vim/pack/coq/start/Coqtail/doc +q

Using pathogen:

git clone https://github.com/whonore/Coqtail.git ~/.vim/bundle/Coqtail
vim +Helptags +q

Using Vundle:

Plugin 'whonore/Coqtail' (add this line in .vimrc)
vim +PluginInstall +qa

Using VimPlug:

Plug 'whonore/Coqtail' (add this line in .vimrc)
vim +PlugInstall +qa

Requirements:

• Vim compiled with either +python¹ or +python3
• Vim configuration options filetype plugin on, and optionally filetype indent on and syntax on (e.g. in .vimrc)
• Coq 8.4 - 8.13

Newer versions of Coq have not yet been tested, but should still work as long as there are no major changes made to the XML protocol Coqtail uses to communicate with coqtop.

Usage

Coqtail provides the following commands (see :help coqtail for more details):

Configuration

Mappings

The mappings above are set by default, but you can disable them all and define your own by setting g:coqtail_nomap = 1 in your .vimrc. Some of the commands, such as CoqNext, also have insert-mode mappings by default, which can be disabled with g:coqtail_noimap. Alternatively, you can keep the defaults but remap specific commands. For example, use map <leader>ci <Plug>CoqInterrupt to avoid hijacking CTRL-C. The <leader>c prefix may be inconvenient depending on your mapleader setting. In that case you can set a custom prefix with g:coqtail_map_prefix (or g:coqtail_imap_prefix for just insert-mode mappings).

Coq Executable

By default Coqtail uses the first coq(ide)top(.opt) found in your PATH. Use b:coqtail_coq_path (or g:coqtail_coq_path) to specify a different directory to search in. You can also override the name of the Coq executable to use with b:coqtail_coq_prog (or g:coqtail_coq_prog). For example, to use the HoTT library:

let b:coqtail_coq_path = '/path/to/HoTT'
let b:coqtail_coq_prog = 'hoqidetop'

_CoqProject

Coqtail understands and will search for _CoqProject files on :CoqStart. Additional or different project files can be specified with g:coqtail_project_files. For example, to include arguments from both _CoqProject and _CoqProject.local:

let g:coqtail_project_files = ['_CoqProject', '_CoqProject.local']

Syntax Highlighting and Indentation

Coqtail also comes with an ftdetect script for Coq, as well as modified versions of Vincent Aravantinos' syntax and indent scripts for Coq. These scripts are used by default but can be disabled by setting g:coqtail_nosyntax = 1 and g:coqtail_noindent = 1 respectively. Formatting of comments can be disabled with g:coqtail_noindent_comment.

In addition to the Coq syntax, Coqtail defines highlighting groups for the sentences that are currently or have already been checked by Coq (CoqtailSent and CoqtailChecked) as well as any lines that raised an error (CoqtailError). By default these are defined as:

if &t_Co > 16
  hi def CoqtailChecked ctermbg=17 guibg=LightGreen
  hi def CoqtailSent    ctermbg=60 guibg=LimeGreen
else
  hi def CoqtailChecked ctermbg=4 guibg=LightGreen
  hi def CoqtailSent    ctermbg=7 guibg=LimeGreen
endif
hi def link CoqtailError Error

To override these defaults simply set your own highlighting (:help :hi) before syntax/coq.vim is sourced (e.g., in your .vimrc). Note, however, that many colorschemes call syntax clear, which clears user-defined highlighting, so it is recommended to place your settings in a ColorScheme autocommand. For example:

augroup CoqtailHighlights
  autocmd!
  autocmd ColorScheme *
    \  hi def CoqtailChecked ctermbg=236
    \| hi def CoqtailSent    ctermbg=237
augroup END

Proof Diffs

Since 8.9, Coq can generate proof diffs to highlight the differences in the proof context between successive steps. To enable proof diffs manually, use :Coq Set Diffs "on" or :Coq Set Diffs "removed". To automatically enable proof diffs on every :CoqStart, set g:coqtail_auto_set_proof_diffs = 'on' (or = 'removed'). By default, Coqtail highlights these diffs as follows:

hi def link CoqtailDiffAdded DiffText
hi def link CoqtailDiffAddedBg DiffChange
hi def link CoqtailDiffRemoved DiffDelete
hi def link CoqtailDiffRemovedBg DiffDelete

See the above instructions on how to override these defaults.

More Options

See :help coqtail-configuration for a description of all the configuration options.

Vim Plugin Interoperability

Jumping between matches

Coqtail defines b:match_words patterns to support jumping between matched text with % using the matchup or matchit plugins.

Automatically closing blocks

Coqtail defines patterns to enable automatic insertion of the appropriate End command for code blocks such as Sections, Modules, and match expressions with endwise.

Thanks

Parts of Coqtail were originally inspired by/adapted from Coquille (MIT License, Copyright (c) 2013, Thomas Refis).

Python 2 Support

Because Python 2 has reached its end-of-life and supporting it alongside Python 3 makes it difficult to improve and maintain the code, Coqtail will drop support for Python 2 in the near future. At that time a stable version will be tagged and all future versions will be Python 3-only. See YouCompleteMe for help building Vim with Python 3 support.