Post PR summary comment / build (pull_request) fails

Stream: mathlib4

[Jiang Jiedong]

Hi, everyone!

My PR #13533's CI "Post PR summary comment / build (pull_request)" fails. I have no idea what is happening.

The error message says that

Previous HEAD position was 40eae034a1 Merge d0da6d4b6a6d2c2d24677357dd88369a0853fffd into 81e2c63b8af1371a08072e40e50aeb41c26ed591

Switched to a new branch 'jiedong_jiang_is_val_extension'

branch 'jiedong_jiang_is_val_extension' set up to track 'origin/jiedong_jiang_is_val_extension'.

/home/runner/work/_temp/2d2c18bd-3af9-471c-ad05-21c6503f4e1d.sh: line 27: ./scripts/update_PR_comment.sh: No such file or directory

Error: Process completed with exit code 127.

What should I do to solve this problem? Thank you!

[Ruben Van de Velde]

I think merging master will help

[Jiang Jiedong]

Ruben Van de Velde said:

I think merging master will help

Thank you! It worked!

[Notification Bot]

Jiang Jiedong has marked this topic as resolved.

[Damiano Testa]

Great! A small number of PRs were caught in a weird state where the script was trying to retrieve a file from a commit of master that was too early to contain it. Updating master makes the file available where the script looks for it.

[James Sundstrom]

I'm not sure whether I should make this a separate topic or if the answer will turn out to be partly relevant here, but here goes.

I had this same problem with #13013. I tried to merge master, but I think I screwed up. All the recent changes to Mathlib are being treated as part of my PR, which now says that it's changing 2,215 files. I tried reverting the last merge, which didn't fix that. But strangely, it now passes CI, despite the fact that I was trying to revert to a version that failed.

I think it's time to admit that I don't know what I'm doing. Help!

[Eric Wieser]

It looks like you did a rebase accidentally somehow

[James Sundstrom]

Okay, but how do I fix it now? I considered abandoning it and copying my code into a new PR, but there are already reviews on this PR, so that seems like a last resort.

[Notification Bot]

James Sundstrom has marked this topic as unresolved.

[Damiano Testa]

There are probably much better ways of doing this, but if you were the only author of the changes in the PR, you could try cherry-picking in a new branch all the commits that you made this PR...

[Kevin Buzzard]

When I've found myself in this situation in the past I've just saved my work, closed the PR and opened a new one on the basis that it's quicker than learning about the different merge strategies in git and that nobody is going to mind.

[Jon Eugster]

I pushed this suggestion (using git cherry-pick) to a new branch called js2357/LebesgueVitali_clean. I think it's easiest if you create a new PR from this and then tell us if you are missing stuff on that new branch. But I could only see two relevant commits on the old branch, where there more?

If there are still missing commits, you might be able to understand better what happened by digging through git reflog on your local machine, but that's wee technical.

I think you could theoretically force-push the correct state to the PR's old branch to recover, but that's highly dangerous as a wrong step leads to unrecoverable loss, so creating a new PR from that new branch seems indeed the safer and better option. You addressed all review comments already, so it's not too much of a loss if they don't appear, and you can always link to the broken PR in the new one.

[James Sundstrom]

Thanks for the help. For some reason git cherry-pick missed some stuff, so I ended up making a new branch and manually copy-pasting the relevant code. Anyway, the problem seems to be resolved.