github actions: can we cancelled obsolete builds?

Stream: general

[Scott Morrison]

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]

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]

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

[Scott Morrison]

Is there any hope of cancelling builds for obsolete commits?

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

#2235, seems to work great!

[Johan Commelin]

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

[Rob Lewis]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

There is already a manual way

[Rob Lewis]

Of course you can manually cancel a build.

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Gabriel Ebner]

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]

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

[Scott Morrison]

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