bors issues

Stream: general

[Ruben Van de Velde]

It seems like the last two attempts to merge something had their ci cancelled? https://github.com/leanprover-community/mathlib/actions/workflows/bors.yml?query=branch%3Astaging

[Yaël Dillies]

bors keeps misreporting that Ci runs failed linting when in fact they failed building. Here's one example. Why do you think this is happening?

[Eric Wieser]

I think you would do better to report that upstream to bors

[Ruben Van de Velde]

It seems like the latest bors run failed (https://github.com/leanprover-community/mathlib4/actions/runs/6160617263/job/16717992280), but it's not starting any new ones

[Johan Commelin]

Mario's and Scott's heroic efforts on improving CI and caching caused some hiccups. But hopefully everything is back on track (soon).

[Mario Carneiro]

that error looks like a std bump issue

[Ruben Van de Velde]

The error is from #3464

[Mario Carneiro]

FYI I'm done for the day re: fixing the cache issues, there are now threads for Mac Malone and Wojciech Nawrocki to follow up on

[Damiano Testa]

I am not sure if this is relevant, but my PR #7075 was in the queue and really acquired a merge conflict. I have resolved the conflict and CI is linting it.

[Damiano Testa]

#7075 passed CI after the merge conflict, but is no longer on the bors queue: can someone put it there again, please? Thanks!

[Ruben Van de Velde]

Would be nice if one of the maintainers could go through https://github.com/leanprover-community/mathlib4/pulls?q=is%3Aopen+is%3Apr+label%3Aready-to-merge and put them on the queue again

[Alex J. Best]

We should have a triage-like bot for this (that reposts a link to all prs that have been marked ready to merge for 24h say). Or just find a way to stop bors forgetting about such prs.

[Anatole Dedecker]

I think I’ve told bors to retry on each of them (with the exception of #7099 which was causing the failures IIUC), let me know if I missed any