Coq
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/coqUser 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.