Zulip Chat Archive

Stream: general

Topic: What to do with PRs awaiting-review with red CI

Arthur Paulino (Apr 27 2022 at 11:14):

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 (Apr 27 2022 at 11:18):

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 (Apr 27 2022 at 11:36):

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 (Apr 27 2022 at 11:36):

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 (Apr 27 2022 at 11:39):

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 (Apr 27 2022 at 11:50):

@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 (Apr 27 2022 at 11:51):

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 (Apr 27 2022 at 12:07):

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

Arthur Paulino (Apr 27 2022 at 12:27):

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

Damiano Testa (Apr 27 2022 at 12:30):

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 (Apr 27 2022 at 12:33):

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

Damiano Testa (Apr 27 2022 at 12:34):

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

Damiano Testa (Apr 27 2022 at 12:35):

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.

Last updated: Aug 03 2023 at 10:10 UTC