Changes to the #queue

Stream: general

[Michael Rothgang]

Should the pull request template be updated to remove mentions of the awaiting-review label?

[Shreyas Srinivas]

1. Is there a discussion thread for this?
2. One issue that is due to the large number of PRs on queue and limits on maintainer time is, PRs quickly get merge conflicts before they ever get into the first page. After removing the merge conflict, they have to start at the back of the line again. This leads to many PRs never getting to the front at all. Can the PRs in queue be sorted in a way that handles this issue better?

[Notification Bot]

2 messages were moved here from #announce > Changes to the #queue by Riccardo Brasca.

[Riccardo Brasca]

Here is the discussion thread :)

[Dagur Asgeirsson]

I think a lot more PRs get merged from the last page of the queue than the first :)
A good strategy to get your PRs merged is to split them up into many small pieces, and not change too many files in one PR. That way, each individual PR is less likely to get merge conflicts (and if it does, it's usually straightforward to fix), and is less overwhelming to review, which leads to quicker merges

[Ruben Van de Velde]

And a reviewer might have time / energy to look at one of your four (say) smaller PRs even when they wouldn't have time to review the bigger one

[Shreyas Srinivas]

Sometimes this is possible. But sometimes you have PRs like my recently merged chore PR which namespaced Vector. This was necessarily going to affect every single place vector was called, even if in small ways. It moved in and out of merge-conflict very quickly over June.

[Andrew Yang]

It's true that shorter PRs get reviews easier, but the system is not rewarding such behaviour when the speed up is sub-linear and the PRs are sequential (which is often the case IMO).

[Johan Commelin]

Michael Rothgang said:

Should the pull request template be updated to remove mentions of the awaiting-review label?

Done

[Johan Commelin]

Shreyas Srinivas said:

Sometimes this is possible. But sometimes you have PRs like my recently merged chore PR which namespaced Vector. This was necessarily going to affect every single place vector was called, even if in small ways. It moved in and out of merge-conflict very quickly over June.

For such PRs, it is strongly encouraged to coordinate on zulip and loudly announce when the PR is ready for review.

[Shreyas Srinivas]

I kinda did that a month ago and then one-two weeks ago after removing a merge conflict. It is merged now, but that happened yesterday after almost a whole month. I had practically given up on it, and it just came up again, and the merge conflict turned out to be easy to fix.

[Riccardo Brasca]

We are sorry for that. Please don't hesitate to post multiple reminds for PRs like that (I mean rather easy to review that get a lot of merge conflicts).

[Geoffrey Irving]

Why is awaiting-CI not automatic? I.e., one could have the convention that if CI is running, one is never sure that the PR will pass CI.

[Yury G. Kudryashov]

Andrew Yang said:

It's true that shorter PRs get reviews easier, but the system is not rewarding such behaviour when the speed up is sub-linear and the PRs are sequential (which is often the case IMO).

I often create small PRs while working on a larger goal (create a new branch, cherry-pick some changes, open a PR, switch back, continue working). This way auxiliary lemmas start going through review while the main result is not ready yet.

[Yaël Dillies]

Geoffrey Irving said:

Why is awaiting-CI not automatic? I.e., one could have the convention that if CI is running, one is never sure that the PR will pass CI.

In practice that's not really the case, and PRs which don't pass CI are not on #queue anyway. awaiting-CI is more like "I expect to need several rounds of fixes"

[Johan Commelin]

I use awaiting-CI when I bors d+ and CI isn't ready yet, as a clear flag that the PR author shouldn't bors r+ before a :check: for CI.

[Yury G. Kudryashov]

Why don't we use auto-merge-auto-CI in this case?

[Kevin Buzzard]

I thought that bors wouldn't merge anything which didn't have a green tick anyway. Hence I've never used the awaiting-CI tag because I couldn't see the point. If I think something needs several rounds of compilation then I just mark it WIP, if I hope it's going to compile I just mark(ed) it awaiting-review.

[Johan Commelin]

bors will happily queue a PR that still has CI running :orange_circle:

[Kevin Buzzard]

I thought that this used to be the case, but when it merged something which had CI running the maintainers changed CI to stop this happening. I could be wrong though, and don't know anything about CI, and certainly don't want to check this by experimenting :-)

[Michael Rothgang]

#14609 ensures github workflows don't create the awaiting-review label any more

[Jireh Loreaux]

@Kevin Buzzard you can definitely put stuff on the bors queue while CI is running. I did it just the other day and then had to take it off again.

[Kevin Buzzard]

I tagged my PR yesterday with awaiting-CI just in case I was wrong :-) (it removed an import so there was a risk :-) )

[Yaël Dillies]

Could we also make RFC PRs show up on #queue regardless of whether they pass CI or not? The point of a RFC is to get early feedback on whether an idea is worth implementing or not

[Yury G. Kudryashov]

I don't think that github search language allows logical operations.

[Kim Morrison]

In any case RFCs perhaps deserve threads in the PR reviews channel?

[Peter Nelson]

in #14781 (which depends on #14721), I added the 'blocked-by-other-PR' label only to have the bot remove it. What did I do wrong?

[Bryan Gin-ge Chen]

The bot manages that tag by parsing the PR comment for lines that look like this:

- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

So if you add the following to the bottom of the PR comment in #14781, the tag will be automatically added and then removed when #14721 gets merged:

- [ ] depends on: #14721

[Bryan Gin-ge Chen]

Ah, except that we've been running into API limits with the bot recently, so it could be a while before the bot gets around to it...