CI Bot comment for merge conflicts

Stream: mathlib4

[Robin Carlier]

This may be github skill issues on my end, but I don’t get any kind of notification when the leanprover-community-bot-assistant adds the "merge conflict" label on my PRs, but I do get notifications whenever the various bots comments things on the PR.
Would it be hard to make the bot comment as well as adding the label?

[Michael Rothgang]

I think github doesn't send notifications for this (so you're not missing anything). My personal hack is to check the overview of all my pull requests often enough (using e.g. https://jcommelin.github.io/queueboard/triage.html?search=grunweg&sort=9-desc#all; replace "grunweg" in the URL by your github username).

[Michael Rothgang]

Making the bot comment: that should be doable; let me ping our CI experts @Damiano Testa and @Bryan Gin-ge Chen.

[Damiano Testa]

This seems more like a preference that GitHub should give each user (and I do not think that it does). Right now, there is no mathlib action that directly sends an email to the author and I do not know if even that would be easy. Besides, I would also not know how to make it configurable, so that each author can choose whether they want to receive emails or not for merge-conflicts.

[Damiano Testa]

In conclusion, my impression is that this is something that I would like to have as an option, but I suspect that it would have to be a github offer, rather than a mathlib one.

[Michael Rothgang]

I fully agree that "receive an email if there is a merge conflict" should be opt-in.

I wondering about something else, though: can the merge conflict bot add a comment "this PR has a merge conflict" (or slightly more creative) when it adds the label? That implies a github notification for those who care about it.
Writing this, I'm not sure if the bot should do so - but this is very feasible, right?

[Robin Carlier]

I agree that in the best of worlds, this is an option that should come from github. But, as this seem not to be the case, can’t we just ask the bot to comment on the PR? We have already a few bots that comment on PRs (dependabot, etc..), so this seems like a good middle ground?

[Robin Carlier]

well, @Michael Rothgang beat me to it.

[Damiano Testa]

The action that mathlib uses does have the option of adding a comment to the PR, beside adding the label.

[Damiano Testa]

Before changing that, I would still like to see some support for the extra emails that everyone will receive.

[Bryan Gin-ge Chen]

The merge conflict workflow we're using does actually allow for commenting on the PR. If this is desired I can add this.

(Adding this shouldn't increase the token usage of the bot by too much, and though we used to have problems with this bot using too much quota it seems the last sequence of failures was several months ago even though we didn't change anything and the number of open PRs has only increased...)

edit: ah, while I was investigating this, Damiano posted the same thing...

[Damiano Testa]

If quota becomes a problem, we can also add the comment in a separate action that is triggered by the label. That could use a different quota, right?

[Damiano Testa]

#22833

[Damiano Testa]

/poll Do you want to receive email notifications when a PR acquires merge-conflicts?
Yes
No
Indifferent

[Julian Berman]

Does the bot we use set X-Github-Reason headers, or an equivalent? This is a header GitHub typically sets which lets one filter out noisy email notifications (see here)

[Julian Berman]

Oh I misread, it'd be a comment? Then no presumably

[Damiano Testa]

I don't know about X-Github-Reason (in the sense that I never heard about it!), but indeed the bot will simply post a comment to the PR and GitHub already has its own mechanism for notifying when a comment is added to a PR.

[Damiano Testa]

Note that this is all speculation, since it has not been tested: I learned to not trust that CI will do what you think it will, unless you test it every single time that you use it.

[Damiano Testa]

It seems like there is a majority of preferences for adding a comment: I'll wait a little bit longer before removing the awaiting-zulip label on the PR, but it looks like this is a direction that most people either want or do not especially care about.

[Damiano Testa]

I've removed awaiting-zulip, as the poll indicates that more people would be happier if we went forwards with this.

[Michael Rothgang]

I have maintainer merge'd this PR, as the implementation looks straightforward.