Rocq Platform

The Rocq Platform Guiding Principles Rocq Prover and Rocq Platform release cycle

The Rocq Platform

The Rocq Platform is a distribution of the Rocq Prover together with a selection of libraries and plugins. The main goal of the Rocq Platform is to provide a distribution for developing and teaching with Rocq that is:

operating-system independent
dependable
easy to install
comprehensive

See the Guiding Principles for more on the Platform concept, and Rocq Prover and Rocq Platform release cycle for more on how the Platform is related to the Rocq Prover release cycle.

The Rocq Platform is based on the OCaml package manager opam and provides a set of scripts to compile and/or install opam, Rocq and the Platform contents on macOS, Windows and many Linux distributions in a reliable way with consistent results. In addition pre-compiled binary packages or installers are provided for macOS and Windows.

The Rocq Platform combines the core Rocq Prover with a coherent set of packages (plugins and libraries) to extend its features.

Detailed instructions to install Rocq and the Platform are available in Installing Rocq.

Packages of the Rocq Platform

Here is a list of all Platform packages sorted by their status.

Packages with a status of "full level" are considered stable, well-maintained and suitable as basis for your own developments. The full level adds many commonly used Rocq libraries, plugins and developments.

The "optional" packages have the same maturity and maintenance level as the packages in the full level, but either take a rather long time to build or have a non-open-source license or depend on packages with non-open-source license. The interactive installation script and the Windows installer explicitly ask if you want to install these packages.

The "extended level" contains packages which are in a beta stage or otherwise don't yet have the level of maturity or support required for inclusion in the full level, but there are plans to move them to the full level in a future release of the Rocq Platform. The main point of the extended level is advertisement: users are important to bring a development from a beta to a release state.

Full Level

The full level adds many commonly used Rocq libraries, plugins and developments.

z3_tptp.4.13.0

TPTP front end for Z3 solver

sexplib.v0.16.0

Library for serializing OCaml values to and from S-expressions

ott.0.33

A tool for writing definitions of programming languages and calculi

menhir.20231231

An LR(1) parser generator

gappa.1.4.1

Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic

eprover.3.1

E Theorem Prover

coq-unicoq.1.6+8.19

An enhanced unification algorithm for Coq

coq-stdpp.1.10.0

An extended \Standard Library\ for Coq

coq-simple-io.1.9.0

IO monad for Coq

coq-relation-algebra.1.7.10

Relation Algebra and KAT in Coq

coq-reglang.1.2.1

Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp

coq-quickchick.2.0.3

Randomized Property-Based Testing for Coq

coq-paramcoq.1.1.3+coq8.19

Plugin for generating parametricity statements to perform refinement proofs

coq-ott.0.33

Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi

coq-mtac2.1.4+8.19

Typed tactic language for Coq

coq-menhirlib.20231231

A support library for verified Coq parsers produced by Menhir

coq-mathcomp-zify.1.5.0+2.0+8.16

Micromega tactics for Mathematical Components

coq-mathcomp-word.3.1

Yet Another Coq Library on Machine Words

coq-mathcomp-ssreflect.2.2.0

Small Scale Reflection

coq-mathcomp-solvable.2.2.0

Mathematical Components Library on finite groups (II)

coq-mathcomp-real-closed.2.0.0

Mathematical Components Library on real closed fields

coq-mathcomp-multinomials.2.2.0

A Multivariate polynomial Library for the Mathematical Components Library

coq-mathcomp-finmap.2.1.0

Finite sets, finite maps, finitely supported functions

coq-mathcomp-fingroup.2.2.0

Mathematical Components Library on finite groups

coq-mathcomp-field.2.2.0

Mathematical Components Library on Fields

coq-mathcomp-character.2.2.0

Mathematical Components Library on character theory

coq-mathcomp-bigenough.1.0.1

A small library to do epsilon - N reasoning

coq-mathcomp-analysis.1.1.0

An analysis library for mathematical components

coq-mathcomp-algebra.2.2.0

Mathematical Components Library on Algebra

coq-mathcomp-algebra-tactics.1.2.3

Ring, field, lra, nra, and psatz tactics for Mathematical Components

coq-math-classes.8.19.0

A library of abstract interfaces for mathematical structures in Coq

coq-libhyps.2.0.8

Hypotheses manipulation library

coq-itauto.8.19.0

Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq

coq-iris.4.2.0

A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs

coq-iris-heap-lang.4.2.0

The canonical example language for Iris

coq-interval.4.10.0

A Coq tactic for proving bounds on real-valued expressions automatically

coq-hott.8.19

The Homotopy Type Theory library

coq-hierarchy-builder.1.7.0

High level commands to declare and evolve a hierarchy based on packed classes

coq-hammer.1.3.2+8.19

General-purpose automated reasoning hammer tool for Coq

coq-hammer-tactics.1.3.2+8.19

Reconstruction tactics for the hammer for Coq

coq-gappa.1.5.5

A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover

coq-flocq.4.1.4

A formalization of floating-point arithmetic for the Coq system

coq-ext-lib.0.12.1

A library of Coq definitions, theorems, and tactics

coq-equations.1.3+8.19

A function definition package for Coq

coq-elpi.2.1.0

Elpi extension language for Coq

coq-dpdgraph.1.0+8.19

Compute dependencies between Coq objects (definitions, theorems) and produce graphs

coq-corn.8.19.0

The Coq Constructive Repository at Nijmegen

coq-coquelicot.3.4.1

A Coq formalization of real analysis compatible with the standard library

coq-coqprime.1.5.0

Certifying prime numbers in Coq

coq-coqprime-generator.1.1.1

Certificate generator for prime numbers in Coq

coq-coqeal.2.0.2

CoqEAL - The Coq Effective Algebra Library

coq-bignums.9.0.0+coq8.19

Bignums, the Coq library of arbitrarily large numbers

coq-aac-tactics.8.19.0

Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators

Optional

The optional packages have the same maturity and maintenance level as the packages in the full level, but either take a rather long time to build or have a non-open-source license or depend on packages with non-open-source license.

coq-vst.2.14

Verified Software Toolchain

coq-unimath.20240331

Library of Univalent Mathematics

coq-compcert.3.13.1

The CompCert C compiler (64 bit)

Extended Level

The extended level contains packages which are in a beta stage or otherwise don't yet have the level of maturity or support required for inclusion in the full level, but there are plans to move them to the full level in a future release of the Rocq Platform.

coq-serapi.8.19.0+0.19.2

Serialization library and protocol for machine interaction with the Coq proof assistant

coq-rupicola.0.0.10

Gallina to imperative code compilation, currently in design phase

coq-riscv.0.0.5

RISC-V Specification in Coq, somewhat experimental

coq-rewriter.0.0.11

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography

coq-reduction-effects.0.1.5

A Coq plugin to add reduction side effects to some Coq reduction strategies

coq-record-update.0.3.4

Generic support for updating record fields in Coq

coq-metacoq.1.3.1+8.19

A meta-programming framework for Coq

coq-fiat-crypto.0.1.3

Cryptographic Primitive Code Generation by Fiat

coq-extructures.0.4.0

Finite sets, maps, and other data structures with extensional reasoning

coq-deriving.0.2.0

Generic instances of MathComp classes

coq-coqutil.0.0.6

Coq library for tactics, basic definitions, sets, maps

coq-bedrock2.0.0.8

A work-in-progress language and compiler for verified low-level programming

coq-bedrock2-compiler.0.0.8

A work-in-progress language and compiler for verified low-level programming (compiler part)

Dependency

In addition the dependencies listed below are partially or fully included or required during build time. Please note, that the version numbers given are the versions of opam packages, which do not always match with the version of the supplied packages. E.g. some opam packages just refer to latest packages e.g. installed by MacPorts, Homebrew or Linux system package managers.

zarith.1.14

Implements arithmetic and logical operations over arbitrary-precision integers

z3.4.13.0-3

Z3 solver

yojson.2.2.2

Yojson is an optimized parsing and printing library for the JSON format

stdlib-shims.0.3.0

Backport some of the new stdlib features to older compiler

sexplib0.v0.16.0

Library containing the definition of S-expressions and some base converters

seq.base

Compatibility package for OCaml'apos;s standard iterator type starting from 4.07.