SlackBuilds Repository

14.2 > Academic > coq (8.9.0)

coq is a formal proof management system. It provides a formal language
to write mathematical definitions, executable algorithms and theorems
together with an environment for semi-interactive development of
machine-checked proofs.

To build CoqIDE, add COQIDE=yes, e.g.: COQIDE=yes ./coq.SlackBuild.
You will need the lablgtk package built with gtksourceview support.

This requires: ocaml-findlib, camlp5

Maintained by: Nick Smallbone
Keywords: coq,theorem prover,proof assistant,proof managment,ocaml
ChangeLog: coq