dev-lang/coq

A proof assistant.

Versions

Slot Version Repository Platforms
0 scm ocaml-unofficial ~amd64 arm? armv7? armv8? x86?
8.5-scm ocaml-unofficial ~amd64 arm? armv7? armv8? x86?
8.5-p2 ocaml-unofficial ~amd64 arm? armv7? armv8? x86?

Metadata

Homepage http://coq.inria.fr/
Summary A proof assistant
Description 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.
Dependencies (
    build+run:
    !dev-lang/ocaml[=4.02.0]
    dev-ocaml/camlp5[>=6.02]
    dev-ocaml/findlib
    gtk? (
        dev-ocaml/lablgtk[gtksourceview(-)]
    )
    suggestion:
    app-editors/emacs
    x11-apps/xdg-utils
    build+run:
    dev-lang/ocaml[>=3.12.1]
)
Downloads https://coq.inria.fr/distrib/V8.5pl2/files/coq-8.5pl2.tar.gz
Licences LGPL-2.1

Choices

OPTIONS

gtk Build the CoqIDE tool