All Releases

Rocq 9.0+rc1

This page describes Rocq version 9.0+rc1, released on Jan 24, 2025. Go here for a list of all releases.

This is the first release candidate of Rocq 9. This is a pre-release, mainly useful to library develpers and package managers.

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 repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install rocq-prover.9.0+rc1

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.