<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>> I (obviously) don't want to ban any kind of conversation on
Agda in other places<br>
<br>
Good! But yes, I guess I just wanted to hint at the fact that
spawning any new channel might just turn out to fragment the
community /more/ (insert relevant xkcd here).<br>
<br>
> For IRC specifically, there is a bidirectional integration of
IRC to Zulip<br>
<br>
Neat!<br>
<br>
> Two advantages of Zulip over Discord are (1) it supports
better integration with Github, and (2) open source communities
get access to all features for free.<br>
<br>
Also neat.<br>
<br>
Arjen<br>
</p>
<div class="moz-cite-prefix">On 8/21/20 1:52 PM, Jesper Cockx wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAEm=boyJo1c3k38FxJGqyD2gw8jEGwG5YrLSAk-=q8ObcYd-FA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr"><span></span>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>A wild thought that might seem impossible to some, but is
much in line<br>
with the proposal: Get rid of the mailing list as well in
the long run.<br>
I'd consider mailing lists to be quite an arcane,
unscalable, closed,<br>
poorly searchable medium. Of course, a technologically
superior<br>
alternative such as Discourse or Zulip would have to be
installed and<br>
stabilised first, and ongoing discussions (and possibly the
mailing list<br>
history) moved there.<br>
</div>
</blockquote>
<div><br>
</div>
<div>I agree that email is an outdated technology, however it is
too entrenched to just get rid of it (unlike, say, the current
Slack or Discord servers). If we have a clear alternative that
works better, then conversations will naturally move over to
there. <br>
</div>
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div><span>Although I agree with the intent, I suspect that
trying to convince the entirety of the community to
consolidate on a single platform is bound to fail.<br>
For example, the #agda freenode channel is not going
anywhere soon. Another example that I only became aware
of: the functional-programming slack (<a
href="http://functionalprogramming.slack.com"
target="_blank" moz-do-not-send="true">functionalprogramming.slack.com</a>)
has an #agda channel with 400 members, and is also on
zulip (<a
href="https://funprog.zulipchat.com/login/#narrow/stream/215389-Agda"
target="_blank" moz-do-not-send="true">https://funprog.zulipchat.com/login/#narrow/stream/215389-Agda</a>).<br>
</span></div>
</blockquote>
<div><br>
</div>
<div>I (obviously) don't want to ban any kind of conversation on
Agda in other places, this is more about having an "official"
channel that we can link to from the website and use for
things like helping people with their code and online Agda
meetings. <br>
</div>
<div><br>
</div>
<div>For IRC specifically, there is a bidirectional integration
of IRC to Zulip, so it can continue to exist (and perhaps
there will even be more people reading the messages on it via
Zulip).<br>
</div>
<div><br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div><span> Personally, I'd like to vouch for Discord---but am
not against Zulip perse, since I have no experience with
it.<br>
Communities like <a
href="https://discord.com/invite/reasonml"
target="_blank" moz-do-not-send="true">https://discord.com/invite/reasonml</a>
are extremely easy access and heavily used by programmers.<br>
Slack is slow and tedious nowadays.</span></div>
</blockquote>
<div><br>
</div>
<div>Two advantages of Zulip over Discord are (1) it supports
better integration with Github, and (2) open source
communities get access to all features for free. OTOH Discord
has integrated audio/video chat and screensharing, so there's
a tradeoff.</div>
<div><br>
</div>
<div>-- Jesper<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Fri, Aug 21, 2020 at 1:38
PM a.j.rouvoet <<a href="mailto:a.j.rouvoet@gmail.com"
target="_blank" moz-do-not-send="true">a.j.rouvoet@gmail.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<p>Although I agree with the intent, I suspect that trying
to convince the entirety of the community to consolidate
on a single platform is bound to fail.<br>
For example, the #agda freenode channel is not going
anywhere soon. Another example that I only became aware
of: the functional-programming slack (<a
href="http://functionalprogramming.slack.com"
target="_blank" moz-do-not-send="true">functionalprogramming.slack.com</a>)
has an #agda channel with 400 members, and is also on
zulip (<a
href="https://funprog.zulipchat.com/login/#narrow/stream/215389-Agda"
target="_blank" moz-do-not-send="true">https://funprog.zulipchat.com/login/#narrow/stream/215389-Agda</a>).<br>
<br>
That being said, you can certainly ensure that the Agda
website etc. picks one solid medium that can be used for
all casual communications besides the mailing list and the
issue tracker. Do not just spawn a new one; make sure you
move the conversation and kill off the ones managed by the
Agda team that are then deprecated (slack, gitter, ...).<br>
<br>
Personally, I'd like to vouch for Discord---but am not
against Zulip perse, since I have no experience with it.<br>
Communities like <a
href="https://discord.com/invite/reasonml"
target="_blank" moz-do-not-send="true">https://discord.com/invite/reasonml</a>
are extremely easy access and heavily used by programmers.<br>
Slack is slow and tedious nowadays.<br>
<br>
(Sorry Jesper, I intended to reply to the list)<br>
</p>
<div>On 8/21/20 1:23 PM, Jesper Cockx wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div>Dear Agdakkers,</div>
<div><br>
</div>
<div>In his recent mail, Jacques raised an important
point that got lost in the rest of the conversation:</div>
<div><br>
</div>
<div>> - the community ought to pick a single
communication system (Slack, Discord, Zulip, gitter,
whatever, but just one!)</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>Here are some of the current options with my
opinion on them:</div>
<div><br>
</div>
<div>- 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.</div>
<div>- 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.</div>
<div>- Gitter: Is well integrated with Github but feels
otherwise quite barebones compared to Slack.</div>
<div>- 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</div>
<div>- 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 (<a
href="https://zulipchat.com/for/open-source/"
target="_blank" moz-do-not-send="true">https://zulipchat.com/for/open-source/</a>).
The HoTT community also seems to be using it quite
effectively.</div>
<div>- 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.<br>
</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>Cheers,</div>
<div>Jesper<br>
</div>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</body>
</html>