Zulip Chat Archive

Stream: general

Topic: Spurious mathlib CI errors?

David Loeffler (Dec 13 2022 at 19:44):

I've had several mathlib CI runs fail in the last couple of days with errors in the test "Check for modifications to ported files". The error message is something like "Error: The head commit for this pull_request event is not ahead of the base commit. Please submit an issue on this action's GitHub repo". Is this a known issue?

(It seems that merging the latest upstream master immediately before pushing suppresses the error, but this is clearly not how things are supposed to work.)

Mauricio Collares (Dec 13 2022 at 19:59):

Probably fixed by #17914. Did the last failure include this fix?

David Loeffler (Dec 13 2022 at 20:18):

Looks like it didn't, so that's probably it then. Sorry for the noise!

Mauricio Collares (Dec 13 2022 at 21:38):

I was just taking a guess, since I didn't find the actual error message anywhere. It's nice to have it documented here.

Kevin Buzzard (Dec 13 2022 at 21:40):

Yeah this might be the first time it's been mentioned here (it's been brought up on the discord and also in PMs to me). Thanks for flagging it David!

Eric Wieser (Dec 14 2022 at 01:36):

Yeah, this is my fault but can be ignored. For some reason "ask GitHub which files changed without a full mathlib checkout" is a hard problem, even though the GitHub UI shows it to humans...

Eric Wieser (Dec 14 2022 at 01:37):

List of runs is here: https://github.com/leanprover-community/mathlib/actions/workflows/add_ported_warnings.yml

Eric Wieser (Dec 14 2022 at 01:39):

Fix seems to be here: https://github.com/jitterbit/get-changed-files/issues/19#issuecomment-854657729

Eric Wieser (Dec 14 2022 at 11:27):

#17936

Eric Wieser (Dec 14 2022 at 23:00):

Can someone merge the above? We'll continue to get spurious errors until that's merged, which also means we won't spot edits to ported files.

Last updated: Dec 20 2023 at 11:08 UTC