Coqtail enables interactive Coq proof development in Vim similar to CoqIDE or ProofGeneral.
It supports:
- Coq 8.4 - 8.19
- Python >=3.6 (see here for older versions)
- 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)
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 +qUsing pathogen:
git clone https://github.com/whonore/Coqtail.git ~/.vim/bundle/Coqtail
vim +Helptags +qUsing Vundle:
Plugin 'whonore/Coqtail' (add this line in .vimrc)
vim +PluginInstall +qaUsing VimPlug:
Plug 'whonore/Coqtail' (add this line in .vimrc)
vim +PlugInstall +qaRequirements:
- Vim/Neovim compiled with
+python3(3.6 or later) - Vim configuration options
filetype plugin on, and optionallyfiletype indent onandsyntax on(e.g. in.vimrc) - Coq 8.4 - 8.19
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.
Note that for Coq >=8.9, the coqidetop executable must be available, which may
require additionally installing CoqIDE depending on the installation method.
See here for help with pointing Coqtail to the appropriate location.
Coqtail provides the following commands (see :help coqtail for more details):
| Command | Mapping | Description |
|---|---|---|
| Starting and Stopping | ||
CoqStart |
<leader>cc |
Launch Coqtail in the current buffer. |
CoqStop |
<leader>cq |
Quit Coqtail in the current buffer. |
CoqInterrupt |
CTRL-C |
Send SIGINT to Coq. |
| Movement | ||
{n}CoqNext |
<leader>cj |
Send the next n (1 by default) sentences to Coq. |
{n}CoqUndo |
<leader>ck |
Step back n (1 by default) sentences. |
{n}CoqToLine |
<leader>cl |
Send/rewind all sentences up to line n (cursor position by default). n can also be $ to check the entire buffer. |
{n}CoqOmitToLine |
No default (see Mappings) | Same as CoqToLine, but skip processing of and admit all opaque proofs. Similar to Proof General's proof-omit-proofs-option. See :help CoqOmitToLine for more information. |
CoqToTop |
<leader>cT |
Rewind to the beginning of the file. |
CoqJumpToEnd |
<leader>cG |
Move the cursor to the end of the checked region. |
CoqJumpToError |
<leader>cE |
Move the cursor to the start of the error region. |
CoqGotoDef[!] <arg> |
<leader>cgd |
Populate the quickfix list with possible locations of the definition of <arg> and try to jump to the first one. If your Vim supports 'tagfunc' you can also use CTRL-], :tag, and friends. |
| Queries | ||
Coq <args> |
Send arbitrary queries to Coq (e.g. Check, About, Print, etc.). |
|
Coq Check <arg> |
<leader>ch |
Show the type of <arg> (the mapping will use the term under the cursor or the highlighted range in visual mode). |
Coq About <arg> |
<leader>ca |
Show information about <arg>. |
Coq Print <arg> |
<leader>cp |
Show the definition of <arg>. |
Coq Locate <arg> |
<leader>cf |
Show where <arg> is defined. |
Coq Search <args> |
<leader>cs |
Show theorems about <args>. |
| Panel Management | ||
CoqRestorePanels |
<leader>cr |
Re-open the Goal and Info panels. |
{n}CoqGotoGoal |
<leader>cgg |
Scroll the Goal panel to the start of the nth goal (defaults to 1). Number of lines shown is controlled by g:coqtail_goal_lines. |
{n}CoqGotoGoal! |
<leader>cgG |
Scroll the Goal panel to the end of the nth goal. |
CoqGotoGoalNext |
]g |
Scroll the Goal panel to the start of the next goal. |
CoqGotoGoalNext! |
]G |
Scroll the Goal panel to the end of the next goal. |
CoqGotoGoalPrev |
[g |
Scroll the Goal panel to the start of the previous goal. |
CoqGotoGoalPrev! |
[G |
Scroll the Goal panel to the end of the previous goal. |
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.
If a mapping for a command already exists when Coqtail is loaded, the default
mapping for that command won't be defined.
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).
Finally, after defining the standard keybindings, Coqtail will call a vim
function named CoqtailHookDefineMappings (if one is defined). This makes it
easy to add additional mappings without removing the standard mappings, and
to add mappings which are only active in Coqtail-managed buffers. One way to
use this hook is to make bindings for commands which augment the standard
Coqtail bindings instead of replacing them. One concrete example is:
function CoqtailHookDefineMappings()
imap <buffer> <S-Down> <Plug>CoqNext
imap <buffer> <S-Left> <Plug>CoqToLine
imap <buffer> <S-Up> <Plug>CoqUndo
nmap <buffer> <S-Down> <Plug>CoqNext
nmap <buffer> <S-Left> <Plug>CoqToLine
nmap <buffer> <S-Up> <Plug>CoqUndo
endfunctionAdding that snippet to your .vimrc would create new bindings for CoqNext,
CoqToLine, and CoqUndo. Those bindings would be active in all Coq buffers,
including Coqtail panels, but inactive in other buffers. The standard Coqtail
bindings (<leader>cj, etc) would remain active.
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 (these are automatically set if the $COQBIN environment
variable is set).
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'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']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), any lines that raised an error (CoqtailError), and the
beginnings and ends of omitted proofs (CoqtailOmitted).
By default these are defined as:
if &t_Co > 16
if &background ==# 'dark'
hi def CoqtailChecked ctermbg=17 guibg=#113311
hi def CoqtailSent ctermbg=60 guibg=#007630
else
hi def CoqtailChecked ctermbg=17 guibg=LightGreen
hi def CoqtailSent ctermbg=60 guibg=LimeGreen
endif
else
hi def CoqtailChecked ctermbg=4 guibg=LightGreen
hi def CoqtailSent ctermbg=7 guibg=LimeGreen
endif
hi def link CoqtailError Error
hi def link CoqtailOmitted coqProofAdmitTo 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 CoqtailHighlight
autocmd!
autocmd ColorScheme *
\ hi def CoqtailChecked ctermbg=236
\| hi def CoqtailSent ctermbg=237
augroup ENDIf you feel distracted by the error highlighting while editing a failed
sentence, you can use the sequence <leader>cl (:CoqToLine) while the cursor
is inside that sentence. If it isn't, you can use <leader>cE
(:CoqJumpToError) to move it to an appropriate position.
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 DiffDeleteSee the above instructions on how to override these defaults.
See :help coqtail-configuration for a description of all the configuration options.
Coqtail defines b:match_words patterns to support jumping between matched text
with % using the matchup or matchit plugins.
Coqtail defines patterns to enable automatic insertion of the appropriate End
command for code blocks such as Sections, Modules, and match expressions
with endwise.
Coqtail supports the :tag family of commands by locating a term on the fly
with tagfunc.
However, as this relies on Coq's Locate command, it only works if the point
where the term is defined has already been evaluated by Coq.
An alternative is to disable Coqtail's default tagfunc (let g:coqtail_tagfunc = 0) and instead use universal-ctags in conjunction with coq.ctags, to
statically generate a tags file.
This works especially well with something like the gutentags plugin to
automatically keep the tags file in sync with the Coq source.
Coqtail and Coq can handle non-ASCII characters in identifiers, notations, etc.,
but Coqtail does not provide a method for inputting these characters itself.
Instead one can use one of the native Vim options (e.g.,
i_CTRL-K or
i_CTRL-V_digit) or a
plugin like latex-unicoder or unicode.vim.
Parts of Coqtail were originally inspired by/adapted from Coquille (MIT License, Copyright (c) 2013, Thomas Refis).
Python 2 and 3.5 have reached their end-of-life so Coqtail no longer supports them in order to simplify the code and take advantage of newer features. See YouCompleteMe for help building Vim with Python 3 support. If you cannot upgrade Vim, the python2 branch still supports older Pythons.