Cancelling builds

Stream: general

[Oliver Nash]

(deleted)

[Oliver Nash]

(deleted)

[Oliver Nash]

Sometimes when I'm working on a PR, I push up a commit that I know I will shortly follow with some other(s). In these cases I tend to cancel the CI jobs for the commit because it seems rather wasteful to kick off redundant hours of CPU time, and possibly, might generate queueing for others.

[Oliver Nash]

My questions are:

1. Does this actually help in any meaningful way?
2. If the answer to the above is yes, could/should we have a new commit to a branch automatically cancel the CI work for any previous commits?

[Kevin Buzzard]

How do you cancel CI? I've done this on several occasions in the past -- I push something and I think "I'm done" and then look through it and think "oops no I forgot a full stop in a docstring" so push something else 10 seconds later

[Alex J. Best]

There is a cancel button on the top right of pages like: https://github.com/leanprover-community/mathlib/runs/1562693851

[Kenny Lau]

I don't think the button does much, from my experience

[Alex J. Best]

Works for me, I just restarted and then cancelled a job of mine that failed yesterday to test, https://github.com/leanprover-community/mathlib/runs/1562938073

[Eric Wieser]

https://github.community/t/github-actions-cancel-redundant-builds-not-solved/16025 is one way to do point 2

[Eric Wieser]

Although if I've waited an hour and a half for a build, then spot a doc typo, usually I want the build to complete so that I at least have a cache to work off, in parallel to the updated version re-building for integration into mathlib

[Kenny Lau]

Alex J. Best said:

Works for me, I just restarted and then cancelled a job of mine that failed yesterday to test, https://github.com/leanprover-community/mathlib/runs/1562938073

are you a mod?

[Anne Baanen]

Works for me too: https://github.com/leanprover-community/mathlib/runs/1563081307

[Alex J. Best]

Nope I'm not a maintainer or anything

[Kenny Lau]

nvm it worked for me but not immediately

[Kevin Lacker]

it's helpful in general to have CI run for old commits, because if there's a bug you can use the CI history to track down where you introduced it. so I would suggest leaving the behavior like it is, if we have enough CI capacity. if you know you're not going to need it then it's fine to cancel it

[Mario Carneiro]

One thing that I sometimes find confusing is when I push a commit, then notice a stupid typo and push a fix, and then three hours later github informs me that I broke something, and I think my fix didn't work, but no, it just is reporting on the earlier commit

[Sebastian Ullrich]

So next time you explicitly cancel the build and then Github thinks it would be a great idea to send you an email about your having cancelled the build :dizzy:

[Oliver Nash]

Thanks for all the answers. Sounds like we should leave things as they are. I'm a bit amazed that CPU time is so cheap. Shows what I know!

[Rob Lewis]

I've wondered how Github justifies all the services they offer for free. I guess it's PR/advertising. We're just a drop in the bucket of open source projects and we still use a huge amount of resources. Huge in that we couldn't pay for them at market price.

[Rob Lewis]

At one point the Zulip archive script was using like 100gb of bandwidth a day. That's a Github action cloning a repo from Github.

[Kevin Lacker]

the main value of github overall, to microsoft, is not even to make money directly, but as a part of microsoft's larger set of developer products, and all the azure services. 100gb of bandwidth a day is not too much - their cost of supporting any single open source project is probably dwarfed by the cost of a single full time microsoft employee

[Kevin Lacker]

if you're curious about the business models behind software industry things like this i recommend reading stratechery - for example this on the github acquisition https://stratechery.com/2018/the-cost-of-developers/

[Kevin Lacker]

providing open source CI is probably a cost-effective way to get developers familiar with using azure

[Adam Topaz]

cc: @Colter MacDonald (for future reference)