Zulip Chat Archive
Stream: mathlib4
Topic: bors crashed
Scott Morrison (Dec 03 2022 at 18:25):
https://app.bors.tech/repositories/37904/log
Any ideas?
Bryan Gin-ge Chen (Dec 03 2022 at 20:27):
No clue. I've filed an issue here for now: https://github.com/bors-ng/bors-ng/issues/1578
Scott Morrison (Dec 04 2022 at 02:02):
I've merged the four stuck PRs by hand (building and testing locally!) hopefully it went okay.
Matej Penciak (Dec 05 2022 at 20:15):
Is bors unstuck now? It looks like a few PRs were merged the last few hours. For PRs that are all done but not merged (like mathlib4#833) should we go back in and remind bors with bors r+ again?
Scott Morrison (Dec 05 2022 at 23:26):
I've restarted it. So far bors is behaving.
Ruben Van de Velde (Dec 09 2022 at 11:01):
Seems like bors ignored mathlib4#918 - is it down again?
Jeremy Tan (Mar 14 2023 at 10:59):
Just now 3 PRs completed their Bors staging but for some reason are not being merged into master
Jeremy Tan (Mar 14 2023 at 10:59):
Jeremy Tan (Mar 14 2023 at 11:08):
someone try to restart the staging process for them?
Floris van Doorn (Mar 14 2023 at 11:16):
We indeed got another bors crash half an hour ago.
Floris van Doorn (Mar 14 2023 at 11:20):
I delegated/re-added those PRs
Jeremy Tan (Mar 14 2023 at 11:40):
sorry, I meant !4#2247
Jeremy Tan (Mar 14 2023 at 14:21):
!4#2874 suffered a merge conflict; someone re-bors r+ ?
Jeremy Tan (Mar 14 2023 at 14:21):
or can I do it myself?
Ruben Van de Velde (Mar 14 2023 at 14:23):
No, that'll need a maintainer.
Ruben Van de Velde (Mar 14 2023 at 14:23):
Maybe @Chris Hughes is around
Jeremy Tan (Mar 14 2023 at 14:24):
the conflict is happening because my two small PRs and the just-merged Algebra.CharP.Two modify Mathlib.lean in almost the same place
Scott Morrison (Mar 15 2023 at 01:29):
It looks like all of these have gone through now.
Notification Bot (Mar 15 2023 at 01:29):
Scott Morrison has marked this topic as resolved.
Notification Bot (Mar 16 2023 at 17:31):
Jeremy Tan has marked this topic as unresolved.
Jeremy Tan (Mar 16 2023 at 17:31):
Bors build for !4#2836 may have crashed; the staging process competed but it is not pushing to master
Jeremy Tan (Mar 16 2023 at 17:35):
nvm
Notification Bot (Mar 16 2023 at 17:35):
Jeremy Tan has marked this topic as resolved.
Jeremy Tan (Mar 27 2023 at 12:28):
(deleted)
Notification Bot (Mar 27 2023 at 12:30):
Jeremy Tan has marked this topic as unresolved.
Jeremy Tan (Mar 27 2023 at 12:30):
bors crashed again, https://github.com/leanprover-community/mathlib4/compare/master...staging succeeded but was not committed to master
Jeremy Tan (Mar 27 2023 at 12:32):
Chris Hughes (Mar 27 2023 at 12:37):
https://www.githubstatus.com/ Github is having issues right now, so that's probably the problem
Chris Hughes (Mar 27 2023 at 13:31):
It's back up
Jeremy Tan (Mar 27 2023 at 13:42):
wew, now back to work
Jeremy Tan (Mar 29 2023 at 16:42):
!4#3132 was pushed to staging by bors but is not being run, bors may have crashed
Bryan Gin-ge Chen (Mar 29 2023 at 16:44):
Looks like GitHub Actions is having issues again: https://www.githubstatus.com/
Jeremy Tan (Mar 31 2023 at 17:22):
!4#3190 succeeded at staging, but wasn't pushed or closed by bors. And GitHub is not at fault this time
Jeremy Tan (Mar 31 2023 at 17:22):
...wait
Jeremy Tan (Mar 31 2023 at 17:23):
bors has just closed the issue as expected
Eric Wieser (Mar 31 2023 at 17:36):
It did crash and forget about !4#3191 it seems
Ruben Van de Velde (Mar 31 2023 at 17:42):
It's best to assume Bors will need a bit of time after the build succeeded to push the actual merge to master
Jeremy Tan (Apr 20 2023 at 17:02):
https://github.com/leanprover-community/mathlib4/actions/runs/4756604274/jobs/8452374862 this staging job for my !4#3553 is perpetually waiting for a runner to lint the style. What is going on – I suspect bors has crashed
Jeremy Tan (Apr 20 2023 at 17:07):
wait, the runner came!
Eric Wieser (Apr 20 2023 at 17:24):
Probably what's happening is that a bunch of mathlib3 PRs have claimed CI machines
Jeremy Tan (Apr 20 2023 at 17:32):
Those mathlib3 PRs are also waiting for runners, and non-staging CIs in mathlib4 are completing in due course, so the mathlib3 PRs can't be the reason
Jeremy Tan (Apr 20 2023 at 17:32):
https://github.com/leanprover-community/mathlib4/actions/runs/4757014979 this is now stuck for the same reason
Jeremy Tan (May 15 2023 at 09:07):
bors has not closed the last several merged mathlib4 PRs; what's wrong?
Jeremy Tan (May 15 2023 at 09:10):
Or rather it hasn't even merged the PRs after the staging build passes
Mauricio Collares (May 15 2023 at 09:11):
Example?
Jeremy Tan (May 15 2023 at 09:11):
Mauricio Collares (May 15 2023 at 09:14):
Very strange indeed
Ruben Van de Velde (May 15 2023 at 09:15):
And it's running the next batch already, odd. Perhaps someone can put them in the queue again
Floris van Doorn (May 15 2023 at 09:51):
I added all of them on the queue.
Floris van Doorn (May 15 2023 at 09:51):
bors crashed this morning
Jeremy Tan (May 15 2023 at 10:57):
!4#3981, being delegated and bors r+'d, needs a bump too
Jeremy Tan (Jun 07 2023 at 17:48):
bors is not staging/merging the Algebra.Spectrum file; it's been 40 minutes since the last merge
Jeremy Tan (Jun 07 2023 at 17:48):
(!4#4778)
Yury G. Kudryashov (Jun 07 2023 at 17:49):
Is it bors or github?
Jeremy Tan (Jun 07 2023 at 17:49):
bors
Yury G. Kudryashov (Jun 07 2023 at 17:50):
Because github behaves strangely with, e.g., !4#4814
Yury G. Kudryashov (Jun 07 2023 at 17:50):
I mean, the failure can be on the github side.
Yury G. Kudryashov (Jun 07 2023 at 17:50):
If you look at https://github.com/leanprover-community/mathlib4/tree/staging, you can see that github didn't run any CI scripts
Jeremy Tan (Jun 07 2023 at 17:51):
right, there is an issue with github right now; I checked status
Jeremy Tan (Jun 07 2023 at 18:14):
OK, the latest batch was merged, try sending it to bors again
Last updated: Dec 20 2023 at 11:08 UTC