timeout in `simplicial_object`

Stream: general

[Anatole Dedecker]

Just FYI the latest bors batch has failed twice in a row because of a timeout in algebraic_topology/simplicial_object. Are we supposed to wait from bors to automatically reduce the batch, or do we need to take some action (and if so, is there anything that can be done by non-maintainers?)

[Anatole Dedecker]

There is also a conflict in #16444 which is tagged as "ready-to-merge", if it matters

[Floris van Doorn]

bors can handle with it automatically, but it is a lot quicker if a maintainer manually removes the offending PR(s) from the queue.
As a non-maintainer, if you can figure out what the PR is that is causing the build failure and post it here, then a maintainer can take it off the queue.

[Floris van Doorn]

I just took #16444 off the queue.

[Floris van Doorn]

I think #16276 was causing the issues.

[Floris van Doorn]

There was also a conflict between #16475 and #16698, so I took one of them off the queue as well.
Hopefully all remaining PRs that are currently on the queue will go through fine (they will be spread over the next 3 batches).

[Yaël Dillies]

I already opened a PR to fix the timeout and Johan merged it

[Yaël Dillies]

(well put it on the queue)

[Yaël Dillies]

See #16729

[Mauricio Collares]

I think no one actually commented bors r+ there (I see bors d+ twice)

[Mauricio Collares]

Probably because linting is taking forever

[Bryan Gin-ge Chen]

It's waiting in the build queue: https://github.com/leanprover-community/mathlib/actions?query=is%3Aqueued