Documentation
(Part of the Coq FAQ)
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.
The main Coq mailing list is coq-club@inria.fr, 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.
The archives of the Coq mailing list are available at http://sympa.inria.fr/sympa/arc/coq-club.
New versions of Coq are announced on the coq-club mailing list and on the News page of the Coq website.
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."
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.
Please create a new issue in Coq's GitHub repository at https://github.com/coq/coq/issues.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.