rocq: Interactive theorem prover¹

The Rocq Prover is an interactive theorem prover, or proof assistant. This means that it is designed to develop mathematical proofs, and especially to write formal specifications: programs and proofs that programs comply to their specifications.

An interesting additional feature of Rocq is that it can automatically extract executable programs from specifications, as either OCaml or Haskell source code.

... part of T2, get it here

URL: https://rocq-prover.org/

Author: INRIA
Maintainer: Tomas Glozar <tglozar [at] gmail [dot] com>

License: LGPL
Status: Stable
Version: 9.0.0

Download: https://github.com/rocq-prover/rocq/tags/download/V9.0.0/ rocq-9.0.0.tar.gz

T2 source: coqtop-version.patch
T2 source: rocq.cache
T2 source: rocq.desc

Build time (on reference hardware): 60% (relative to binutils)²

Installed size (on reference hardware): 400.14 MB, 4161 files

Dependencies (build time detected): bash binutils coreutils diffutils dune findutils gawk git grep gzip linux-header make ocaml ocaml-findlib sed tar zarith

Installed files (on reference hardware): n.a.

¹) This page was automatically generated from the T2 package source. Corrections, such as dead links, URL changes or typos need to be performed directly on that source.

²) Compatible with Linux From Scratch's "Standard Build Unit" (SBU).