A Vim plugin for interactive Rocq (Coq) proof development, providing IDE-like features within the editor.
Coqtail is a Vim plugin that enables interactive proof development with the Rocq (formerly Coq) proof assistant. It allows developers to write, step through, and manage formal proofs directly within Vim, providing IDE-like features such as goal display, query execution, and syntax highlighting. The plugin bridges the gap between Vim's editing efficiency and Rocq's interactive proof environment.
Formal verification researchers, developers, and students who use Rocq for theorem proving and prefer Vim or Neovim as their primary editor. It is ideal for those who want a keyboard-driven, customizable workflow for proof development.
Coqtail offers a lightweight, integrated alternative to standalone Rocq IDEs by bringing full interactive proof development into Vim. Its non-blocking communication, support for multiple sessions, and extensive customization options make it a powerful tool for efficient proof engineering without leaving the editor.
Interactive Coq Proofs in Vim
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
Enables forward/backward navigation of proofs with keyboard mappings like <leader>cj and <leader>ck, allowing real-time feedback and rewind similar to RocqIDE.
Supports non-blocking interaction between Vim and Rocq for Vim ≥8.0 and Neovim, preventing editor freezes during proof checking as highlighted in the README.
Allows running simultaneous Rocq sessions in different Vim buffers, facilitating work on multiple proofs or projects concurrently.
Provides default mappings but fully customizable via Vim settings, such as disabling with g:coqtail_nomap or using hooks like CoqtailHookDefineMappings for personalized workflows.
Officially supports only Rocq 8.4 to 9.2, with newer versions untested and potential breaking changes in the XML protocol, as admitted in the README.
Requires Vim compiled with Python 3.6+, specific configuration like filetype settings, and may need manual steps for Rocq executable detection, especially for Rocq ≥8.9.
Lacks built-in features like Unicode input, relying on third-party Vim plugins such as latex-unicoder, which adds overhead for full functionality.
Coqtail is an open-source alternative to the following products:
ProofGeneral is an Emacs-based generic interface for proof assistants, supporting interactive theorem proving with systems like Coq, Isabelle, and others.
RocqIDE is an integrated development environment for the Coq proof assistant, providing tools for writing, verifying, and managing formal proofs.