Tools

Some of the tools listed here are part of bigger projects that support other proof assistants/theorem provers. Another list of Coq-related tools can be found at https://coq.inria.fr/related-tools.

Interface for Editing Proofs

• CoqIDE

  The graphical user interface distributed with Coq.

• ProofGeneral

  ProofGeneral is a generic interface for proof assistants, based on the customizable text editor Emacs.

• Coqoon

  Eclipse plugin for Coq development (based on Wenzel's asynchronous PIDE framework).

• ProofWeb

  An online web interface for Coq (and other proof assistants), with a focus on teaching.

• vscoq

  A Visual Studio based interface developed in 2016.

• jscoq

  A port of Coq to the browser; runs standalone using js_of_ocaml.

• CoqTail

  CoqTail is a vim plugin aiming to bring the interactivity of CoqIDE into your favorite editor.

Language Servers

• coq-lsp

  coq-lsp is a Language Server and Visual Studio Code extension for Coq. Experimental support for Vim and Neovim is also available in their own projects. Key features of coq-lsp are continuous and incremental document checking, advanced error recovery, markdown support, positional goals and information panel, performance data, and more.

• coq-serapi

  A language-server based in the STM protocol with full serialization capabilities [proofs, documents, terms].

Discontinued interfaces

• Coq PIDE

  Jedit (proof of concept) plugin for Coq development by Carst Tankink (also based on asynchronous PIDE framework).

• ProverEditor

  An experimental Eclipse plugin with support for Coq.

• tmEgg

  Coq plugin for TeXmacs

• Papuq

  Papuq is patched version of CoqIde with teaching oriented features.

• GeoProof

  GeoProof was a dynamic geometry software, which can communicate with CoqIDE to build the formula corresponding to a geometry figure interactively.

• PCoq (for versions of Coq in old syntax, version 7.4 of 2003 and before)

  A graphical user interface for Coq. The environment provides ways to edit structurally formulas and commands, new notations can easily be added. It allows proof by pointing.

• TmCoq

  TmCoq integrates Coq within TeXmacs.

Interface for Browsing Proofs

• Helm is a browsable and searchable (using the Whelp tool) repository of formal mathematics (includes the Coq User Contributions).

Presenting Proofs

• coqdoc exports vernacular file to TeX or HTML. It is part of the Coq distribution and documented in the Reference Manual.

Tactics packages

• Micromega: solves linear (Fourier-Motzkin) and non linear (Sum-of-Square's algorithm) systems of polynomial inequations; also provides a (partial) replacement for the Coq's omega tactic.
• Ssreflect facilitates proof by small scale reflection, "a style of proof that ... provide[s] effective automation for many small, clerical proof steps. This is often accomplished by restating ("reflecting") problems in a more concrete form ... For example, in the Ssreflect library arithmetic comparison is not an abstract predicate, but a function computing a boolean. (source)"
• AAC Tactics provides tactics that facilitates the rewriting of universal equations,modulo associative and possibly commutative operators, and modulo neutral elements (units).

Packaging extracted code

• Z_interface An approach for deriving directly standalone programs from extracted code.

Automation

• CoqHammer/sauto
• Tactician
• Proverbot 9001
• Trakt
• Proofster
• SMTCoq
• Sniper
• MirrorSolve
• Hierarchy Builder
• Elpi
• Equations
• itauto
• MirrorCore/RTac

The following automation projects are academic research projects which may or may not be maintained.

• ASTactic/CoqGym (paper)
• TacTok ( paper )
• PassPort ( paper )

Utilities

• coqwc is a stand-alone command line tool to print line statistics about Coq files (how many lines are spec, proof, comments). coqwc comes with the standard Coq distribution.

• coq-tools is a collection of scripts for manipulating Coq developments:

  • find-bug.py is a "bug minimizer" that automatically minimizes a .v file producing an error, allowing automatic creation of small stand-alone test cases for Coq bugs;

  • absolutize-imports.py processes .v files, replacing things like Require Import Program. with Require Import Coq.Program.Program., making Requires robust against shadowing of file names;

  • inline-imports.py inlines the Required dependencies of a .v file, allowing the automatic creation of stand-alone files from developments;

  • minimize-requires.py removes unused Require and Require Import statements, and, optionally, unused Require Export statements;

  • move-requires.py splits all Require Import and Require Export statements into separate Require and Import/Export statements, and moves all Require statements to the top of a .v file;

  • move-vernaculars.py lifts many vernacular commands and inner lemmas out of Proof. ... Qed. blocks;

  • proof-using-helper.py processes the output of running coqc on a file with Suggest Proof Using set, to modify the file with the given Proof using suggestions;