Rocq Changelog

We are happy to announce that Rocq 9.2.0 has been released. The main changes are:

• Reenable support for native_compute when compiled with OCaml 5. As it relies on some architecture-specific code, only some x86 setups are supported for now
• Records in Type and Prop, with only fields in SProp, can now have primitive projections but without eta conversion.
• Implicit elaboration of elimination constraints
• Parsing of elimination constraints in prenex polymorphic definitions as well as in constraints declaration Constraint s1 -> s2.
• Induction hypotheses are now generated for nested arguments provided an All predicate, and a theorem to prove it, have been registered with the keys All and AllForall.
• Add a Scheme All command to generate the All predicate and its theorem for inductive types used for the eliminators of nested inductive types
• Tactics such as induction find eliminators (like nat_rect) through the Register Scheme table (which is automatically populated by Scheme and automatic scheme declarations) instead of by name (the lookup by name remains for now for backward compatibility)
• attribute schemes to control automatic scheme declaration.
• Goal names can be automatically generated for induction, destruct and eapply by using the Generate Goal Names flag
• congruence tactics now handle primitive ints, floats and strings
• Ltac2 Custom Entry making it possible to define more complex Ltac2 Notations and many other additions to Ltac2 (see below for details).
• Printing Fully Qualified to print all names (global references, modules, module types, universes, etc) using fully qualified paths
• Generalized universe polymorphism flag structure (ML API change)

See the changelog Recent changes for more information.

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 rocq-core=9.2.0

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

• GitHub

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

• Fixed an anomaly when defining a sort polymorphic inductive without enabling Universe Polymorphism.
• Fixed compatibility with OCaml 5.4 with warnings as errors

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 rocq-core=9.1.1

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

• GitHub

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

• Fixed incorrect guard checking leading to inconsistencies
• Sort polymorphic universe instances should now be written as @{s ; u} instead of @{s | u}
• Fixed handling of notation variables for ltac2 in notations (i.e. Notation "'foo' x" := ltac2:(...))
• Support for refine attribute in Definition
• Rocq can be compile-time configured to be relocatable
• Extraction handles sort polymorphic definitions

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 rocq-core=9.1.0

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

• GitHub

We have the pleasure of announcing the first release of Rocq 9.0. 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