Rocq Changelog

We have the pleasure of announcing the first release of Rocq 9. The main changes are:

• "The Rocq Prover" is the new official name of the project. We leave to users the choice of renaming their projects to reflect this change, see Renaming Advice. The Rocq Prover comes with a new visual identity and website, see The Rocq Prover Website.

• A single rocq binary dispatches commands for compilation, read-eval-print-loop, documentation building, dependency computation, etc. See The Rocq Prover commands. It corresponds to the rocq-runtime opam package. This is a bare-bones package that does not provide any Gallina code.

• The Coq standard library has been split into two libraries:

  • A Corelib library (the rocq-core opam package). This is an extended prelude, which is enough to run Rocq tactics and contains the Ltac2 library and bindings for primitive types (integers, floats, arrays and strings).

  • An Stdlib library (the rocq-stdlib opam package). The Stdlib is now maintained out of the main rocq repository. We welcome maintainers and contributors to the new repository. A specific call for contributions will be sent soon.

The full list of changes is available here for more details.

Installation Instructions

The base compiler 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

The source code for the release is also directly available on:

• GitHub

We have the pleasure of announcing the release of Coq 8.20.1.

The full list of changes is available here for more details.

Installation Instructions

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

opam update
opam switch create 4.14.1
opam install coq.8.20.1

The source code for the release is also directly available on:

• GitHub

The Rocq Team is pleased to announce the preview release of the new website of the Rocq Prover and Platform, along with its new logo and visual identity.

This website is based on a fork of the www.ocaml.org website. The Rocq developers are extremely grateful to the OCaml.org developers for making their sophisticated website open-source 🙏🏼.

The new identity was designed by Bastien Sozeau, founder of the Noir Blanc Rouge type foundry.

We have the pleasure of announcing the release of Coq 8.20.0.

The full list of changes is available here for more details.

Installation Instructions

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

opam update
opam switch create 4.14.1
opam install coq.8.20.0

The source code for the release is also directly available on:

• GitHub