---

Ⅰ. 插件描述

Interactive Coq Proofs in Vim

Ⅱ. 基本信息

创建日期：  2017-05-31 使用用户：  3 Github星：  48 插件作者：  Wolf Honore

Ⅲ. 安装方法

使用Vundle管理器安装

在你的.vimrc下添加:

Plugin 'whonore/coqtail'

… 然后在Vim中运行以下命令:

:source %
:PluginInstall

对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。

使用NeoBundle管理器安装

在你的.vimrc下添加:

NeoBundle 'whonore/coqtail'

… 然后在Vim中运行以下命令:

:source %
:NeoBundleInstall

使用VimPlug管理器安装

在你的.vimrc下添加:

Plug 'whonore/coqtail'

… 然后在Vim中运行以下命令:

:source %
:PlugInstall

使用Pathogen管理器安装

在终端中运行以下命令:

cd ~/.vim/bundle
git clone https://github.com/whonore/coqtail

Ⅳ. 文档说明

# 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.11
• Having multiple Coq buffers open
• Python 2¹ and 3

Installation and Requirements

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:

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

Using
Vundle:

Plugin 'whonore/Coqtail' | Plugin 'let-def/vimbufsync' (add this line in .vimrc)
vim +PluginInstall +qa

Using
VimPlug:

Plug 'whonore/Coqtail' | Plug 'let-def/vimbufsync' (add this line in .vimrc)
vim +PlugInstall +qa

Coqtail requires:

• Vim compiled with either +python¹ or +python3
• Vim configuration options filetype plugin indent on and syntax 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.

Usage

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. If your Vim supports 'tagfunc' you can just use CTRL-], :tag, and friends instead.
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 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 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.

Interoperability

Jumping between matches

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

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.