coq-coreversion

The Coq Proof Assistant -- Core Binaries and Tools

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.

Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching.

This package includes the Coq core binaries, plugins, and tools, but not the vernacular standard library.

Note that in this setup, Coq needs to be started with the -boot and -noinit options, as will otherwise fail to find the regular Coq prelude, now living in the coq-stdlib package.

AuthorThe Coq development team, INRIA, CNRS, and contributors
LicenseLGPL-2.1-only
Published
Homepagehttps://coq.inria.fr/
Issue Trackerhttps://github.com/coq/coq/issues
MaintainerThe Coq development team <coqdev@inria.fr>
Dependencies
Optional dependencies
Conflicts
Source [http] https://github.com/coq/coq/releases/download/V8.18.0/coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/coq-core/coq-core.8.18.0/opam