<div dir="ltr"><div>I hopped onto the agda:<a href="http://matrix.org">matrix.org</a> server (which already exists and is being used by the Oxford Agda people) and asked for opinions on the platform, which Nick Hu was kind enough to provide:</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 class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto"></span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto">The biggest issue with Matrix is when people (like us unfortunately) use the <a href="http://matrix.org" class="gmail-linkified" target="_blank" rel="noreferrer noopener">matrix.org</a> homeserver, which is severely over capacity (<a href="https://t2bot.io/docs/2020-matrix-org-lag/" class="gmail-linkified" target="_blank" rel="noreferrer noopener">https://t2bot.io/docs/2020-matrix-org-lag/</a>). This causes events, e.g. push notifications and messages, to sometimes be severely delayed, although I haven't noticed this super recently</span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><div class="gmail-mx_LinkPreviewWidget"></div></span><br><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto">Ideally, each university/CS department should have their own homeserver - I've been trying to set ours up in Oxford</span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto">I feel that discourse (and forums in general) is a different medium to webchat, and we actually have a discourse instance too at <a href="http://discourse.agda.club" class="gmail-linkified" target="_blank" rel="noreferrer noopener">discourse.agda.club<br><br></a></span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto">Slack has this weird user limit and privacy issues because you have to let them host it, and I don't think it offers any tangible benefit over Matrix - it doesn't do anything particularly novel, and as far as I can tell it's just IRC made proprietary and marketed for millions of dollars<br><br></span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto">Zulip is the same as slack except you have the "killer feature" of threads - to me, it seems like at any moment slack could implement this and then zulip will be abandoned</span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto"><br><br>In particular I'm excited for element to adopt LaTeX support (<a href="https://github.com/matrix-org/matrix-react-sdk/pull/3251" class="gmail-linkified" target="_blank" rel="noreferrer noopener">https://github.com/matrix-org/matrix-react-sdk/pull/3251</a>), which is on the roadmap and should happen soon(TM)</span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto"><br><br>Mozilla and the French government have adopted Matrix, so hopefully that's convincing enough to show you it's not so niche! (Although polish is undoubtedly desired, we'll get there..)<br><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body" dir="auto"></span></span></span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body gmail-markdown-body" dir="auto"><p>Matrix supports markdown with syntax highlighting, so you can write things like</p>
<div class="gmail-mx_EventTile_pre_container"><pre><code class="gmail-language-haskell gmail-hljs"><span class="gmail-hljs-title">main</span> :: <span class="gmail-hljs-type">IO</span> ()
<span class="gmail-hljs-title">main</span> = undefined
</code></pre><span class="gmail-mx_EventTile_copyButton"></span></div>
</span></span><span class="gmail-mx_MTextBody gmail-mx_EventTile_content"><span class="gmail-mx_EventTile_body gmail-markdown-body" dir="auto">It uses <a href="https://highlightjs.org/" target="_blank" rel="noreferrer noopener">highlight.js</a> for this, so if someone were to write a highlight.js plugin for Agda then that might be nice 😉</span></span></div></blockquote><div><br></div><div> Although it still feels slightly less mature than Zulip, I think Matrix actually shows a lot of potential, and the fact that it's open to alternative clients is a big plus. So we should definitely also consider it as an option.</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 2:15 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</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 dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><span></span>
One property of e-mail that I like is that one can choose between many<br>
different clients. Does the same apply to any of the other communication<br>
methods being discussed?<font color="#888888"><br>
</font></div></blockquote><div><br></div><div>As far as I know the only platform with this feature is Matrix.org, which is designed as an open platform with many possible clients, e.g. <a href="https://element.io/" target="_blank">https://element.io/</a>. I have never tried it myself however, so I can't say much about it other than that.</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:58 PM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</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">On 2020-08-21 13:35, Manuel Bärenz wrote:<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>
<br>
One property of e-mail that I like is that one can choose between many<br>
different clients. Does the same apply to any of the other communication<br>
methods being discussed?<br>
<br>
-- <br>
/NAD<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>