Karl Palmskog (Oct 24 2021 at 16:00): Karl Palmskog (Oct 24 2021 at 16:00):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.
Théo Zimmermann (Oct 24 2021 at 20:14):This also happens with Ltac2 questions, but moving topics doesn't seem such a big issue to me.
Théo Zimmermann (Oct 24 2021 at 20:15):@Karl Palmskog We could make you a moderator so that you can move topics between streams without pining @Cyril Cohen or me.
Karl Palmskog (Oct 24 2021 at 20:20):OK, if you think that's a better option
Théo Zimmermann (Oct 24 2021 at 20:28):I've promoted you to moderator. Note that we can do that for other trusted community members as well.
Théo Zimmermann (Oct 24 2021 at 20:29):As for the default stream list, my position is not a strong one, so this is up to debate.
Karl Palmskog (Oct 24 2021 at 20:32):OK, I don't even know where we discuss this stuff, I guess under Misc?
Notification Bot (Oct 24 2021 at 20:34):This topic was moved here from #math-comp users > Default subscribed streams by Karl Palmskog
Paolo Giarrusso (Oct 24 2021 at 20:34):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.
Karl Palmskog (Oct 24 2021 at 20:35):yeah, we should by default subscribe participants to the new stream a topic is moved to.
Paolo Giarrusso (Oct 24 2021 at 20:36):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...
Karl Palmskog (Oct 24 2021 at 20:39):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: Jun 01 2023 at 13:01 UTC