Coqtail enables interactive Coq proof development in Vim similar to CoqIDE or ProofGeneral.
It supports:
- Coq 8.4 - 8.11
- Having multiple Coq buffers open
- Python 21 and 3
As a vim package:
mkdir -p ~/.vim/pack/coq/start
git clone https://github.com/let-def/vimbufsync.git ~/.vim/pack/coq/start/vimbufsync
git clone https://github.com/whonore/coqtail.git ~/.vim/pack/coq/start/coqtail
vim +helptags\ .vim/pack/coq/start/coqtail/doc +q
Using pathogen:
cd ~/.vim/bundle && git clone https://github.com/whonore/coqtail.git
Using Vundle:
Plugin 'whonore/coqtail' (in .vimrc)
:PluginInstall
Using VimPlug:
Plug 'whonore/coqtail' (in .vimrc)
:PlugInstall
Coqtail requires:
- Vim compiled with either
+python
1 or+python3
- Vim configuration options
filetype plugin indent on
andsyntax on
(e.g. in.vimrc
) - vimbufsync
- Coq 8.4 - 8.11
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
.
If you are using pathogen, documentation can be generated by
:call pathogen#helptags()
. Alternatively, you can do :helptags {path-to-coqtail}/doc
.
Coqtail provides the following commands (see :help coqtail
for more details):
Command | Mapping | Description |
---|---|---|
Starting and Stopping | ||
CoqStart |
<leader>cc |
Launch Coqtail for the current buffer. |
CoqStop |
<leader>cq |
Quit Coqtail for the current buffer. |
Movement | ||
{n}CoqNext |
<leader>cj |
Check the next n (1 by default) sentences with Coq. |
{n}CoqUndo |
<leader>ck |
Step back n (1 by default) sentences. |
{n}CoqToLine |
<leader>cl |
Check/rewind all sentences up to line n (cursor position by default). n can also be $ to check the entire buffer. |
CoqToTop |
<leader>cT |
Rewind to the beginning of the file. Similar to 1CoqToLine , but CoqToLine only rewinds to the end of the line. |
CoqJumpToEnd |
<leader>cG |
Move the cursor to the end of the checked region. |
CoqGotoDef[!] <arg> |
<leader>cg |
Populate the quickfix list with possible locations of the definition of <arg> and try to jump to the first one. |
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). |
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 SearchAbout <args> |
<leader>cs |
Show theorems about <args> . |
Goal Focusing | ||
{n}CoqGotoGoal |
<leader>cgg |
Scroll the goal panel to the start of the n th 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 n th 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 shown above are set by default, but you can disable them all and
define your own by setting g:coqtail_nomap = 1
in your .vimrc.
Alternatively, you can choose to only remap specific commands and the defaults
will still be used for the rest.
By default Coqtail will use the coqtop
or coqtop.opt
on your PATH
.
You can tell it to search instead in a specific directory by setting
b:coqtail_coq_path
before calling CoqStart
. To set this option globally use
g:coqtail_coq_path
.
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.
Parts of Coqtail were originally inspired by/adapted from Coquille (MIT License, Copyright (c) 2013, Thomas Refis).
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.