CI: error in Post PR summary comment

Stream: mathlib4

[Vasilii Nesterov]

For some reason, CI fails with the error
./scripts/update_PR_comment.sh: No such file or directory
for these three PRs:
https://github.com/leanprover-community/mathlib4/actions/runs/9465178854
https://github.com/leanprover-community/mathlib4/actions/runs/9465906261
https://github.com/leanprover-community/mathlib4/actions/runs/9466395834

[Yaël Dillies]

cc @Damiano Testa

[Damiano Testa]

This is strange: the PR has a PR summary comment, but the CI step for it appears to be missing in .github/workflow. Could you try to merge current master into it and see if the file .github/workflows/PR_summary.yml appears?

[Damiano Testa]

I suspect that this PR managed to get an intermediate version of the PR_summary script to work, but then missed the update that would make it correct the issue that it is seeing now.

[Vasilii Nesterov]

I merged master into my branch (locally). .github/workflows/PR_summary.yml is here.

[Damiano Testa]

Ok, that is a good sign. I think that either pushing as is might work, or maybe rebase master first.

[Damiano Testa]

The issue could be that the script would still git-travel backwards in time to a version of master that does not have the scripts that master contains now and the script does not know what to do in that case.

Rebasing may help the script use a more recent version of master instead.

[Damiano Testa]

But, simply pushing what you currently have may be enough, assuming that the algorithm that git uses to find a common ancestor uses a recent-enough version of master.

[Damiano Testa]

I created #13728 (and I also already closed it) to check that simply merging master and pushing solves the CI error related to PR summary.