Strange error in CI

Stream: mathlib4

[Artie Khovanov]

In PR #20621:
Job post-ot-update-summary-content fails with output:

Run PR="20621"
HEAD is now at 8fea628435 Merge 624611a2fdf76d7c9ba368f9baca73abf651052f into 039d0c764222c952a7433440024a4adb1aaebaba
Updated 0 paths from 7dcf6fc0b2
HEAD is now at 8fea628435 Merge 624611a2fdf76d7c9ba368f9baca73abf651052f into 039d0c764222c952a7433440024a4adb1aaebaba
Previous HEAD position was 8fea628435 Merge 624611a2fdf76d7c9ba368f9baca73abf651052f into 039d0c764222c952a7433440024a4adb1aaebaba
HEAD is now at 039d0c7642 doc(Mathlib/Algebra/CharP/LinearMaps.lean): Fix doc errors (#20679)
Updated 0 paths from 7dcf6fc0b2
Previous HEAD position was 039d0c7642 doc(Mathlib/Algebra/CharP/LinearMaps.lean): Fix doc errors (#20679)
HEAD is now at 8fea628435 Merge 624611a2fdf76d7c9ba368f9baca73abf651052f into 039d0c764222c952a7433440024a4adb1aaebaba
https://github.com/leanprover-community/mathlib4/pull/20621
Previous HEAD position was 8fea628435 Merge 624611a2fdf76d7c9ba368f9baca73abf651052f into 039d0c764222c952a7433440024a4adb1aaebaba
Switched to a new branch 'artie2000-closure-abstract'
branch 'artie2000-closure-abstract' set up to track 'origin/artie2000-closure-abstract'.
***  pr_summary passed  ***
/home/runner/work/_temp/06a5414e-c0ac-4f62-aad4-461cce7b216b.sh: line 49: ./scripts/update_PR_comment.sh: Argument list too long
Error: Process completed with exit code 126.

[Damiano Testa]

Did you try merging a recent master and pushing again?

[Damiano Testa]

This error is similar, but slightly different, from errors that I have seen before.

[Damiano Testa]

If merging master does not fix it, I will take a look.

[Damiano Testa]

(Note that a change to a part of the summary was merged an hour or so ago: I was not expecting PRs to break with the change, but you never know.)

[Damiano Testa]

Ok, that did not work.

[Damiano Testa]

Let me investigate.

[Artie Khovanov]

still broken
can't be that change bc the error started appearing even yesterday
started after I rebased my existing changes onto #20638

[Artie Khovanov]

Damiano Testa said:

Let me investigate.

thank you!

[Bryan Gin-ge Chen]

The failing job is not one of the ones required for us to merge the PR (the ones starting with "continuous integration" are the ones we (and bors) pay attention to), so I wouldn't worry about it too much.

[Damiano Testa]

It looks as though the message that the bot would post is too long, since there seems to be a 100 lines limit on arguments passed.

[Artie Khovanov]

Oh
that's fine ig

[Damiano Testa]

However, there have been PRs that touched thousands of files and I do not think that this problem ever came up.

[Artie Khovanov]

problem also doesn't come up in #20638, and the file diff between #20638 and #20621 is (currently) very small, only like 4 files?

[Artie Khovanov]

despite both PRs affecting over 100 files

[Damiano Testa]

Right, something else is off, but the script is complaining that it is receiving an input that is too long in your PR.

[Damiano Testa]

But I cannot find anything that seems exceptionally long...

[Damiano Testa]

E.g. #20436 is comparable in size, both in terms of number of files and number of lines, but also had no problems.

[Damiano Testa]

I am not really sure what is going on: the shell limit for the argument should be 20 times bigger than what I observe and yet bash complains that the argument list is too long also locally.

[Damiano Testa]

@Bryan Gin-ge Chen do you know what might be happening?

[Damiano Testa]

This happens when .github/workflows/PR_summary.yaml reaches its final line ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}": $message is a variable that is long, but does not seem insane:

$ echo "$message" | wc
    147    3755  132733

[Bryan Gin-ge Chen]

I’m not at a computer now but are there any suspicious substrings in $message? If not then I’d look at the other long examples that do work and see if there are any obvious differences

[Damiano Testa]

The string does not contain double quotes ", it contains 4 single quotes ' but does not seem to contain any weird character that would not have appeared in other strings.

[Damiano Testa]

For instance, it contains lots of backticks, but these are all over the place in other messages.

[Bryan Gin-ge Chen]

maybe for the time being you can try having the script truncate the string to various lengths and seeing when it breaks?

[Damiano Testa]

I do not have time now to investigate further, but here is a gist which should reproduce the issue:

https://gist.github.com/adomani/52d9ca2c0387e5b9cfc67261f07f13d7

[Damiano Testa]

The variable $message does have a very long line and I think that the long line might be the culprit, but I have not isolated the issue completely.

[Damiano Testa]

Bryan Gin-ge Chen said:

maybe for the time being you can try having the script truncate the string to various lengths and seeing when it breaks?

This is essentially what I tried: I took | head xx and | tail xx of the string and both from the top and from the bottom it choked when it reached the same long line.

[Damiano Testa]

Probably the issue is that there are almost 3k files that changed their imports by the same amount and this may be the first time that the number of files does not exceed the limit that the script uses and is large enough to cause problems. :shrug:

[Damiano Testa]

The limit for posting on GitHub is here:

https://github.com/leanprover-community/mathlib4/blob/2b06bd42bb773436dae0db6119c16b294ea8d2aa/scripts/import_trans_difference.sh#L70

If I remember correctly, there is a pretty large margin: probably 2 or 3 times this length would be allowed on GitHub. But the issue now is with the shell, before it reaches the time to post the comment on GitHub.

[Damiano Testa]

Anyway, it is time to go to bed for me now!

[Junyan Xu]

Not sure if it's connected, but GitHub had an issue for some period:
Pasted image 20250114011250.png

Other symptoms:
Pasted image 20250114010746.png
Pasted image 20250114005056.png

[Bryan Gin-ge Chen]

I attempted to reproduce on my macOS machine (in both zsh and bash shells) but am not seeing the error. (If it matters, the commit of origin/master is 93a78ce08172d64f34b00d48cee6c0cc12c949ea and artie2000-closure-abstract is 16be1f426a8d82c391bf59b92ce3de6bb1cc8b76; the update_PR_comment.sh script fails when it can't find GITHUB_REPOSITORY and GITHUB_TOKEN; filling in those and comment_id with dummy values results in the curl command failing to connect, as expected).

To make the script more robust against "argument list too long", maybe we could save message to a file and then use that everywhere instead of a shell variable? Both jq and curl should be able to read / write input from files just as easily.

[Damiano Testa]

Yes, maybe saving the message to a file is a good solution: on my machine I could reproduce.

[Damiano Testa]

(Also, I had forgotten that I had to replace the variables with dummy names, but it was indeed one of the steps that I also had to go through!)

[Bryan Gin-ge Chen]

I'll see if I can open a PR to fix the script along these lines tonight or tomorrow :fingers_crossed:

[Damiano Testa]

I made a start towards this: #20761.

[Damiano Testa]

It looks like Bryan's idea to store the message in a file works!

[Damiano Testa]

I think that the issue was that there was a really long line in the string that was being passed around.

[Damiano Testa]

So, while the total length of the string and the total number of lines in the string was not bigger than in other PRs, there may be a limit on length of individual lines that triggered an error in some function.

[Artie Khovanov]

It works! thanks

[Junyan Xu]

store the message in a file

I've observed some github-actions bots are now posting comments on PRs with the sole content messageFile.md, e.g. here where it should post PR summary with import changes, declarations diff and tech debt change.

[Christian Merten]

Junyan Xu said:

store the message in a file

I've observed some github-actions bots are now posting comments on PRs with the sole content messageFile.md, e.g. here where it should post PR summary with import changes, declarations diff and tech debt change.

See #mathlib4 > messageFile.md .

[Nick Ward]

As @Christian Merten said, this should be fixed by merging master. I can't really comment on the cause, other than to say it appears to be the PR_summary workflow from #20761 running against scripts/update_PR_comment.sh from a pre-20761 commit.

[Damiano Testa]

The cause is that the script used to take as input the string to be updated, but now it takes the name of a file containing the message.

[Damiano Testa]

Since the "fix" is simply to merge master, it was decided to not add extra backwards compatibility fluff in the script.

[Nick Ward]

I wonder if its worth having a script that pings PR authors to merge master if a newer scripts dir is needed?

[Damiano Testa]

I hope that these scripts change seldom enough that it may not be worth it. However, I will keep it in mind: rather than printing the file name, this time it would have been minimal effort to make it print "Merge current master and push again to see the PR summary report.".

[Nick Ward]

Oh good point. You don't really need to do anything fancy, just put a message in the same place you were already going to.

[Michael Rothgang]

(It's not hard to find all such PRs. If you would like to mass-post, ping me and I can compute this easily.)