Rocq Packages

Explore hundreds of Rocq packages with their documentation

Install Rocq Packages

Learn how to install and search for Rocq packages using opam, including extensions, libraries, and tools

Publish a Rocq Package

Learn how to publish your first Rocq opam package today and make it available to the rest of the community

opam

Package Manager for OCaml and Rocq

The source-based package manager opam supports OCaml and Rocq packages. With opam installed, released Rocq packages can be accessed by adding the official Rocq opam repository:

592

Packages
4

New packages this month
20

Updates this week

packages

Most Used

rocq-stdlib

The Rocq Proof Assistant -- Standard Library

Used by 58 other packages

coq-mathcomp-algebra

Compatibility package for rocq-mathcomp-algebra

Used by 31 other packages

coq-mathcomp-ssreflect

Compatibility package for rocq-mathcomp-ssreflect

Used by 31 other packages

coq-flocq

A formalization of floating-point arithmetic for the Coq system

Used by 21 other packages

coq-ext-lib

A library of Coq definitions, theorems, and tactics

Used by 16 other packages

New Packages

rocq-infotheo

Discrete probabilities and information theory for Rocq

8 days ago

rocq-hollight

HOL-Light library in Rocq

10 days ago

rocq-coqprime

Certifying prime numbers in Rocq

2 weeks ago

rocq-vst

Verified Software Toolchain

5 weeks ago

Start Contributing