What to do with PRs awaiting-review with red CI

Stream: general

[Arthur Paulino]

If you don't mind running a bot on your PC, it should be pretty straightforward to build a Python script that checks for your red PRs periodically. And if the community agrees, building a globally alerting bot should be straightforward as well (I can help with that)

[Johan Commelin]

Personally, I think there are now so many PRs that I only have time to look at PRs with a green CI checkmark (barring occasional exceptions). In particular, I wouldn't mind strong bot flags that turn PRs with failing CI back in the realm of the PR author. I'm happy to have an even stronger label that authors can apply sparingly to override the broken-CI-bot to kick their PR on the review queue nonetheless.

[Eric Rodriguez]

another one that always bites me is when there's magically a merge conflict, and I have no clue till a week later or so. it's also annoying that gh pr status (from the github cli) doesn't show labels

[Eric Rodriguez]

but mercifully it does show all your PRs and whether CI is passing/failing, so it's a nice tool to run randomly

[Scott Morrison]

I think the correct mechanism to handle "my PR is broken but I'd like a review anyway" is to post a message on #PR reviews!

[Arthur Paulino]

@Johan Commelin if labeling PRs is part of the scope of the lean-community bot, maybe it could be extended to change such labels back to awating-author?

[Johan Commelin]

I have no idea how to do that, but it sounds reasonable to me. Of course, that's just my opinion. It would be good to hear from a lot of others as well. Including a bunch more @maintainers

[Ruben Van de Velde]

While we're here, automatically adding awaiting-review to new PRs when I forget would be neat

[Arthur Paulino]

@Ruben Van de Velde how to conclude that the PR is indeed ready for review?

[Damiano Testa]

I do not really know whether there is a flow associated to awaiting-CI, but that label I would interpret as: "I am happy with the current version and would tag it awaiting-review, provided it passes CI". If this is not the current behaviour, then maybe it could become that, instead? I.e., the bot could check that PRs labeled awaiting-CI are "green" and could remove awaiting-CI and replace it by awaiting-review?

[Johan Commelin]

So far, I've mostly treated it as "Warning, do not merge right now! Please review/merge in a couple of hours".

[Damiano Testa]

Ah, I was looking at it from the perspective of the author, not of the reviewer!

[Damiano Testa]

Actually, Johan, I realize now that what you are saying also applies to the author. Anyway, maybe there should be an awaiting-review-if-green-tag.