Zulip Chat Archive

Stream: PR reviews

Topic: bors timeout

Sebastien Gouezel (Jun 11 2021 at 12:01):

bors has just timed out on a proof in lie/classical.lean. It might be a good idea to merge quickly #7894 that fixes this.

Patrick Stevens (Jun 12 2021 at 08:29):

Bors has been timing out on https://github.com/leanprover-community/mathlib/pull/7748 in classical.lean and also in ring_theory/adjoin_root.lean:248:0 :(

Sebastien Gouezel (Jun 12 2021 at 09:26):

#7905

Last updated: Dec 20 2023 at 11:08 UTC