From Gentoo Wiki
Jump to:navigation Jump to:search

Coq is a formal proof management system, for formalizing and machine-checking proof written in Ocaml. Coq is based on the Calculus of Inductive Constructions.[1] From the official website

It (Coq, red.) provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.[2]


USE flags for sci-mathematics/coq Proof assistant written in O'Caml

debug Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see
doc Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally
gui Enable support for a graphical user interface
ocamlopt Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
test Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)


Coq can be installed from the official gentoo repositories.

root #emerge --ask sci-mathematics/coq

User interfaces

Coq supports multiple user interfaces, such as VSCode, Emacs, Vim/Neovim as well as its own CoqIDE.


Users of Visual Studio Code can use the VsCoq extention which is currently maintained by the coq-community.[3]


Users of Emacs can use the major Coq mode Proof General and extend that with the minor Coq mode Company-Coq.


Users of Vim/Neovim can use the Coqtail plugin.

Further reading

For a thorough introduction to logic in Coq see the free e-book Logical Foundation from the University of Pennsylvania.