Zulip Chat Archive

Stream: general

Topic: github actions: can we cancelled obsolete builds?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 25 2020 at 05:55):

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

view this post on Zulip Scott Morrison (Mar 25 2020 at 05:55):

Is there any hope of cancelling builds for obsolete commits?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 25 2020 at 05:59):

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

view this post on Zulip Scott Morrison (Mar 25 2020 at 06:20):

#2235, seems to work great!

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 25 2020 at 08:01):

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

view this post on Zulip Johan Commelin (Mar 25 2020 at 08:02):

There is already a manual way

view this post on Zulip Rob Lewis (Mar 25 2020 at 08:02):

Of course you can manually cancel a build.

view this post on Zulip Johan Commelin (Mar 25 2020 at 08:02):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Rob Lewis (Mar 25 2020 at 08:41):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Mar 25 2020 at 08:42):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 25 2020 at 09:26):

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


Last updated: May 13 2021 at 05:21 UTC