Documentation - coq/coq GitHub Wiki

Where can I find documentation about Coq?

All the documentation about Coq, from the reference manual to friendly resources such as this tutorial and documentation of the standard library, is available online. All these documents are viewable either in browsable HTML or as downloadable files.

Is there any mailing list about Coq?

The main Coq mailing list is [email protected], which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See http://sympa.inria.fr/sympa/info/coq-club for subscription. For bugs reports see below.

Where can I find an archive of the list?

The archives of the Coq mailing list are available at http://sympa.inria.fr/sympa/arc/coq-club.

How can I be kept informed of new releases of Coq?

New versions of Coq are announced on the coq-club mailing list and on the News page of the Coq website.

Is there any book about Coq?

The first book on Coq, Yves Bertot and Pierre Castéran's Coq'Art, was published by Springer-Verlag in 2004:

"This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-default software."

Where can I find some Coq examples?

There are examples in Coq's reference manual and in the exercises of the Coq'Art book. You can also find large developments using Coq in the Coq Package Index.

How can I report a bug?

Please create a new issue in Coq's GitHub repository at https://github.com/coq/coq/issues.