sponsor Vim development Vim logo go to HTTPS page Vim Book Ad

CoqIDE : Emulate Coq IDE in VIM

 script karma  Rating 13/12, Downloaded by 1131    Comments, bugs, improvements  Vim wiki

created by
Matthieu Carlier
script type
You can use this script to make vim behaves like CoqIDE.

This script needs +perl vim option.

Should work well on non-gui version of vim on unix systems.

See comments at beginning of coq_IDE.vim for more informations.
install details
Copy the coq_IDE.vim file to "~/.vim/ftplugin/coq_IDE.vim" and add "filetype plugin on" in your "~/.vimrc".
Alternatively, you can ":source coq_IDE.vim" whenever you want.

"coqtop" should be accessible on PATH. If "coqtop" is not in
your PATH, add 'let CoqIDE_coqtop = "/path/to/coqtop"' in your "~/.vimrc".

This script comes with key bindings. These bindings are not loaded by default.
You can add "let g:CoqIDEDefaultKeyMap = 1" in your "~/.vimrc" to load its automatically.

<F2> undo last command
<F3> send next command
<F4> goto the command under the cursor
<F5> undo all commands
<F6> send all the buffer
<F7> refresh screen
<F8> kill coqtop

b : break computation (only when a command is being interpreted)

Rating scripts is only available on the HTTPS page

script versions (upload new version)

Click on the package to download.

package script version date Vim version user release notes
coq_IDE-0.97b.tgz 0.97b 2013-09-04 7.0 Matthieu Carlier Various improvements from Shu-Chun Weng:
- Customize coqtop options: read from CoqIDE_coqtop_option variable
- Check and show background goals when the foreground ones are all done.
- ProceedUntilCursor reads the character under the cursor, too, so you can park the cursor on the period and still get the last command in.
coq_IDE-0.96b.tgz 0.96b 2013-05-18 7.3 Matthieu Carlier Corrected script behavior when multiple files are edited.
Expressions containing  '..' are now correctly sent to coqtop.
coq_IDE-0.94b.tgz 0.94b 2013-04-13 7.3 Matthieu Carlier Aesthetical changes + robustness on sourcing
coq_IDE.tgz 7.3 2013-01-06 7.3 Matthieu Carlier Initial upload
ip used for rating:

If you have questions or remarks about this site, visit the vimonline development pages. Please use this site responsibly.
Questions about Vim should go to the maillist. Help Bram help Uganda.
SourceForge.net Logo