Ⅰ. 插件描述
Interactive theorem proving with Coq in vim.Ⅱ. 基本信息
|
Ⅲ. 安装方法
使用Vundle管理器安装
在你的.vimrc下添加:Plugin 'the-lambda-church/coquille':source %
:PluginInstall对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。
使用NeoBundle管理器安装
在你的.vimrc下添加:NeoBundle 'the-lambda-church/coquille':source %
:NeoBundleInstall使用VimPlug管理器安装
在你的.vimrc下添加:Plug 'the-lambda-church/coquille':source %
:PlugInstall使用Pathogen管理器安装
在终端中运行以下命令:cd ~/.vim/bundle
git clone https://github.com/the-lambda-church/coquilleⅣ. 文档说明
Coquille
Coquille is a vim plugin aiming to bring the interactivity of CoqIDE into your
favorite editor.
Installation
This repository is meant to be used as a pathogen bundle. If you don't
already use pathogen, I strongly recommend that you start right now.
As everybody knows, vim is a wonderful editor which offers no way for a plugin
to track modifications on a buffer. For that reason Coquille depends on a set of
heuristicts collected in vimbufsync to detect modifications in the buffer.
You will need to make this plugin available in your runtime path (it can be
installed as a pathogen bundle as well) if you want Coquille to work.
Once that is done, installing Coquille is just as simple as doing :
cd ~/.vim/bundle
git clone https://github.com/trefis/coquille.git
Not that by default, you will be in the pathogen-bundle branch, which also
ships Vincent Aravantinos syntax and indent scripts for Coq, as well
as an ftdetect script.
If you already have those in your vim config, then just switch to the master
branch.
Getting started
To launch Coquille on your Coq file, run :CoqLaunch which will make the
commands :
- CoqNext
- CoqToCursor
- CoqUndo
- CoqKill
available to you.
By default Coquille forces no mapping for these commands, however two sets of
mapping are already defined and you can activate them by adding :
" Maps Coquille commands to CoqIDE default key bindings
au FileType coq call coquille#CoqideMapping()
or
" Maps Coquille commands to <F2> (Undo), <F3> (Next), <F4> (ToCursor)
au FileType coq call coquille#FNMapping()
to your .vimrc.
Alternatively you can, of course, define your owns.
Running query commands
You can run an arbitrary query command (that is Check, Print, etc.) by
calling :Coq MyCommand foo bar baz. and the result will be displayed in the
Infos panel.
Configuration
Note that the color of the "lock zone" is hard coded and might not be pretty in
your specific setup (depending on your terminal, colorscheme, etc).
To change it, you can overwrite the CheckedByCoq and SentToCoq highlight
groups (:h hi and :h highlight-groups) to colors that works better for you.
See coquille.vim for an example.
You can set the following variable to modify Coquille's behavior:
g:coquille_auto_move Set it to 'true' if you want Coquille to
(default = 'false') move your cursor to the end of the lock zone
after calls to CoqNext or CoqUndo
Screenshoots
Because pictures are always the best sellers :
