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

[Jesper Cockx]

I hopped onto the agda:matrix.org 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:

The biggest issue with Matrix is when people (like us unfortunately) use
> the matrix.org homeserver, which is severely over capacity (
> https://t2bot.io/docs/2020-matrix-org-lag/). This causes events, e.g.
> push notifications and messages, to sometimes be severely delayed, although
> I haven't noticed this super recently
>
> Ideally, each university/CS department should have their own homeserver -
> I've been trying to set ours up in OxfordI feel that discourse (and
> forums in general) is a different medium to webchat, and we actually have a
> discourse instance too at discourse.agda.club
>
> 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
>
> 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
>
> In particular I'm excited for element to adopt LaTeX support (
> https://github.com/matrix-org/matrix-react-sdk/pull/3251), which is on
> the roadmap and should happen soon(TM)
>
> 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..)
>
> Matrix supports markdown with syntax highlighting, so you can write things
> like
>
> main :: IO ()main = undefined
>
> It uses highlight.js <https://highlightjs.org/> for this, so if someone
> were to write a highlight.js plugin for Agda then that might be nice 😉
>

 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.

-- Jesper

On Fri, Aug 21, 2020 at 2:15 PM Jesper Cockx <Jesper at sikanda.be> wrote:

> One property of e-mail that I like is that one can choose between many
>> different clients. Does the same apply to any of the other communication
>> methods being discussed?
>>
>
> 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.
> https://element.io/. I have never tried it myself however, so I can't say
> much about it other than that.
>
> -- Jesper
>
> On Fri, Aug 21, 2020 at 1:58 PM Nils Anders Danielsson <nad at cse.gu.se>
> wrote:
>
>> On 2020-08-21 13:35, Manuel Bärenz wrote:
>> > I'd consider mailing lists to be quite an arcane, unscalable, closed,
>> > poorly searchable medium. Of course, a technologically superior
>> > alternative such as Discourse or Zulip would have to be installed and
>> > stabilised first, and ongoing discussions (and possibly the mailing list
>> > history) moved there.
>>
>> One property of e-mail that I like is that one can choose between many
>> different clients. Does the same apply to any of the other communication
>> methods being discussed?
>>
>> --
>> /NAD
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200821/c835aa96/attachment.html>