CI cancelled on master

Stream: mathlib4

[Kevin Buzzard]

I'm not sure why, but mathlib master currently is apparently not passing CI because of #20412 ? Maybe the red x is a red herring though?

Screenshot from 2025-01-03 11-06-09.png

[Henrik Böving]

If you click on the x you can see that its red because some checks were skipped or cancelled, none actually failed (though of course something might fail if they do not get cancelled, who knows!). Why that happened I cannot tell you though.

[Kevin Buzzard]

The PR itself got a green tick.

[Bryan Gin-ge Chen]

We have a step which cancels CI runs on a commit if another commit is pushed to a branch containing it, which looks like it's the culprit here (it uses this action). I don't immediately see an easy way to exclude jobs being run on commits in master, though.

[Damiano Testa]

I had seen a red cross on master already, but had not tracked it down to the "cancel previous workflows!" action: thanks for the explanation, Bryan!

[Edward van de Meent]

Bryan Gin-ge Chen said:

We have a step which cancels CI runs on a commit if another commit is pushed to a branch containing it, which looks like it's the culprit here (it uses this action). I don't immediately see an easy way to exclude jobs being run on commits in master, though.

This definitely is something that is possible with github actions, let me see if i can find this...

[Bryan Gin-ge Chen]

Ah, re-reading my message, I may have worded it poorly. It's not that we want to exclude the job from being triggered from master, it's that we don't want the action which cancels CI jobs to cancel CI on commits that are on master...

[Edward van de Meent]

i see... i still think that's possible

[Edward van de Meent]

let me look into it

[Ruben Van de Velde]

I think that'll be the same in practice, no?

[Edward van de Meent]

i hope #20435 should stop the cancelling of master building...

[Notification Bot]

20 messages were moved here from #mathlib4 > Persistent #allow_unused_tactic by Yaël Dillies.

[Bryan Gin-ge Chen]

Ruben Van de Velde said:

I think that'll be the same in practice, no?

I'm probably still not explaining this well, but see this log where pushing to a different branch caused the CI on this commit on master to get canceled.

[Ruben Van de Velde]

Huh, that surprises me

[Edward van de Meent]

from what i can tell, the cancelled CI is on a different branch, no?

[Edward van de Meent]

image.png
this seems to suggest the cancelled run belongs to RD_compProdApply?

[Edward van de Meent]

apparently, github GUI is not as intuitive as i thought

[Edward van de Meent]

it does make sense that the cancel previous CI step gets triggered in that case, it just doesn't exactly make sense that the step cancels the CI for a different branch

[Edward van de Meent]

this seems like an issue with the implementation of the action...

We could switch to using githubs concurrency option... specifically, we can have each workflow get put into the concurrency group of $${{format('{1}.{2}',github.ref, (github.ref == 'refs/heads/master' && github.run_id) || '')}}? i think that might work

[Edward van de Meent]

(and forego the current cancel CI job)

[Damiano Testa]

Edward van de Meent said:

apparently, github GUI is not as intuitive as i thought

This summarizes every use that I made of github GUI.

[Bryan Gin-ge Chen]

Ah, I wasn't aware of the concurrency option. :eyes:

[Edward van de Meent]

i'm guessing it got added at some point after we already were using the current action.

[Edward van de Meent]

the page for the current action suggests to rather use the concurrency option, which is where i found out about it

[Edward van de Meent]

#20435 now contains an implementation using concurrency