rocq-devtoolsversion Documentation on ocaml.org
Development tools for Rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. 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 tools to help when developing Rocq projects (timelog2html).
| Author | The Rocq development team, INRIA, CNRS, and contributors |
|---|---|
| License | LGPL-2.1-only |
| Homepage | https://rocq-prover.org/ |
| Issue Tracker | https://github.com/rocq-prover/rocq/issues |
| Documentation | https://rocq-prover.org/docs/ |
| Maintainer | The Rocq development team <rocq+rocq-development@discoursemail.com> |
| Dependencies |
|
| Source [http] | https://github.com/rocq-prover/rocq/releases/download/V9.3.0/rocq-9.3.0.tar.gz sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad |
No package is dependent
