Coq

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]

Installation

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

+ocamlopt Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
debug Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces
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
test Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)

Emerge

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.

VSCode

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

Emacs

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

Vim/Neovim

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.