Create a private stream

Stream: new members

[Vasily Ilin]

Do ordinary members of Lean Zulip not have permission to create their own (private) stream? I'm trying to collaborate with multiple people, and so want to create a stream.

[Yaël Dillies]

I think it got disabled because people were accidentally creating streams instead of new topics. You can have private group messages.

[Vasily Ilin]

I see. Thanks!

[Johan Commelin]

@Vasily Ilin If private group messages is too disorganized, please ping the @maintainers and we can make a stream for you.

[Patrick Massot]

I think we should create this stream right away. We know from the perfectoid project that having all discussions in private messages isn't convenient, even with a small team.

[Vasily Ilin]

@maintainers , can I please get my own stream? We'll be working with a team of 7 students, learning Lean, hopefully working up to formalizing something new. Thank you!

[Patrick Massot]

Could you provide a stream name?

[Vasily Ilin]

Name: University of Washington. @Patrick Massot

[Patrick Massot]

Done.

[Kevin Buzzard]

FWIW there's an Imperial College private stream but nowadays we just use a discord server.

[Vasily Ilin]

@Patrick Massot , could I please get the permission to generate an invite link to the channel?

[Patrick Massot]

I don't think such a thing exists. You can subscribe people to this stream after they have created an account.

[Vasily Ilin]

So for a class with n students, I would need to copy-paste n usernames? Oh God

[Eric Wieser]

Can you click the "invite users" link under the cog at the top right?

[Vasily Ilin]

I can
image.png

[Vasily Ilin]

But I wish I could generate an invite link

[Eric Wieser]

Can't you just paste the list of emails?

[Eric Wieser]

That way you can also encourage students to use their academic email addresses

[Eric Wieser]

(for what it's worth, that option is grayed out for me too)