Zulip Chat Archive
Stream: PR reviews
Topic: Thread for failed staging PRs
Jeremy Tan (Feb 05 2024 at 04:34):
This thread is for asking maintainers to re-send to bors PRs that have been sent to bors but failed staging for a technical reason (cache failed, unexpected failure after build step, etc.)
cc @Scott Morrison
Junyan Xu (Feb 05 2024 at 17:21):
There is a certain label you should feel free to add if you're granted bors d+ or r+ (the link may not work for everyone).
Jeremy Tan (Feb 07 2024 at 23:33):
#10167 failed at cache
Jeremy Tan (Feb 09 2024 at 06:01):
#10360 failed at cache
Wen Yang (Feb 13 2024 at 12:18):
#7018 and #7815 failed at build mathlib
Johan Commelin (Feb 13 2024 at 12:38):
Thanks, I took them off the queue
Ruben Van de Velde (Feb 13 2024 at 20:00):
#10233 needed a fix for the FunLike changes but is green again
Christian Merten (Feb 13 2024 at 22:09):
#10419 failed at build, I merged master, could someone give it another go?
Ruben Van de Velde (Feb 13 2024 at 22:17):
The error didn't come from your PR, fwiw
Christian Merten (Feb 13 2024 at 22:20):
I guessed so, but thought maybe merging master helps anyway. Probably it didn't make any difference though.
Ruben Van de Velde (Feb 13 2024 at 22:22):
Fortunately it didn't, though if your PR had been in the batch that bors is currently running, you would have cancelled that and bors would need to start over with the rest of the batch
Christian Merten (Feb 13 2024 at 22:29):
Ah, that's good to know. So if I push to a PR that bors is currently running on, the whole batch is cancelled?
Ruben Van de Velde (Feb 13 2024 at 22:37):
Yeah
Jeremy Tan (Feb 27 2024 at 17:45):
#10987 needs remerging – the staging commit containing it was cancelled but for some reason it was not automatically re-queued or cancelled by bors
Sébastien Gouëzel (Feb 27 2024 at 17:55):
Thanks!
Jeremy Tan (Feb 27 2024 at 18:58):
Sébastien Gouëzel said:
Thanks!
It failed again, this time at cache...
Jeremy Tan (Feb 28 2024 at 00:25):
Failed yet again at cache. I've merged master
Jeremy Tan (Feb 28 2024 at 00:30):
@maintainers?
Matthew Ballard (Feb 28 2024 at 00:35):
I am hoping it is transient network error. There is a failure to connect to the cache server in there
Kim Morrison (Feb 28 2024 at 00:48):
Jeremy Tan said:
maintainers?
@Jeremy Tan, please use @maintainers sparingly (in particular, not in this thread, unless there's at least a 24 delay.)
Michael Rothgang (Feb 28 2024 at 12:14):
#11045 failed at getting the cache; it built successfully before
Failed to connect to lakecache.blob.core.windows.net port 443 after 1360 ms: Connection reset by peer
Failed to connect to lakecache.blob.core.windows.net port 443 after 1362 ms: Connection reset by peer
Anne Baanen (Feb 28 2024 at 14:31):
Michael Rothgang said:
#11045 failed at getting the cache; it built successfully before
Failed to connect to lakecache.blob.core.windows.net port 443 after 1360 ms: Connection reset by peer Failed to connect to lakecache.blob.core.windows.net port 443 after 1362 ms: Connection reset by peer
Thanks for the notification, kicked it back on the queue!
Jeremy Tan (Mar 06 2024 at 04:44):
#9550 failed at the first attempt because of not being adapted to 4.7.1. I've pushed a simple merge/fix; would like maintainers to resend to bors
Jeremy Tan (Apr 19 2024 at 17:36):
#12267 failed at cache
Kim Morrison (Apr 20 2024 at 07:17):
Restarted.
Jeremy Tan (Aug 23 2024 at 15:26):
#15864 failed because of a deprecation, which has now been fixed
Jeremy Tan (Aug 23 2024 at 17:11):
Anyone free to re-send the above PR to bors?
Jeremy Tan (Sep 13 2024 at 05:09):
I think bors is now failing (stalled on the current staging) because a rate limit has been hit
Jeremy Tan (Sep 13 2024 at 05:27):
Jeremy Tan (Sep 13 2024 at 05:33):
The staging PR has completed all its stages but is not returning the success exit code
Jeremy Tan (Sep 13 2024 at 05:52):
nevermind, I kicked the workflow and it went through the second time
Jeremy Tan (Mar 03 2025 at 08:11):
#22284 (and apparently some contemporaries) failed at installing elan for some reason
Michael Rothgang (Mar 10 2025 at 17:22):
Would somebody like to delegate or re-bors #22783? (I accrued a merge conflict in the bors stage; I just merged master to be safe.)
Jeremy Tan (Mar 31 2025 at 03:34):
#23294 passed all CI in staging, but was not actually merged
Jeremy Tan (Mar 31 2025 at 03:40):
Can someone bors merge it again
Kim Morrison (Mar 31 2025 at 03:48):
Are you sure we don't just need to wait longer?
Jeremy Tan (Mar 31 2025 at 03:49):
I don't know why the merge did not take place after all CI passed
Kim Morrison (Mar 31 2025 at 03:50):
Patience, sometimes bors needs time to think. If it had taken >6 hours, then it is worth pinging people about.
Jeremy Tan (Mar 31 2025 at 04:31):
The specific staging build is at https://github.com/leanprover-community/mathlib4/actions/runs/14162654813
Right now (as I write this) there is no PR staged. I think no amount of waiting alone will get the PR merged, that there really has been an error and we should try again
Jeremy Tan (Mar 31 2025 at 04:32):
(does bors periodically scan for PRs with ready-to-merge label and push them on?)
Bryan Gin-ge Chen (Mar 31 2025 at 04:40):
bors did indeed crash about 2.5 hours ago, dropping all the PRs on the queue. I'll go through them now.
edit: it looks like #23294 was the only affected PR. Thanks for your patience!
Jeremy Tan (Apr 11 2025 at 02:35):
Jeremy Tan (Apr 11 2025 at 02:35):
(same issue as #23294, I think)
Last updated: May 02 2025 at 03:31 UTC