Home
The Rocq prover, formerly known as Coq, is a proof assistant based on the calculus of constructions. It is used to formalize proofs in a variety of fields, including mathematics and programming languages.
You need to install Rocq and an appropriate IDE. Currently supported IDE's are RocqIDE (recommended for beginners), Proof General (major mode for Emacs users), Visual Studio with the VSRocq extension, and Coqtail for Vim.
For most users, it is easiest to install the Rocq platform which comes with a broad selection of stable packages tested for interoperability.
- Installation of the Rocq system:
- Configuration of RocqIDE
- Configuration of Proof General (to be completed)
- Configuration of coq-lsp for VScode
- Reference Manual
- Documentation of the Standard Library
- Discourse Forum (see also Discourse wiki page)
- Zulip Chat
- Coq-Club mailing list
- Bug tracker
- FAQ
- Twitter account
- IRC channel:
irc://irc.libera.chat/#rocq - Sub-reddit
- Stack Overflow tag
-
Software Foundations
- Volume 1: Logical Foundations (by Benjamin C. Pierce et al.)
- Volume 2: Programming Language Foundations (by Benjamin C. Pierce et al.)
- Volume 3: Verified Functional Algorithms (by Andrew W. Appel)
- Volume 4: QuickChick (by Leonidas Lampropoulos and Benjamin C. Pierce)
- Certified Programming with Dependent Types, by Adam Chlipala
- Coq'Art, by Yves Bertot and Pierre Castéran
- Mathematical Components book, by Assia Mahboubi and Enrico Tassi
- Formal Reasoning About Programs, by Adam Chlipala
- Programs and Proofs, by Ilya Sergey
- Computer Arithmetic and Formal Proofs, by Sylvie Boldo and Guillaume Melquiond
- Program Logics for Certified Compilers, by Andrew W. Appel et al.
- Teaching Coq and teaching with Coq
- Hydras & Co., accompanying textbook here.
- The Contributing Guide
- Rocq weekly Calls
- Coq Working Groups
- The next Coq Working Group
- Ideas for the Google Summer of Code 2016
- Wishes for Coq (and a specific page of wishes for unification)
- Wishes for Graphical User Interfaces (and a specific page for CoqIDE wishes)
- Basic architecture of Coq User Interfaces
- A development tutorial
- Development frequently asked questions
- List of maintainers
- Archive of discussions
- Setting up your development environment
- State of the continuous integration infrastructure
Rocq Users and Developers Workshops
Pointers to existing projects involving Rocq.
A non-exhaustive list of Rocq libraries that are being used by other people than the developers.
- Rocq Platform - A Coq installation for Windows, Linux, and MacOS together with a large family of libraries chosen for stability and tested for interoperability. For Rocq 8.16 the precise list is here
- Rocq Community - a repository containing numerous and diverse Rocq packages collectively maintained by the Rocq community.
- Mathematical Components: formalization of mathematical theories, focusing in particular on group theory.
- Flocq: formalization of floating-point computations.
- TLC: a non-constructive alternative to Rocq's standard library.
- ExtLib: a collection of theories and plugins that may be useful in other Rocq developments.
- CoLoR: a library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Rocq standard library (especially on vectors)
- Coq-std++: an extended "Standard Library" for Rocq
- Alternative “Standard” Libraries: list and descriptions of alternative standard libraries
(to be completed)
(section to be updated)
- Some help on this Wiki.
- More content
- List of recent changes (compare two revisions by selecting them then clicking on "Compare Revisions")
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.