Stream: Miscellaneous

Topic: Stream creation and naming policy

Cyril Cohen (May 06 2020 at 11:57):

Welcome to the coq zulip chat. First, manage your subscriptions https://coq.zulipchat.com/#streams/subscribed

Karl Palmskog (May 08 2020 at 10:50):

who are the admins? I mistakenly created a stream, and now I can't remove it... To be honest, should stream creation even be allowed for ordinary users? I think it's extremely confusing.

Karl Palmskog (May 08 2020 at 10:56):

I think there needs to be heavy curation of the stream list, otherwise one needs to go through a long decision process to figure out where one should add anything

Théo Zimmermann (May 08 2020 at 10:56):

The admins are @Cyril Cohen and myself. I activated stream creation for ordinary users because I considered that this Zulip would be more welcoming to external Coq projects if a project author could simply go ahead and create a stream. Zulip also supports the concept of new vs full members. If we activate this, we could restrict stream creation to full members only (a status that you get after a few days of activity). Should we do this?

Théo Zimmermann (May 08 2020 at 10:58):

Karl Palmskog said:

I think there needs to be heavy curation of the stream list, otherwise one needs to go through a long decision process to figure out where one should add anything

Could you elaborate on this or maybe give an example?

Karl Palmskog (May 08 2020 at 10:58):

yeah, any stream creation limits are good

Théo Zimmermann (May 08 2020 at 10:59):

Is the "Coq conventions" the stream you want to remove?

Karl Palmskog (May 08 2020 at 11:00):

Could you elaborate on this or maybe give an example?

should streams be "topics" in general or "projects"? If it's projects, I guess it can work, but if you have one "Coq documentation" and one "Coq", it will rapidly get confusing

Karl Palmskog (May 08 2020 at 11:00):

Théo Zimmermann said:

Is the "Coq conventions" the stream you want to remove?

yes, exactly, I wanted this to be a topic under Coq

Karl Palmskog (May 08 2020 at 11:02):

already, having "math-comp development" and "math-comp library" makes it hard to decide where things should go

Karl Palmskog (May 08 2020 at 11:02):

for example, one might have a question about the implementation of some SSReflect tactics, and maybe even how to change it

Théo Zimmermann (May 08 2020 at 11:03):

Streams should correspond to projects, although it makes sense to have a stream for devs and a stream for users (I think).
That's kind of the same idea with the renaming of the imported Coq Gitter channel into "Coq and plugin development"

Théo Zimmermann (May 08 2020 at 11:03):

Karl Palmskog said:

for example, one might have a question about the implementation of some SSReflect tactics, and maybe even how to change it

Sounds like a dev topic to me.

Karl Palmskog (May 08 2020 at 11:04):

but what about Coq itself, I don't see a distinction between Coq dev and Coq whatever?

Karl Palmskog (May 08 2020 at 11:06):

it may help if there was a convention like: "<project-name>" and "<project-name>-development" for top streams

Théo Zimmermann (May 08 2020 at 11:07):

Karl Palmskog said:

but what about Coq itself, I don't see a distinction between Coq dev and Coq whatever?

There is not yet a "Coq users" channel but I definitely see why Coq users would like to follow a channel where they can answer to questions on Coq without having to be flooded with long discussions between devs.

Gaëtan Gilbert (May 08 2020 at 11:08):

Streams should be things where one expects to want multiple threads in them.
Otherwise a thread is sufficient.

Karl Palmskog (May 08 2020 at 11:14):

Gaëtan Gilbert said:

Streams should be things where one expects to want multiple threads in them.
Otherwise a thread is sufficient.

this is a very generous criterion, let's say you log in and there are 100+ streams? just figuring out which ones people are actually using and for what will take a lot of time (and no, descriptions seldom match)

Théo Zimmermann (May 08 2020 at 11:18):

I've renamed a bunch of streams in line with your suggestion @Karl Palmskog

Théo Zimmermann (May 08 2020 at 11:22):

And as a follow-up, I've created the "Coq users" stream and added it to the default streams for new users (with "Announces").

Karl Palmskog (May 08 2020 at 11:23):

very nice, that helps a ton for me personally on how to use the chat, and also hopefully for new users

Karl Palmskog (May 08 2020 at 11:25):

now if we only can convince @Cyril Cohen to rename "Mathematical Components Library" to just "math-comp users"...

Théo Zimmermann (May 08 2020 at 11:26):

It's too bad that we cannot have stream-specific moderators, but if anyone wants to rename a channel (especially those for which I haven't added the "devs" / "users" qualifiers yet), feel free to ping me.

Cyril Cohen (May 08 2020 at 12:07):

I meant this channel to be reserverd for announcments, so that a new user see only very few and relevant information when logging in, I screwed up by not explaining and not restricting posting....
I will rename it #general ... and create a new announces as I intended

Notification Bot (May 08 2020 at 12:08):

Cyril Cohen renamed stream Announces to general.

Karl Palmskog (May 08 2020 at 12:11):

sorry for the name nitpicking, but maybe call it something other than "general", such as "meta"? "General" sounds like a general encouragement to ask questions about anything

Théo Zimmermann (May 08 2020 at 12:12):

Couldn't you also have moved the discussion to another stream/topic? It seemed to me that this was one of the core features of Zulip.

Théo Zimmermann (May 08 2020 at 12:13):

This might make sense actually. If people don't know where to ask, they can ask here. We can see how it turns out.

Karl Palmskog (May 08 2020 at 12:14):

in this case I would call it "miscellaneous", but sure, we can wait and see

Cyril Cohen (May 08 2020 at 12:15):

So one can move a discussion to anotherbtopic, but not to another stream....

Théo Zimmermann (May 08 2020 at 12:22):

Turns out that this feature is less powerful than the equivalent in Discourse then! (But in Discourse, it is reserved to admins.)

Cyril Cohen (May 08 2020 at 12:23):

@Théo Zimmermann I think it should be...

Cyril Cohen (May 08 2020 at 12:30):

What we can do is merge streams though... If you think there are too many streams I can send a message the the zulip guys

Théo Zimmermann (May 08 2020 at 12:31):

No, I don't think there are too many streams. I appreciate being able to separate devs from users discussion in high traffic projects.

Cyril Cohen (May 08 2020 at 12:33):

I meant, at a future point in time...

Christian Doczkal (May 08 2020 at 13:41):

Cyril Cohen said:

So one can move a discussion to anotherbtopic, but not to another stream....

Maybe this is the kind of issue to test how well Zulip responds to feature request. Moving a topic to another stream seems useful (e.g., to move a topic that was asked in users to devs in case it turns technical and/or involves changes to the projects code), and it does not seem like it would be hard to implement.

Cyril Cohen (May 08 2020 at 13:42):

@Christian Doczkal you are right, I will ask. I know they were pretty reactive in the integration of my PR modifying gitter import though ;)

Hugo Herbelin (May 10 2020 at 16:11):

What do you think, should we have a stream about continuous integration issues or only a coq devs & plugin devs topic?

Théo Zimmermann (May 10 2020 at 16:20):

I think we should avoid multiplying streams, especially at the beginning. The topic is not distinct enough to be worth a stream IMHO. Streams are especially useful when people might not want to follow part of the discussions, so my impression is that a stream per project (+ sometimes a distinction between users and devs) is enough. We can always decide later on to add more streams if ever we feel the need.

Jonathan Chan (May 19 2020 at 21:46):

Hey I'm kind of new to how Zulip works and I'm not sure about what kind of things Streams and Topics are. If I have a new question to ask, do I pick an existing Topic and ask there (so Topics are like substreams), or do I create a new Topic for it under the appropriate Stream (kind of like a Slack thread)?

Karl Palmskog (May 19 2020 at 21:53):

@Jonathan Chan it's always good to start by searching for some keywords if there is some relevant topic already added somewhere. If not, you pick one of the streams that seems relevant (typically "Coq users") and create a new topic by writing something with that topic

Théo Zimmermann (May 20 2020 at 09:30):

The power of Zulip comes from the fact that if a topic is diverging, it is always possible to extract a new topic out of it.

Last updated: Dec 07 2023 at 06:38 UTC