it's becoming a common occurrence that people ask MathComp questions in the #Coq users stream. The main reason is that people who join the Zulip are not even aware of that there are MathComp streams, since they are not subscribed to any by default.
Maybe it would make sense to subscribe people to #math-comp users by default and let people mute/unsubscribe if it's not relevant to them? The general activity in streams besides the general Coq users stream is low anyway.
This also happens with Ltac2 questions, but moving topics doesn't seem such a big issue to me.
@Karl Palmskog We could make you a moderator so that you can move topics between streams without pining @Cyril Cohen or me.
OK, if you think that's a better option
I've promoted you to moderator. Note that we can do that for other trusted community members as well.
As for the default stream list, my position is not a strong one, so this is up to debate.
OK, I don't even know where we discuss this stuff, I guess under Misc?
This topic was moved here from #math-comp users > Default subscribed streams by Karl Palmskog
Minor downside: migrating topic to hidden streams could hide them from other interested parties in the same situation. (EDIT: maybe not)
Otherwise, subscribing people to Ltac2 by default seems a safe first migration step, even considering the last discussion.
yeah, we should by default subscribe participants to the new stream a topic is moved to.
I was assuming the participants would be handled by Zulip — I was thinking of people who missed the question. OTOH, zulip does leave a link in the old stream...
right, the migration strategy can even be used for stream discovery. But I think we should have something like 4-5 people that are actively relocating stuff they see, and promoting "newly" created specialized streams.
Last updated: Nov 29 2023 at 19:01 UTC