## Stream: metaprogramming / tactics

### Topic: stream events

#### Notification Bot (May 17 2020 at 13:38):

Stream created by Jalex Stark.

#### Scott Morrison (May 17 2020 at 13:46):

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

#### Jalex Stark (May 17 2020 at 13:59):

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

#### 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

#### 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

#### Jalex Stark (May 17 2020 at 14:05):

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

#### 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

#### Jalex Stark (May 17 2020 at 14:08):

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

#### 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.

#### 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.

#### 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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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

#### Scott Morrison (May 17 2020 at 14:12):

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

#### Scott Morrison (May 17 2020 at 14:12):

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

#### Scott Morrison (May 17 2020 at 14:13):

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

#### Jalex Stark (May 17 2020 at 14:13):

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

#### Scott Morrison (May 17 2020 at 14:13):

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

#### 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)

#### 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.

right

#### 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.

#### Scott Morrison (May 17 2020 at 14:14):

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

#### Jalex Stark (May 17 2020 at 14:14):

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

#### Jalex Stark (May 17 2020 at 14:14):

but yeah I haven't collected strong evidence for that

#### 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.

#### 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

#### 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