waiting for CI

Stream: general

[Joachim Breitner]

Waiting for CI to finish is annoying. (Not a useful post, of course)

[Yakov Pechersky]

CI wait time just gives me a good chunk of time in which to start writing new PRs!

[Mauricio Collares]

When support for squashing and delegation gets added to GitHub merge queues, this will be a thing of the past! Squashing is certainly on their roadmap, but I don't know if delegation is too.

[Julian Berman]

Will it? The time to run CI is still pretty long regardless, no? I don't send as many PRs as I wish I did but in other similar situations I sometimes use e.g. gh run watch 123456789 && notify "CI is done, get back to work"

[Joachim Breitner]

Auto-merge once CI is green (whether with bors, mergify or GitHub native) makes it much less annoying, however. Having to manually check the status is silly. Once that eventually is fixed one way or another, there are significantly less cases, I think, where one might actually wait for CI.

[Eric Rodriguez]

oh, I see you're in the conversation Joachim, but for all others this is being tracked by #11609

[Yury G. Kudryashov]

If you have a few independent prs then you just switch to another branch.

[Yury G. Kudryashov]

If you have a few independent prs then you just switch to another branch.

[Yury G. Kudryashov]

And in many cases you don't need to wait for tests and lint.

[Joachim Breitner]

You mean saying bors mergebefore lint is green? Isn't that pretty bad style and can cause whole batches to fail and thus annoy everyone else? Or is that ok, as bors will retry and bisect and nobody will mind?

[Eric Wieser]

Didn't we very recently configure bors to wait for CI to go green anyway?

[Eric Wieser]

Worst case scenario is you annoy everyone else by making them wait for a rebuild after the first build falls

[Eric Rodriguez]

Eric, that's the PR that I linked beforehand - there's issues there

[Yury G. Kudryashov]

Sorry, I was reading in a bus and misinterpreted the issue. I thought that you're waiting for oleans to continue working on the branch.

[Yury G. Kudryashov]

I usually don't care how soon (± 5h) an approved commit will be merged.

[Stuart Presnell]

I get an email notification when one of my PRs fails CI (I don’t know if this is the default or if I’ve set something to do this). Is there a way to get a notification when CI passes?

[Moritz Doll]

@Stuart Presnell go to settings->notifications->actions and disable "Send notifications for failed workflows only"

[Stuart Presnell]

Hmm, now I'm getting an email for each successful stage of CI (the Dependent Issues workflow, the linter self test, etc.) which is much more detail than I want. Is there a way I can set things up so I only get a notification when the CI has finished running, to tell me whether it succeeded, failed, or was cancelled?

[Mauricio Collares]

If there's no better option, you can always set up email filters to ignore all but the Build and Lint steps

[Mauricio Collares]

Mauricio Collares said:

When support for squashing and delegation gets added to GitHub merge queues, this will be a thing of the past! Squashing is certainly on their roadmap, but I don't know if delegation is too.

If I understand correctly, GitHub merge queues now support squashing according to the screenshot in https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue. I don't know what the commit message is in this case, and I don't think GH merge queues support delegation yet.

[Arthur Paulino]

Interesting. I think it makes (or will eventually make) bors obsolete?

[Eric Wieser]

Right now we're on the wait-list for that feature, so can't even try it out yet

[Mauricio Collares]

They prioritize projects with a high number of merged PRs and mathlib hasn't had a PR merged to master in two years ;)

[Eric Wieser]

I'm sure we could send a politely-worded email to request a boost, but I don't think the maintainers have discussed this; I only signed us up for the beta so that we had a head start when the discussion eventually happens

[Anne Baanen]

Do GitHub merge queues have a bors d+ equivalent?

[Eric Rodriguez]

seems there is for "bors d+, wait for build merge" (here) whilst I can't see one for "do minor changes then merge"

[Mauricio Collares]

I filed a feature suggestion at https://github.com/github/feedback/discussions/14699

[Yaël Dillies]

Note that this could be a security breach. "Do something small and merge" puts a lot of trust on the collaborator, who could upturn the entire library as "something small" before merging.

[Eric Rodriguez]

yes, this does seem like the sort of thing only a project that isn't executable could do

[Yaël Dillies]

Hence not having it might be an intentional safety from Github, but I would be glad to be proven wrong.

[Eric Wieser]

This feels like something for a custom workflow to handle

[Eric Wieser]

That custom workflow can parse a user comment / some mathlib-specific trust data, and then fire off the github merge queue

[Rémi Bottinelli]

I was wondering if I could bors r+ before waiting for my PR to build successfully, and a search directed me here. Can I?

[Junyan Xu]

Since #bors is idle right now, I think you can just do it.

[Mauricio Collares]

Mauricio Collares said:

When support for squashing and delegation gets added to GitHub merge queues, this will be a thing of the past! Squashing is certainly on their roadmap, but I don't know if delegation is too.

https://github.blog/changelog/2023-02-08-pull-request-merge-queue-public-beta/