Build failed: detect changes to header SHAs

Stream: mathlib4

[Anne Baanen]

We're running into build failures I don't understand on #6576: https://github.com/leanprover-community/mathlib4/actions/runs/6399965647/job/17378238549

As far as I can see we didn't touch any header SHA, so why is this build step failing, and how can we fix it?

[Alex J. Best]

#6576 I think you mean

[Anne Baanen]

Alex J. Best said:

#6576 I think you mean

Corrected, thanks!

[Alex J. Best]

Did you merge master recently?

[Anne Baanen]

Nope, let's try that...

[Damiano Testa]

I opened the PR a while ago and I merged master yesterday, after a long period of non-merging, but the SHAs were still unhappy. Anyway, I see that Anne merged it again now: if the check passes, I am happy!

[Anne Baanen]

It failed :(

[Damiano Testa]

I also tried pushing your suggestion, in case it helped, but it failed again.

[Scott Morrison]

Rebase on master?

[Eric Wieser]

Does the sha it complains about exist?

[Eric Wieser]

If so, I would guess that adding a git fetch somewhere in CI fixes it.

[Eric Wieser]

(due to some shallow checkout shenanigans)

[Damiano Testa]

Unfortunately,

$ git cat-file -e 530610771ae0ef4ca41280633545883763d0b897 || echo fail
fail

[Damiano Testa]

I'll try to rebase master, if I can do it via gitpod.

[Damiano Testa]

On gitpod, I can rebase master, but I have not found a way to push the rebased branch back to remote. It seems that it is a problem with permissions. I'll try it when I am back at home later today

If someone else wants to have a look before, when rebasing there is only one non-clean commit and you simply accept all "current changes" (it is just indentation and almost all conflicts are identical in the two versions anyway).

[Anne Baanen]

Let me have a go rebasing...

[Damiano Testa]

The SHAs are happy! Thank you @Anne Baanen!!

[Anne Baanen]

Now let's hope I didn't mess up the rebase :fingers_crossed:

[Damiano Testa]

It is already linting, so I am confident that it will work! Thank you very much!

[Damiano Testa]

For future reference, Scott's suggestion of rebasing master fixed this issue!

Thank you all for the help!

[Eric Wieser]

The sha is supposed to be in mathlib3 not mathlib4

[Damiano Testa]

While I did the wrong check earlier, it turns out that the SHA did not exist in Lean 3 either:

$ lean --version
Lean (version 3.51.1, commit cce7990ea86a, Release)
$ git cat-file -e 530610771ae0ef4ca41280633545883763d0b897 || echo fail
fail

[Eric Wieser]

Does GitHub know about it?

[Eric Wieser]

How did the sha get there?

[Eric Wieser]

I looked at the stack trace more closely; this looks like somehow GitPython is confused; it ran git diff, then looked at the shas in the git diff header and blew up because they didn't exist.

[Damiano Testa]

Eric, I am afraid that I do not even understand if you have answered your own question or not...

[Joachim Breitner]

Just a blind pass-by comment, but Git has this horrible default setting where a pull_request CI job does _not_ run on the latest commit of the feature branch. Instead, it secretly does a merge with the target branch, and runs on that commit, which you will not find anywhere else. Could this be it?

(This behavior can be very confusing, because it is inherently stateful and with hidden state at that. It could be that your PR looks red even though everything works locally, and then it suddenly turns green the next time you run it, just because the target branch changed.)

[Joachim Breitner]

The linked action says at the beginning:

  /usr/bin/git checkout --progress --force refs/remotes/pull/6576/merge
  Note: switching to 'refs/remotes/pull/6576/merge'.

  HEAD is now at 7680267 Merge 6704be3b38a4acf30eb3bb602443e70680a7c88f into b2540cf9b47f7cf8d913114cb688317719bc50b4

so maybe that’s how otherwise unknown git commits enter the scene?

[Damiano Testa]

Joachim, in the past, when I had issues with SHAs, it is true that they went away simply by re-running the job... sometimes.

What I do not understand is why this behavious of Git would not give errors always, but only occasionally.