awaiting-zulip PRs not yet awaiting Zulip

Stream: mathlib4

[Yaël Dillies]

I have noticed some issue with the current usage of awaiting-zulip: Reviewers tend to mark a PR awaiting-zulip as soon as they expect the PR author to create a discussion on Zulip, rather than when that discussion is actually created. This means that plenty of PRs tagged awaiting-zulip are actually awaiting an action from the author, rather than from the community.

[Yaël Dillies]

For example, #19872 was tagged awaiting-zulip even though the relevant Zulip discussion didn't exist until five minutes ago.

[Yaël Dillies]

The description of the awaiting-zulip tag makes it quite clear that there is an expectation that the Zulip discussion already exists:

There is a Zulip discussion; the author should await and report/implement the decision reached there

[Yaël Dillies]

Could I please ask reviewers to only use awaiting-zulip once there's a clearly signposted Zulip discussion linked to from the PR? This will ensure that labels stay actionable.

[Yury G. Kudryashov]

IMHO, explicitly asking the author to start a discussion is enough to use this label.

[Yury G. Kudryashov]

OTOH, I understand why you prefer to have awaiting-author, not awaiting-zulip in this case.

[Yury G. Kudryashov]

What about the following?

• We add a bot that adds awaiting-zulip whenever the PR description has - [ ] Zulip discussion: link
• The same bot marks this TODO item as done whenever the Zulip discussion is marked as resolved.
• If a reviewer requests the author to start a Zulip thread, they use awaiting-author and post a standard message (we can have it in saved responses).

[Yury G. Kudryashov]

Another option for item 3: if a reviewer adds awaiting-zulip but there is no - [ ] Zulip discussion: in the description, then a bot posts a standard message and changes the label to awaiting-author.

[Yury G. Kudryashov]

Of course, someone has to write this bot.

[Eric Wieser]

Is a convention of "apply both awaiting-author and awaiting-zulip" sufficient here?