Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: stream events


view this post on Zulip Notification Bot (May 17 2020 at 13:38):

Stream created by Jalex Stark.

view this post on Zulip Scott Morrison (May 17 2020 at 13:46):

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

view this post on Zulip Jalex Stark (May 17 2020 at 13:59):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:01):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:04):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:05):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:06):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:08):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:09):

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.

view this post on Zulip Scott Morrison (May 17 2020 at 14:09):

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.

view this post on Zulip Jalex Stark (May 17 2020 at 14:10):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:10):

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.

view this post on Zulip Scott Morrison (May 17 2020 at 14:11):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:11):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:12):

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.

view this post on Zulip Jalex Stark (May 17 2020 at 14:12):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:12):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:12):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:13):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:13):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:13):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:13):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:13):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:13):

right

view this post on Zulip Scott Morrison (May 17 2020 at 14:14):

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

view this post on Zulip Scott Morrison (May 17 2020 at 14:14):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:14):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:14):

but yeah I haven't collected strong evidence for that

view this post on Zulip Scott Morrison (May 17 2020 at 14:15):

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.

view this post on Zulip Johan Commelin (May 17 2020 at 14:18):

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

view this post on Zulip Jalex Stark (May 17 2020 at 14:19):

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"?


Last updated: May 09 2021 at 21:10 UTC