Rant

Stream: general

[Joachim Breitner]

Hmm, quite annoying when I think my PR is ready for review, and I have labeled at that, and I’m patiently waiting for a review only to notice a few days later that CI wasn’t actually happy, and nobody is likely to look at it, and I only notice if I happen to check my open PRs. I wonder how best to avoid that? Maybe a bot that looks at PRs that are labeled awaiting-review, but CI is red, and that comment & relabel the PR? Or maybe do that if nothing else is happening for a few days (no need to have bots annoy us when there is activity)?

[Yaël Dillies]

You can look at either of your Github branches and of your open PRs.

[Eric Wieser]

You can setup github to send you emails when CI fails; I think this might even be the default

[Johan Commelin]

@Joachim Breitner I'm sorry to hear that. I agree this can be annoying, because it's sometimes not clear where the responsibility for a PR lies, and so they can fall through the cracks.
I like your idea of a bot that draws some attention to such PRs.

[Joachim Breitner]

(oh, and I hope it’s not negative to call this “rant”, I’m not blaming anyone or such. It’s just nice to speakout what is bothering a bit.)
I think I might even get these emails, but they are also sent for PRs that I haven’t submitted for review, or for cancelled builds, so most of them are noise and that’s why I probably miss the relevant one.

[Joachim Breitner]

Indeed, clear responsibilities are probably a good idea. Assuming we only expect reviews on CI-green PRs by default (maybe there is a separate way to indicate “this doesn’t pass yet, and I know, but I still would like a review”), then that label plus a red CI is an invalid state that could be reconciled by a bot, by assigning to the user? But I’m worried it might cause too much noise…

[Damiano Testa]

There is also a slight difference between "red because mathlib did not build correctly" and "red but the olean's are available". I would say that flagging the first one is more important than the second one.

[Arthur Paulino]

If you look at #queue, it's just a fixed URL with some filtering parameters. I see two options:

• Creating a #broken_queue (or something along those lines) which points to such PRs
• You can create a URL of your own with red PRs labeled as awating_review and include author:joachim as a parameter so you can see your broken PRs from time to time

[Joachim Breitner]

I do look at my PRs from time to time, that’s how I find these stuck PRs right now. But I’m spoiled and lazy, and would like someone (better something) alert me when I made a mistake :-)