Zulip Chat Archive

Stream: general

Topic: github actions: can we cancelled obsolete builds?


Scott Morrison (Mar 25 2020 at 05:55):

Hmm... the new leanproject up and faster CI is amazing, but it's so good it's causing a problem. I'm happily relying on github to build branches for me rather than compiling them completely locally, and I'm even jumping back and forth between branches working on whatever is available while CI works on other branches. The result, however, is that I'm spamming github with new commits.

Scott Morrison (Mar 25 2020 at 05:55):

I only just realised, per https://github.com/leanprover-community/mathlib/actions, that making a new commit on a branch doesn't cancel the build running on the old commit.

Scott Morrison (Mar 25 2020 at 05:55):

And so I'm causing a lot of work for github actions. :-)

Scott Morrison (Mar 25 2020 at 05:55):

Is there any hope of cancelling builds for obsolete commits?

Scott Morrison (Mar 25 2020 at 05:57):

It seems https://github.community/t5/GitHub-Actions/Github-actions-Cancel-redundant-builds/td-p/29549 is about this.

Scott Morrison (Mar 25 2020 at 05:57):

and someone says it is scriptable: https://github.community/t5/GitHub-Actions/Github-actions-Cancel-redundant-builds/m-p/44690/highlight/true#M5869

Scott Morrison (Mar 25 2020 at 05:59):

and maybe https://github.com/marketplace/actions/workflow-run-cleanup-action is a solution?

Scott Morrison (Mar 25 2020 at 06:20):

#2235, seems to work great!

Johan Commelin (Mar 25 2020 at 07:39):

@Scott Morrison Right now I see 3 builds in action on that PR. So it doesn't seem to cancel them...

Rob Lewis (Mar 25 2020 at 07:56):

I'm not sure this is a good idea. Often I'd like the earlier builds to finish, just to see if there are errors I didn't anticipate in the newer commits.

Rob Lewis (Mar 25 2020 at 07:57):

Note that we don't upload olean caches if there's a new commit when the build finishes.

Mario Carneiro (Mar 25 2020 at 08:01):

Even so, it might be nice to have a way to manually cancel a build

Johan Commelin (Mar 25 2020 at 08:02):

There is already a manual way

Rob Lewis (Mar 25 2020 at 08:02):

Of course you can manually cancel a build.

Johan Commelin (Mar 25 2020 at 08:02):

Just go to the page of the build, and click cancel

Bryan Gin-ge Chen (Mar 25 2020 at 08:02):

Another point: I think we have a limit of 20 concurrent jobs. So far the most I've seen running at one time is around 17. However, if we switch community Lean to github actions, then we will probably run into problems.

Rob Lewis (Mar 25 2020 at 08:41):

I think I posted something along these lines a few weeks ago and then forgot about it: the PR builds aren't doing anything for us, are they? They test a merge commit that will never be checked out, and Mergify makes sure that the one merge commit that matters gets tested (as a push build).

Rob Lewis (Mar 25 2020 at 08:41):

The PR builds only matter for PRs that come from an external repo with Actions disabled.

Rob Lewis (Mar 25 2020 at 08:42):

There are other reasons to avoid external PRs as much as possible, and if we get them, we can just ask the author to enable Actions. It's simple to do.

Rob Lewis (Mar 25 2020 at 08:42):

No configuration needed because the Actions config is part of the repo.

Rob Lewis (Mar 25 2020 at 08:43):

This should be as effective at cutting down the number of builds, and less disruptive than auto cancelling obsolete ones.

Gabriel Ebner (Mar 25 2020 at 08:59):

Rob Lewis said:

Note that we don't upload olean caches if there's a new commit when the build finishes.

I'd like to revisit this decision once we have the garbage collection script set up. I'm regularly running into the situation where I'd like to have oleans for old revisions and I'd be happy to git reset --hard HEAD^^ && leanproject get-cache for lack of better tooling. But it's vexing when you're waiting for the CI build to finish and somebody pushes a fix for a typo and now you have to wait again.

Rob Lewis (Mar 25 2020 at 09:00):

Fair enough. Once garbage collection is running we can delete those builds quickly, after a day or two.

Scott Morrison (Mar 25 2020 at 09:26):

Okay, I will close my "cancel obsolete builds" PR, which looked like trouble anyway.


Last updated: Dec 20 2023 at 11:08 UTC