Community
We have a code of conduct that applies to all spaces (online forums as well as physical events) managed by the Coq team. Make sure you read it and abide by it. Note that it contains a section specifically on how to ask questions on Coq forums.
There are several channels to reach the user community and the development team:
- Our Zulip chat, for casual and high traffic discussions, which are continuously archived.
- Our Discourse forum, for more structured and easily browsable discussions and Q&A. Posts in other languages than English are explicitly welcome there.
- The Proof Assistants Stack Exchange Q&A site. Make sure to use the coq tag to get your questions noticed by Coq users.
- Our historical mailing list, the Coq-Club.
- Our GitHub issue tracker, for bug reports and feature requests.
The following channels also have a strong presence of Coq users:
- Other sites in the Stack Exchange Q&A site galaxy, such as Stack Overflow (coq tag) and TCS Stack Exchange (coq tag) also receive questions about Coq.
- /r/Coq on Reddit.
- The #coq IRC channel on Libera.Chat.
Our @CoqLang Twitter account is managed by community members and developers.
The page Planet Coq lists recent discussions from many of the above channels.
The Coq user community has contributed a large ecosystem of formalization works and plugins throughout the years. An index of packages can be browsed online. Installing them can be done using the opam package manager. A subset of these packages are also included in the Coq Platform.
Users are encouraged to submit their packages to the index. They are also encouraged to add their projects to Coq's Continuous Integration. In particular, for authors of projects that link to Coq's ML API (a.k.a. plugins), this can be really useful as it allows getting updates from the development team when the (unstable) ML API receives breaking changes.
An informal organization of users, called coq-community, exists to ensure the long term maintenance of Coq packages, and advance other collaborative projects such as documentation writing; it is always looking for new volunteers. Among other projects, coq-community hosts Awesome Coq, a curated list of Coq formalizations, plugins, tools, and resources.
Coq developers and interested users gather every month through visio-conference for Working Groups. You are welcome to attend!
The Coq development team organizes a one-week-long Coq Users and Developers Workshop (CUDW) every year in France. The goal is to help users become contributors by guiding them and answering their questions.
Other Coq workshops:
- Coq Workshops (generally colocated with ITP)
- CoqPL workshops (colocated with POPL)
- Iris tutorials and workshops (since 2018)
Coq schools:
- Coq / Math-Comp Winter Schools
- DeepSpec Summer Schools (2017; 2018; 2020 editions)
- School and Workshop on Univalent Mathematics (2017; 2019; 2020; 2022; 2024 editions)
- Other past or non-recurring events