A complaint

Stream: general

[Panda Coder]

Dear moderators.

Hi About 10-15 people were having a discussion about formalising physics in Lean. And then someone moved the discussion to a hidden channel so no-one can see it. (It will not appear in when searching for it in the search bar.) And then subscribed myself and one other person to that channel.

This evening I spent several hours crafting a post which I posted there only to realise this is now a hidden channel so it was a big waste of my time. I only realised it was shadow banned by logging into a new account to check.

That is fine. I understand that maybe it is annoying if notifications appear on discussions they are not interested in. But please next time someone does this can they make it clear that they have moved it from a public channel to a hidden channel. Because this is more-or-less the same as shadow banning discussions which is not very cool.
A more sensible solution would be to move it to another public channel in which people can turn off notifications.

This is also counter productive because by hiding discussions, it means people will re-implement things several times over which is a waste of brain power for the world.

Thanks for listening.

[Jason Rute]

Is the channel #Natural sciences hidden from you or private, or are you just not subscribed? I do agree it was confusing for me also since I wasn’t subscribed, but it might just be a case of someone not realizing that channel isn’t one people are subscribed to by default.

[Jason Rute]

Anyway, I’m subscribed to it now. :)

[Bulhwi Cha]

Let's make #Natural sciences a public channel.

[Utensil Song]

The default channel for new users are as follows:

image.png

There are many interesting channels you may find out by using the "Browse n more channels" at the left bottom corner of the web UI to subscribe to more channels.

Actually, when these topics are moved to separate channels, they are more discoverable in the long run.

[Kyle Miller]

@Bulhwi Cha It's already a public channel.

[Utensil Song]

I'm happy with opt-in in general, and I'm afraid that opt-out suggested by Panda would be too noisy for many. But there is indeed an issue of discoverability, namely:

A lot of meta programming discussions happen in other channels simply because #metaprogramming / tactics is not in default channels, and one might wish to find all related discussions there. Likewise for #Program verification . These channels including #Natural sciences , due to their discoverability, very few discussions about these topics actually took place in these channels.

[Utensil Song]

image.png

#Natural sciences is public, but not web public. A similar discussion happened before for #FLT, then it was decided to change to web-public, the benefit seems to be better discoverability without registering an account, and maybe search engine friendly?

[Bulhwi Cha]

Ah, I confused "public" with "web-public."

[Bulhwi Cha]

Let's make it a web-public channel.

Screenshot_20240618_135531_Firefox.jpg

[Bulhwi Cha]

Utensil Song said:

the benefit seems to be better discoverability without registering an account, and maybe search engine friendly?

I don't think Zulip messages are discoverable through a search engine even if these messages are in a web-public channel, which is unfortunate.

[Patrick Massot]

I am really sorry about this issue. I had no idea this channel was hard to find.

[Patrick Massot]

I am not sure I see the point of having channels that are opt-in for new users.

[Kim Morrison]

Patrick Massot said:

I am not sure I see the point of having channels that are opt-in for new users.

Surely you mean the opposite? I would not want to subscribe all new users to nightly-testing. :-)

[Patrick Massot]

Yes I meant opt-out, sorry

[Patrick Massot]

And indeed I forgot the technical channels. Those should be opt-in

[Yaël Dillies]

There are also channels like #mathlib documentation that are so cross-sectional that I don't see their point

[Eric Wieser]

That one was created by accident I think

[Kevin Buzzard]

But just to be clear to Panda Coder -- this was not an attempt to stop the conversation! Just the contrary -- it was to stop it continuing in a channel which the lean developers use to discuss issues with core lean, not general lean projects. We're sorry that you interpreted it as some kind of ban but I would urge you to continue the conversation! (in the appropriate channel).

[Joseph Tooby-Smith]

I would also like to see #Natural sciences made web-public. I have, in the past, tried to send people without Zulip accounts posts there - which naturally doesn't work.

[Joseph Tooby-Smith]

(That said: Not sure if there is an issue making a channel suddenly web-public. People may have posted there things they would not want on a channel which is web-public.)