The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

TL;DR: Coq-Club will be closed, turned into archive mode and messages will be automatically rejected in one month from now (i.e. end of November). Below, we present available alternatives, including how to post CFPs, and how to keep interacting via email.

Dear Coq-Club subscribers,

Following the renaming, the Rocq team has decided that the Coq-Club (and Coqdev) mailing lists would be closed, rather than being renamed, in favor of more modern communication platforms. This is done in particular to facilitate the work of the moderators / code of conduct enforcement team. Below, we present the alternatives, and how you can use them, in particular if your preferred interaction means is email.

There are several platforms on which you can interact with the Rocq community. Official platforms are GitHub (for bug reporting and contributing through pull requests), Discourse (for forum/mailing-list style discussions and announcements), and Zulip (for chat style discussions). In addition to the official platforms, Rocq users are active on many other platforms, including notably the Proof Assistants Stack Exchange and Mastodon (where the Rocq Prover has an official account).

The most active platform in the community is Zulip. It offers various channels that you can subscribe to, including channels around specific projects (e.g., Ltac2, Equations, MathComp, MetaRocq, and many others) and topics (Teaching [with] Rocq, User interfaces, Machine learning and automation, etc.). It also hosts public or private channels dedicated to Rocq courses, summer schools, etc.

The best alternative to the mailing list is Discourse. It is a forum with mailing-list feature parity. When you register there, you can set things up to receive every new post or reply as an email (including your own activity), just like you would with a mailing list. You can also create a new topic by email using a few email addresses, depending on which category in the forum you wish to post to. See https://github.com/rocq-prover/rocq/wiki/Discourse to learn more. In particular, CFPs (which were becoming the main use of Coq-Club recently) can be posted to rocq+cfp AT discoursemail.com. If you don't want to subscribe to all of the Discourse activity by email (mailing-list mode), you have the option to receive daily, weekly, or monthly summaries, and you can set specific parameters by category (e.g., if you want to see all the emails posted to the Announcements category).

In addition, to promote the discussion on the Rocq Prover in other languages than English, Discourse has language-specific categories. You can easily mute these if you don't speak the languages.

For better integration of the various communication platforms, we have bots that post any new Discourse topic (except those in non-English categories) or Stack Exchange question (tagged coq or rocq-prover) to appropriate Zulip channels. This is notably the case for any announcements on Discourse (including CFPs) which are publicized in the #Annoucements channel on Zulip, which is otherwise read-only.

See you on Discourse and/or Zulip!

— Matthieu Sozeau, for the Rocq Development Team