Enable github discussions for this project (or metamath organization)

[savask]

In recent years the discussions surrounding set.mm and metamath itself moved mostly from google groups to this repository. Hence quite often issues are used to ask for opinions and propose ideas, and sometimes even to ask for guidance and help. The original purpose of issues is to track real problems and goals, though.

I suggest we enable github discussions for this project. For those who haven't seen it in action, it is a sort of forum available on the project page (a tab next to "Pull requests"), where people can ask questions, discuss minor problems, make polls etc. One can convert a given issue into a discussion, so if this is implemented, we can clean the issues tab a little bit and reserve it to "real" issues so to speak.

As far as I know, it is also possible to enable discussions for an entire metamath organization, so in theory that could be used to ask "interdisciplinary" questions related to metamath-knife, metamath.exe etc, but I haven't used this functionality, so I'm not sure here.

[wlammen]

To give this idea a head start, and check whether it is an improvement over the google group, I suggest to make it a first topic in the github discussions. Then we can perhaps better see how well it is received.

Edit: I don't have sufficient rights to enable 'Discussions' features for Metamath.
For those with sufficient rights: here's the todo https://docs.github.com/en/discussions/quickstart

[savask]

To give this idea a head start, and check whether it is an improvement over the google group, I suggest to make it a first topic in the github discussions. Then we can perhaps better see how well it is received.

Just to clarify, I haven't meant this suggestion as a replacement to google groups, it just seems to be a fact of life that google groups are mostly lifeless while all important questions are discussed and settled here.

I agree with the idea of moving this issue to discussions once (and if) they are enabled.

For those with sufficient rights: here's the todo ...

I think @david-a-wheeler or @digama0 should be able to do this, so I'll ping them just in case.

[digama0]

I do worry about further splitting metamath communication across multiple fora. I remember how well the metamath gitter went... I'll let others chime in first, I would prefer to see a majority of active contributors favoring it.

[david-a-wheeler]

It's true that @digama0 or I can enable GitHub discussions. It sounds like the proposal is to replace the use of the mailing list with GitHub discussions.

I have a mild preference for mailing lists. If Google Groups shut down, we have the list of email addresses & could move somewhere else. If we use only GitHub discussions, I don't think we could do the same so easily. Many other organizations are moving to mailing lists, to ensure they aren't beholden to a company. Personally, I have to track a number of things, and having them all go into my inbox is convenient to me.

However, what's most important is enabling progress on formalized mathematics. If switching to GitHub discussions would help, then great! I'd want to hear more from others in the Metamath community, & discussion on the mailing list first, before making such a big change.

[savask]

It sounds like the proposal is to replace the use of the mailing list with GitHub discussions.

It absolutely wasn't my intention to suggest replacing google groups, as I wrote in my previous message.

My real intention was to stop the practice of asking questions in github issues (anyone can open the issues tab right now and see quite a few open ended questions among genuine issues - I'm not linking them here to avoid pinging the relevant authors). Of course these questions could have been asked in google groups, but they haven't. Part of the reason is that it's much more convenient to reference specific commits, issues etc here on github, and another reason is that anyone who is planning to contribute to set.mm seriously is going to use github anyway.

To reiterate, I'm all for doing announcements on google groups or asking for questions or directions etc, but it seems that most discussions happen here anyway, so why not make it a little bit more convenient.

Now, it is possible that active contributors are fine with using issues for questions and discussions, or perhaps they don't find the github discussions functionality appealing. In that case we can indeed simply leave things as is.

[benjub]

A trigger for this thread (@savask may confirm) is probably my question at #4279 : as I wrote on its first line, it was more of a question, but I posted it here rather than the mailing list because:

• it was specifically about a database hosted here (namely, set.mm)
• I wanted advice from someone here and to be able to ping him (or actually, two persons, still not sure: @sctfn and @scott-fenton)
• it was on the same platform as the repo, which was convenient to me.

These are just data points, and I have no strong opinions either way.

[savask]

A trigger for this thread (@savask may confirm) is probably my question at #4279

That is true :-) Though there are other issues which do the same, it just so happened that in the mean time I saw another repository use github discussions, so I thought it is timely to suggest enabling them here. Of course three points you list (the question being set.mm related, pinging relevant people, being on the same platform) apply to most discussions we have about metamath.

[metakunt]

Honest opinion. I don't particularily like the mailing list because I like locality.
Having to go to a different place is already too much. Especially because it also was quite difficult to set up.
If I think about it, where would I find the most developers/maintainers? That's right, on github, where people are creating PR's and merging their work. It's also a decent way to track progress.

I am in favour of moving discussions to github, as my first instinct was to just open an issue and hope for some helpful answers. This would also declutter the issues page a bit.

[tirix]

One advantage of Github issues vs. Mailing list is that you can tag people and limit some conversations to only those interested. Does "Discussions" work the same way? I often fear that a mail to the mailing list will spam many people who might not be interested.

Maybe we could start a trial, for just one topic ?

[savask]

Does "Discussions" work the same way?

Each discussion also has a "participants" list, just like an issue, so I think it should work in the same way (I've never participated in "discussions" myself, only read them).

Maybe we could start a trial, for just one topic ?

Several people have already spoken in favor or were curious to try it out - maybe @david-a-wheeler or @digama0 could set up a trial run for us, after all? If "discussions" turn out to be useless, we can always convert important topics into issues (there's a button for that in each discussions topic), and disable the feature.

[jkingdon]

set up a trial run for us, after all? If "discussions" turn out to be useless, we can . . .

I guess that's my sentiment: willing to experiment. I don't know if using issues as we have been causes a lot of problems but Discussions do seem to have a few features, like polls and upvotes, which I suppose might make them better for gathering opinions or comparing alternatives.

I do hope we keep the mailing list and also participate in places like https://proofassistants.stackexchange.com/questions/tagged/metamath as people have the time and interest, for reasons including not being too dependent on one platform. But at least in my mind that's mostly separate from what feature set we use within github.