Stream: Miscellaneous

Topic: Default subscribed streams

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 24 2021 at 20:20):

OK, if you think that's a better option

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 24 2021 at 20:32):

OK, I don't even know where we discuss this stuff, I guess under Misc?

view this post on Zulip Notification Bot (Oct 24 2021 at 20:34):

This topic was moved here from #math-comp users > Default subscribed streams by Karl Palmskog

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Oct 24 2021 at 20:35):

yeah, we should by default subscribe participants to the new stream a topic is moved to.

view this post on Zulip 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...

view this post on Zulip 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: Nov 29 2023 at 19:01 UTC