Welcome to the coq zulip chat. First, manage your subscriptions https://coq.zulipchat.com/#streams/subscribed
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.
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
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?
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?
yeah, any stream creation limits are good
Is the "Coq conventions" the stream you want to remove?
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
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
already, having "math-comp development" and "math-comp library" makes it hard to decide where things should go
for example, one might have a question about the implementation of some SSReflect tactics, and maybe even how to change it
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"
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.
but what about Coq itself, I don't see a distinction between Coq dev and Coq whatever?
it may help if there was a convention like: "<project-name>" and "<project-name>-development" for top streams
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.
Streams should be things where one expects to want multiple threads in them.
Otherwise a thread is sufficient.
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)
I've renamed a bunch of streams in line with your suggestion @Karl Palmskog
And as a follow-up, I've created the "Coq users" stream and added it to the default streams for new users (with "Announces").
very nice, that helps a ton for me personally on how to use the chat, and also hopefully for new users
now if we only can convince @Cyril Cohen to rename "Mathematical Components Library" to just "math-comp users"...
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.
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
Cyril Cohen renamed stream Announces to general.
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
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.
This might make sense actually. If people don't know where to ask, they can ask here. We can see how it turns out.
in this case I would call it "miscellaneous", but sure, we can wait and see
So one can move a discussion to anotherbtopic, but not to another stream....
Turns out that this feature is less powerful than the equivalent in Discourse then! (But in Discourse, it is reserved to admins.)
@Théo Zimmermann I think it should be...
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
No, I don't think there are too many streams. I appreciate being able to separate devs from users discussion in high traffic projects.
I meant, at a future point in time...
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.
@Christian Doczkal you are right, I will ask. I know they were pretty reactive in the integration of my PR modifying gitter import though ;)
What do you think, should we have a stream about continuous integration issues or only a coq devs & plugin devs topic?
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.
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)?
@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
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: May 31 2023 at 10:01 UTC