A CI error message I don't understand

Stream: mathlib4

[Sina Hazratpour]

My PR builds and passes linter locally, but I am getting this CI error message at the build stage which I don't understand. Anyone who knows what this says and how it can be resolved?

https://github.com/leanprover-community/mathlib4/actions/runs/19133718169/job/54680513835?pr=30373

NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing

https://github.com/leanprover-community/mathlib4/actions/runs/19133718169/job/54680513835?pr=30373#step:40:613/home/lean/actions-runner/_work/_temp/20530572-d485-4183-8d45-f23b065f2dc1.sh: line 1: master-branch/scripts/lean-pr-testing-comments.sh: No such file or directory

https://github.com/leanprover-community/mathlib4/actions/runs/19133718169/job/54680513835?pr=30373#step:40:614Error: Process completed with exit code 127.

[Michael Rothgang]

I haven't seen this error either. Interesting. Did you try merging master?

[Michael Rothgang]

(That's the analogue of "did you reboot your computer". Sorry if you already did, but let's exclude this first.)

[Sina Hazratpour]

Thanks for taking a look into this. I assume you mean the master branch of my mathlib fork; by merging do you mean git fetch and then git pull on the branch of this PR (lccc-section)? If so, I have done this.

[Robin Carlier]

No, you need to merge master from the upstream repo! You can do this by git fetch upstream followed by git merge upstream/master (assuming the upstream repo is named "upstream" in you local setup, which should normally be the case)

[Robin Carlier]

(the commands above need to be performed from your local repo while the branch of the PR is checked out)

[Sina Hazratpour]

interesting! I basically never do this (and this CI issue never arises in other PRs), since i thought my master branch automatically tracks upstream following the step 4 of this guide:
https://leanprover-community.github.io/contribute/git.html
But, i guess it does not hurt trying in this case.

[Robin Carlier]

Oh, right, if your local master branch tracks upstream/master it should be fine. (though in this case I think that you may still need to git pull while master is checked out from time to time to update it, as git fetch alone will not write anything to your local copy of master, when doing explicitly git merge upstream/master you are sure that you are merging the one from mathlib)

[Yaël Dillies]

@Robin Carlier, are you saying that your local master branch tracks your fork's master? Is there any reason one would ever do this (instead of tracking the original repo's master branch)?

[Robin Carlier]

No? My local master tracks upstream? You’re right that you usually don’t want to do this.

[Sina Hazratpour]

@Robin Carlier
git merge upstream/master did it though – the PR passed CI – which leaves me more confused since i thought upstream changes were being tracked automatically, and I think they were not, since git merge upstream/master actually pulled some new stuff.
I did the step 4 of the guide again, namely git branch --set-upstream-to=upstream/master master. Let's hope this issue never arises again.

[Chris Henson]

Yaël Dillies said:

Robin Carlier, are you saying that your local master branch tracks your fork's master? Is there any reason one would ever do this (instead of tracking the original repo's master branch)?

I do this, because I personally find it an easier to remember delineation between the fork and upstream.

[Robin Carlier]

Sina Hazratpour said:

Robin Carlier
git merge upstream/master did it though – the PR passed CI – which leaves me more confused since i thought upstream changes were being tracked automatically, and I think they were not, since git merge upstream/master actually pulled some new stuff.
I did the step 4 of the guide again, namely git branch --set-upstream-to=upstream/master master. Let's hope this issue never arises again.

The diff for the last commit (merging the remote branch) looks pretty small so it’s safe to assume the tracking was working and you just picked up the few PRs that were merged recently. So it was maybe just a transient error :shrug:

(I usually do merge upstream/master explicitly instead of relying on the tracking just out of habit, so that I don’t have to bother if my local master is behind the upstream one because I didn’t git pull on it for a while, but it’s really a matter of taste.)

[Bryan Gin-ge Chen]

I think this is probably related to #31316. I'll push a fix shortly.

[Yaël Dillies]

I can confirm the error doesn't go away on merging master: #22039

[Bryan Gin-ge Chen]

I've used my admin powers to push #31329. This should hopefully fix things for PRs from forks after it lands on master (merging master shouldn't be necessary).