<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>