Zulip Chat Archive

Stream: general

Topic: waiting for CI


Joachim Breitner (Feb 10 2022 at 17:15):

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

Yakov Pechersky (Feb 10 2022 at 18:39):

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

Mauricio Collares (Feb 10 2022 at 19:51):

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 (Feb 10 2022 at 19:56):

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 (Feb 10 2022 at 20:38):

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 (Feb 10 2022 at 20:40):

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

Yury G. Kudryashov (Feb 10 2022 at 20:58):

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

Yury G. Kudryashov (Feb 10 2022 at 20:58):

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

Yury G. Kudryashov (Feb 10 2022 at 20:58):

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

Joachim Breitner (Feb 10 2022 at 21:37):

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 (Feb 10 2022 at 22:21):

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

Eric Wieser (Feb 10 2022 at 22:22):

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

Eric Rodriguez (Feb 10 2022 at 22:27):

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

Yury G. Kudryashov (Feb 10 2022 at 23:40):

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 (Feb 10 2022 at 23:56):

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

Stuart Presnell (Feb 11 2022 at 11:29):

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 (Mar 06 2022 at 12:56):

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

Stuart Presnell (Mar 06 2022 at 22:22):

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 (Mar 06 2022 at 22:43):

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

Mauricio Collares (Apr 11 2022 at 10:43):

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

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

Eric Wieser (Apr 11 2022 at 11:03):

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

Mauricio Collares (Apr 11 2022 at 11:09):

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

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

Do GitHub merge queues have a bors d+ equivalent?

Eric Rodriguez (Apr 11 2022 at 11:28):

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

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

Yaël Dillies (Apr 11 2022 at 11:44):

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

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

Yaël Dillies (Apr 11 2022 at 11:46):

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

Eric Wieser (Apr 11 2022 at 12:45):

This feels like something for a custom workflow to handle

Eric Wieser (Apr 11 2022 at 12:45):

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

Rémi Bottinelli (Jan 21 2023 at 19:14):

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 (Jan 21 2023 at 19:26):

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

Mauricio Collares (Feb 09 2023 at 08:11):

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/


Last updated: Dec 20 2023 at 11:08 UTC