Stream: Zulip meta

Topic: Splitting lean4?

Scott Morrison (Mar 08 2021 at 22:13):

I wonder if it is reaching the point we should have multiple lean4 streams. My thinking is basically we should have "stuff Leo might want to see" and "stuff he won't". Zulip maintainers can then try to shuffle things into the right places at first.

Mario Carneiro (Mar 09 2021 at 05:32):

I don't think it's worth it at this time. The issue seems to be a mismatch of expectation regarding the level of formality on zulip in general, and I don't think we should make a split along formality lines because an #off-topic stream is sure to draw more off-topic things than we already get. I don't think we need to change anything regarding the level of jokes / code of conduct stuff either.

Scott Morrison (Mar 09 2021 at 05:52):

I was thinking more in terms of splitting into lean4-getting-started, lean4-general, and lean4-issues.

Kevin Buzzard (Mar 09 2021 at 07:30):

Oh that might be worth a try

Last updated: May 08 2021 at 21:09 UTC