[Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)

[Jesper Cockx]

Dear Agdakkers,

In his recent mail, Jacques raised an important point that got lost in the
rest of the conversation:

> - the community ought to pick a single communication system (Slack,
Discord, Zulip, gitter, whatever, but just one!)

I wholeheartedly agree with this! Github does a reasonable job of keeping
track of issues and feature requests, and this mailing list works well for
broadcasting messages to the broader community, so these two we should
definitely keep. But it would be nice to consolidate all other discussions
and questions on a single platform.

Here are some of the current options with my opinion on them:

- IRC: An open system but based on archaic technology. I'm having a hard
time browsing the history of a channel when I'm not always connected.
- Slack: Seems to be the de facto standard for many people and we used it
successfully during the latest Agda meeting. However, it is commercial
software and keeping a full history is not free.
- Gitter: Is well integrated with Github but feels otherwise quite
barebones compared to Slack.
- Discord: Many features are more aimed at gamers than programmers. Some
people used it for screensharing during the Agda meeting. It is commercial
software and we'd have to pay for certain features
- Zulip: Has a nice threaded interface to conversations that can take a
while to get used to. It is 100% open source software and is explicitly
aimed at open source communities (https://zulipchat.com/for/open-source/).
The HoTT community also seems to be using it quite effectively.
- MatterMost, RocketChat, Matrix.org, ...: These are other open source
alternatives to Slack, but they seem to be less popular than Zulip in the
type theory / formalized math circles.

My personal preference would be to centralize all communication (other than
Github and the mailing list) on Zulip. But since this is an important
decision, I would very much like to hear other opinions as well before we
decide on anything.

Cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200821/cbd54987/attachment.html>