CI failing

Stream: mathlib4

[Yury G. Kudryashov]

It looks like @Damiano Testa 's #14077 makes CI fail on any PR that depend on it.

[Yury G. Kudryashov]

E.g., here the "build Mathlib" step only compiles and runs mk_all.

[Yury G. Kudryashov]

@Damiano Testa , do you have a quick fix, or should we revert this PR for now?

[Yury G. Kudryashov]

For now, I'm rebasing my branches on top of master^ to exclude this PR.

[Bryan Gin-ge Chen]

@Yury G. Kudryashov #16808 should fix things. Sorry that I missed this in review!

[Yury G. Kudryashov]

Please double check that the fix works, then merge it.

[Damiano Testa]

Sorry about this.

I thought that I had tested that the new workflow worked, but it looks like CI always has ways of surprising you.

[Damiano Testa]

I investigated this a bit and it looks like I tested that adding a new file would work as expected, but I did not check whether modifying an existing file would not break.

[Bryan Gin-ge Chen]

There was actually a hint even in the successful logs of #14077. The "Build completed successfully." line is missing from the Build Mathlib step (compare this log from #16808). Of course, since all the checks were green, there was pretty much no way for us to notice!

[Andrew Yang]

A number of PRs of mine are failing the "Post or update the summary comment" step, giving the following error

Run PR="18684"
HEAD is now at 89b4dcf5d7 Merge 2fed817babf5778ecfd63ce888327de126381935 into ddccebecee5c4ac22e404536049b1a9ea8c79a8d
Updated 0 paths from 93e7af9cc0
HEAD is now at 89b4dcf5d7 Merge 2fed817babf5778ecfd63ce888327de126381935 into ddccebecee5c4ac22e404536049b1a9ea8c79a8d
Previous HEAD position was 89b4dcf5d7 Merge 2fed817babf5778ecfd63ce888327de126381935 into ddccebecee5c4ac22e404536049b1a9ea8c79a8d
HEAD is now at ddccebecee feat(NumberTheory/EulerProduct/DirichletLSeries): add exp-log variants of Euler products (#19034)
Updated 0 paths from 93e7af9cc0
Previous HEAD position was ddccebecee feat(NumberTheory/EulerProduct/DirichletLSeries): add exp-log variants of Euler products (#19034)
HEAD is now at 89b4dcf5d7 Merge 2fed817babf5778ecfd63ce888327de126381935 into ddccebecee5c4ac22e404536049b1a9ea8c79a8d
https://github.com/leanprover-community/mathlib4/pull/18684
Previous HEAD position was 89b4dcf5d7 Merge 2fed817babf5778ecfd63ce888327de126381935 into ddccebecee5c4ac22e404536049b1a9ea8c79a8d
Switched to a new branch 'erd1/extension'
branch 'erd1/extension' set up to track 'origin/erd1/extension'.
error: pathspec 'pr_summary' did not match any file(s) known to git
Error: Process completed with exit code 1.

Does anyone know what causes this?

[Damiano Testa]

Have you tried merging current master and pushing again? This looks like

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Relative.20technical.20debt.20in.20PRs

[Andrew Yang]

Ah I thought I just merged master but that was on a different branch. Thanks!

[Kevin Buzzard]

Mathlib master currently has a red x for some reason.

[Thomas Murrills]

On the summary, it seems that the run was cancelled:

Canceling since a higher priority waiting request for 'continuous integration-refs/heads/pitmonticone/pairwise_iUnion₂. ' exists

(Note the branch referenced in that message seems unrelated to the branch of the PR that was just merged.)

Not sure why it would think that that run was "higher priority"...?

[Bryan Gin-ge Chen]

Our build workflows are designed to cancel previous runs on the same branch so that we don't spend computer time building oudated commits (the relevant bit is here), and #20435 by @Edward van de Meent was supposed to make it so that builds for commits on master don't get canceled, but it seems that sometimes GitHub still gets confused.

(The previous Zulip discussion is here: #mathlib4 > CI cancelled on master @ 💬 )