stream events

Stream: metaprogramming / tactics

[Notification Bot]

Stream created by Jalex Stark.

[Scott Morrison]

I think we might be going overboard creating new streams here.

[Jalex Stark]

I agree, I think new streams should have justifications which I haven't provided

[Jalex Stark]

my thought here is something like:
we have conversations about questions like "what would it take to write a tactic that does blah" which don't have enough "gravitational pull" to connect to each other

[Jalex Stark]

for example here mario said (and we agreed) that it was hard to find examples of "tactic specs"
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Effectiveness.20as.20a.20computer.20algebra.20system.3F/near/197828817
I think i have seen conversations get close to writing a tactic spec, except that the people in the conversation don't know that going all the way is useful

[Jalex Stark]

I think collecting such conversations in a stream makes discoverability later much easier

[Jalex Stark]

even if the "collecting" is just an archival process done by e.g. me, which is also how sort of how the "organizing online events" stream is being used right now

[Jalex Stark]

@Scott Morrison are you worried about a mechanism by which conversations become instead harder to find?

[Scott Morrison]

Yes. The problem is that new streams are mostly invisible. People don't get subscribed to them automatically, so unless they notice the "announce" message and actively subscribe then they never see the subsequent conversations.

[Scott Morrison]

It's even worse for new users who arrive after the creation of the stream, unless we change the organisation settings to automatically subscribe new users to it.

[Jalex Stark]

I see. So one could start an "archival" stream, and then it quietly turns into a place where a small set of users have active and useful discussion, but the rest of the server doesn't know about it

[Scott Morrison]

As an example, I wasn't aware of the "Is there code for X?" stream for months after it was created, even though I was otherwise actively reading zulip, and would have liked to follow it.

[Scott Morrison]

I only ever noticed it because someone posted a link to a discussion there back in general.

[Scott Morrison]

It's also not possible to move topics between streams, so having more top level streams actually makes it harder to keep things organised.

[Scott Morrison]

Unless everyone is quite disciplined about putting things in the right places, we'll end up with topics split between general and the named streams.

[Jalex Stark]

right, i think i have reached for the "move topic" tool a few times and been disappointed

[Scott Morrison]

I think streams work great for "private" discussions for working groups.

[Scott Morrison]

(e.g. a group of students at the same university)

[Scott Morrison]

(or, for that matter, the Lean 4 team)

[Jalex Stark]

the type theory stream is also sort of a private discussion group

[Scott Morrison]

streams are good for _private_ conversation, but I think a bad idea for public conversation.

[Jalex Stark]

(in that it's never going to be interesting to more than say 10% of the population here)

[Scott Morrison]

Well --- the type theory stream was created because some people didn't want to see any of that.

[Jalex Stark]

right

[Scott Morrison]

Now, that may be the case for metaprogramming / tactics, but I haven't seen evidence of that so far.

[Scott Morrison]

(but I'd be the wrong person to notice...)

[Jalex Stark]

well i sometimes hear kevin saying he's not interested in working with the meta keyword

[Jalex Stark]

but yeah I haven't collected strong evidence for that

[Scott Morrison]

I assure you that even if @Kevin Buzzard isn't planning on spending lots of time writing tactics soon, he remains interested in development of new tactics.

[Johan Commelin]

Scott Morrison said:

It's also not possible to move topics between streams, so having more top level streams actually makes it harder to keep things organised.

Note that admins can do this... but of course that's still a nuisance

[Jalex Stark]

on meta didn't we have an open question "are there any tasks the server would be better at if we gave more people admin"?