streams

Stream: general

[Kevin Buzzard]

Pretty much every public stream we have here either has the property that it has 1000+ subscribers (including #rss, which I suspect most people have no interest in) or less than 100 (including #Geographic locality , which is perhaps a stream that more people would be interested in). What is going on here? When a new user appears, which streams are they automatically subscribed to? I had no idea that the #Is there code for X? stream existed until just now. Is it possible to change it so that a new user does not get subscribed to #rss but does get subscribed to #Geographic locality ?

[Kevin Buzzard]

It is also often the case that new users appear and instantly ask "is representation theory / graph theory / ... in Lean?".

[Kevin Buzzard]

To everyone: clicking on the cog to the right of the word "STREAMS" in the left hand pane shows you a list of all public streams.

[Mario Carneiro]

The default streams are announce, general, maths, new members, rss

[Kevin Buzzard]

How about we add Geographic locality? It's super-low-traffic and people might be interested to hear about local Leaners. And should we remove rss?

[Sebastian Ullrich]

This really is a misfeature of Zulip imo, at least for this kind of communities. Just subscribe everyone to everything (maybe opt-out per stream) and let them mute things they don't care about...

[Kevin Buzzard]

e.g. if a random Cambridge UK undergrad subscribes then they will see that there is this weekly Cambridge meeting, and one could imagine that more such meetings could happen organically if a couple of people from the same uni appear.

[Mario Carneiro]

what is the story for discoverability of non-default streams though? I would rather sign everyone up for everything and let them pick what is too chatty

[Kevin Buzzard]

One way of discovering them is for Patrick to randomly mention one when talking about Bolzano-Weierstrass.

[Mario Carneiro]

in theory you can catch the stream creation event in #announce but how often is that?

[Sebastian Ullrich]

We could of course force-subscribe existing users to streams of general interest retroactively...

[Kevin Buzzard]

Why not subscribe everyone to Geographic locality and see what happens?

[Mario Carneiro]

I'm pretty sure nothing will happen

[Mario Carneiro]

unless there is traffic on the stream no one will even notice

[Kevin Buzzard]

Someone new will look at it, post where they are, and then maybe a bunch of people will. I think that local communities are really important.

[Sebastian Ullrich]

Actually I feel like most of Zulip's defaults are messed up... getting notifications for every message in a stream should be opt-in, not opt-out (mute).

[Kevin Buzzard]

Look at all that topos stuff which the Cambridge people have done. If some new Cambridge kid appears, some smart UG, they play with Lean a bit and then maybe they go on to other things, but then if they notice the meetings they might show up there.

[Mario Carneiro]

certainly this is a problem for Geographic locality since you probably want to mute all topics except your locality

[Kevin Buzzard]

But this is a very low traffic stream.

[Sebastian Ullrich]

That's another missing feature, unmuting a topic in a muted stream

[Sebastian Ullrich]

If I've ever forgotten to reply to a discussion without someone tagging me, that's exactly what happened...

[Mario Carneiro]

I added geographic locality and is there code for X to default streams, but I haven't done any retroactive signups

[Sebastian Ullrich]

Following topics might be resolved by https://github.com/zulip/zulip/issues/12309

[Sebastian Ullrich]

Looks like the Rust and Julia people are flagging many issues in that direction, e.g. https://github.com/zulip/zulip/issues/11864

[Kevin Buzzard]

Why not retroactive geographic locality? It will just randomly appear on the left for 1000 people but that won't cause some huge disruption, especially as it's quiet.

[Mario Carneiro]

no reason, I just don't want to look into it right now

[Mario Carneiro]

it sounds like a lot of work

[Kevin Buzzard]

Oh!

[Kevin Buzzard]

Sorry, I thought it was just a tick in a box.

[Mario Carneiro]

maybe it is, I will check tomorrow

[Kevin Buzzard]

Thanks.

[Sebastian Ullrich]

Urghh. It's trivial to subscribe everyone to a new stream, but not to an existing one...

[Sebastian Ullrich]

Ok, looks like that worked.

$ curl -sS https://leanprover.zulipchat.com/api/v1/users -u $ZULIP_EMAIL:$ZULIP_API_KEY | jq -c '.members | map(select(.is_active) | .email)' | curl -sS https://leanprover.zulipchat.com/api/v1/users/me/subscriptions -u $ZULIP_EMAIL:$ZULIP_API_KEY --data-urlencode subscriptions='[{"name": "Geographic locality"}]' --data-urlencode principals@-

[Sebastian Ullrich]

image.png

[Sebastian Ullrich]

And @Kenny Lau even pinged all 1732 members already, just in time

[Kenny Lau]

so zulip has an unsecure api

[Sebastian Ullrich]

Do you see the ZULIP_API_KEY there?

[Marc Huisinga]

do you get an email when you get subscribed to a stream?

[Kevin Buzzard]

I will run some Lean stuff over the summer. It was supposed to be at Imperial but now we have this lockdown I suspect I'll have to run it online. When it's all set up and I have something to offer, I can add The Internet

[Sebastian Ullrich]

Marc Huisinga said:

do you get an email when you get subscribed to a stream?

I hope not, I've never gotten an email from Zulip except for "OMG you're using a new PC!". But otherwise I'm sure people will let us know very soon.

[Gabriel Ebner]

I've only got a private message from the notification bot that Sebastian has personally invited me to the stream.

[Erika]

hello, I'm here because of an email about getting subscribed

[Kevin Buzzard]

oops

[Marc Huisinga]

oh no

[Sebastian Ullrich]

Yeah, apparently you do get an email if you're not active... but the same would have happened with a new stream, I don't see how to avoid it

[Sebastian Ullrich]

Well, that's a lot more positive than negative feedback than I feared!

[Kevin Buzzard]

Yeah I think it worked out quite nicely! Thanks Sebastian.