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 http://coq.inria.fr/tools1-eng.html.
Interface for Editing Proofs
- The graphical user interface distributed with Coq.
ProofGeneral is a generic interface for proof assistants, based on the customizable text editor Emacs.
- Eclipse plugin for Coq development (based on Wenzel's asynchronous PIDE framework).
- Jedit (proof of concept) plugin for Coq development by Carst Tankink (also based on asynchronous PIDE framework).
GeoProof is a dynamic geometry software, with can communicate with CoqIDE to build the formula corresponding to a geometry figure interactively.
Papuq is patched version of CoqIde with teaching oriented features.
Coq plugin for TeXmacs
- An online web interface for Coq (and other proof assistants), with a focus on teaching.
- An experimental Eclipse plugin with support for Coq.
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 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).
coqdoc exports vernacular file to TeX or HTML. It is part of the Coq distribution and documented in the Reference Manual.
enscript mode for Coq http://www.cs.ru.nl/~milad/programs/enscript
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.