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.
USE flags for sci-mathematics/coq Proof assistant written in O'Caml
||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|
||Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally|
||Add support for x11-libs/gtk+ (The GIMP Toolkit)|
||Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)|
The lastest stable version in the gentoo repositories is 8.6.1-r1 as of writing (10. Feb. 2021), whilst the latest stable official release is 8.13.0. The latter is in testing.
Coq can be installed from the official gentoo repositories.
emerge --ask sci-mathematics/coq
Users of Visual Studio Code can use the VsCoq extention which is currently maintained by the coq-community.
Users of Vim/Neovim can use the Coqtail plugin.
For a thorough introduction to logic in Coq see the free e-book Logical Foundation from the University of Pennsylvania.