package rocq-devtools

  1. Overview
  2. No Docs
Development tools for Rocq

Install 

dune-project
 Dependency

rocq-prover.org Edit opam file Versions (2)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

Description

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).

Published: 23 Feb 2026

Dependencies (4)

  1. camlzip
  2. yojson >= "2.0"
  3. rocq-runtime = version
  4. dune >= "3.8"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None