All Releases

Rocq 9.0.0

This page describes Rocq version 9.0, released on March 12th, 2025. Go here for a list of all releases.

This is the first release of Rocq, version 9. It marks the completion of the renaming from The Coq Proof Assistant to The Rocq Prover.

Github release

Reference Manual

Corelib Theories

OCaml API

Stdlib Manual

Stdlib Theories

Changes

See the full changelog in the reference manual.

Installation Instructions

The base proof assistant can be installed as an opam switch with the following commands:

opam update
opam switch create 4.14.1
opam install rocq-prover.9.0.0

Refer to the general install instructions for more information.

Source Distribution

  • Source tarball (.tar.gz) for compilation under Unix (including Linux and macOS X) and Microsoft Windows (including Cygwin).
  • Also available in .zip format.
  • Opam is a source-based distribution of OCaml, Rocq and many companion libraries and tools. Compilation and installation are automated by powerful package managers.
  • The official development repo is hosted on GitHub.