Please open a Gitter channel

[ejgallego]

I often get mails asking questions about ssreflect / math-comp; please open a Gitter channel and add a Gitter badge to the project README so I can direct people to the chat.

Thanks!

[CohenCyril]

Hi @ejgallego, I am trying to understand the pros and cons here.

Could you briefly explain how this would help, compared to directing this people to the ssreflect mailing list, which is, according to the project's README "the primary venue for help and questions about the library."?

[amahboubi]

We can just open it and let users decide which channel works best for them.

[ejgallego]

Hi @ejgallego, I am trying to understand the pros and cons here.

I don't see a lot of cons other than people "losing" time in the channel.

Could you briefly explain how this would help, compared to directing this people to the ssreflect mailing list, which is, according to the project's README "the primary venue for help and questions about the library."?

It is a good question; I guess you are already familiar with how things go for other systems such as Lean and Zulip chat. For some reason the chat seems better suited to small interactive discussion. Mailing lists tend to be seen as burdensome by some younger scientist, and also it is the factor of "spam".

It was not so long for example that people complained about "excessive mail" on Coq Club; recall that when we asked at Sophia why plugins developers didn't write more to coq-club/dev their answer was "I know Pierce and Apple are reading, I am scared to write".

[ejgallego]

But indeed both channels are a bit different and IMVHO interactive discussion has certain advantages.

Note the we also have the StackOverflow which is a de-facto help channel for math-comp, and there even many questions are often redirected to math-comp as it provides the best available solution.

[CohenCyril]

@ejgallego I am a bit afraid by the scattering of questions among numerous supports. Maybe the solution is to close the mailing list and announce another privileged way of interaction between users and developers. Maybe this other way is gitter, maybe it is zulip, maybe it is stackoverflow?
I had the impression than gitter was more dev oriented, stackoverflow more user oriented, and I see the Lean community using Zulip as both...
As discussed briefly with @amahboubi, this will be in the agenda of the next mathcomp meeting.

[ejgallego]

I agree that scattering of questions is not ideal, however it is also hard to avoid I'd dare to say.

I am not sure why you would want to close help channels, tho; each of the 3 media [chat, SO, mail] are different enough as to serve different purposes.

[CohenCyril]

I agree that scattering of questions is not ideal, however it is also hard to avoid I'd dare to say.

One way to avoid it, is to think carefully before creating a new one. E.g. opening at most one out of zulip or gitter.

[anton-trunov]

I see the Lean community using Zulip as both...

One nice thing I personally like about Zulip (although I'm not a proficient user) is that it's topic-oriented ("streams"). With Gitter it's really hard to separate different conversations.

Let me make yet another, I must admit rather hacky, proposition: create a quasi-repo, something like math-comp/support or math-comp/questions to use its issues for thematic discussions. People wishing to participate just "watch" that repo.

Pros:

• one gets email notifications;
• its easy to unsubscribe just from an uninteresting thread (unlike mailing lists);
• there is still a possibility to answer by email;
• one still has some GitHub integration;
• markdown support.

Cons:

• no app (or is it a pro?).

I'm sure there are more pros and cons.

In principle, the repo can have some content, e.g. FAQ. And those frequently-asked questions could be added via the pull request mechanism to this repo. I know that a repo can have wiki, but I never liked how that is implemented on GitHub (too unstructured).

[ejgallego]

Oh sure, there should be only one channel; personally I don't like Zulip or Slack as they are closed source and worse, not readable without registering. Gitter is open source and we have some hopes it will integrate well with gitlab.

On the other hand Slack or Zulip do provide much better features that Gitter these days, so I can understand people preferring them.

[ejgallego]

@anton-trunov I'm not sure a repos would work very well for that; wouldn't something like discourse [example https://discuss.ocaml.org/ ] work better for your proposal?

We could open a discuss.coq.org and have a mathcomp section there.

But even for OCaml, discourse didn't centralize a lot, we still have the OCamllabs slack, SO, the discord channel / IRC which is a big one. Even the ML is alive.

Yup, messy times we live in :)

[anton-trunov]

@ejgallego I tried once the Discord app. It made my laptop extremely hot and I gave up on it. Perhaps I should try again. If it has email notifications, I can live with its web interface.

[ejgallego]

So here is a list of communication media people in the OCalm / Coq / Theorem Proving community is using:

• mailman
• sympa
• github
• gitlab
• gitter
• stack overflow
• discord
• discourse
• IRC
• slack
• zulip
• wikimedia
• google hangouts
• skype
• renater / VISIO
• appear.in
• matrix.org

O_O

[anton-trunov]

@ejgallego Thanks for the list!

We could open a discuss.coq.org and have a mathcomp section there.

This sounds like a great idea for Coq in general!

[CohenCyril]

@ejgallego @amahboubi @gares I cannot manage to create https://gitter.im/math-comp it complains the address is not available... Did one of you ever tried to create the organization and not go further?
EDIT: I sent a mail to support@gitter.im

[ejgallego]

Done, thanks!