Zulip Chat Archive
Stream: general
Topic: bors failing
Sebastien Gouezel (Jun 08 2021 at 06:06):
bors has been failing recently due to some instance search becoming slow. I'll fix it by adjusting locally the priorities, but for the record here is the instance search it tries to solve:
[class_instances] (0) ?x_0 : @is_scalar_tower R (@mv_polynomial S₁ R _inst_1) (@mv_polynomial S₁ R _inst_1)
(@smul_with_zero.to_has_scalar R (@mv_polynomial S₁ R _inst_1)
(@mul_zero_class.to_has_zero R
(@mul_zero_one_class.to_mul_zero_class R
(@monoid_with_zero.to_mul_zero_one_class R
(@semiring.to_monoid_with_zero R (@comm_semiring.to_semiring R _inst_1)))))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@mul_action_with_zero.to_smul_with_zero R (@mv_polynomial S₁ R _inst_1)
(@semiring.to_monoid_with_zero R (@comm_semiring.to_semiring R _inst_1))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@module.to_mul_action_with_zero R (@mv_polynomial S₁ R _inst_1) (@comm_semiring.to_semiring R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1)))))
(@mv_polynomial.module R R S₁ (@comm_semiring.to_semiring R _inst_1) _inst_1
(@semiring.to_module R (@comm_semiring.to_semiring R _inst_1))))))
(@smul_with_zero.to_has_scalar (@mv_polynomial S₁ R _inst_1) (@mv_polynomial S₁ R _inst_1)
(@mul_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@mul_zero_one_class.to_mul_zero_class (@mv_polynomial S₁ R _inst_1)
(@monoid_with_zero.to_mul_zero_one_class (@mv_polynomial S₁ R _inst_1)
(@semiring.to_monoid_with_zero (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@mul_action_with_zero.to_smul_with_zero (@mv_polynomial S₁ R _inst_1) (@mv_polynomial S₁ R _inst_1)
(@semiring.to_monoid_with_zero (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1) (@mv_polynomial.comm_semiring R S₁ _inst_1)))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@module.to_mul_action_with_zero (@mv_polynomial S₁ R _inst_1) (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1) (@mv_polynomial.comm_semiring R S₁ _inst_1))
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1)))))
(@semiring.to_module (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))
(@smul_with_zero.to_has_scalar R (@mv_polynomial S₁ R _inst_1)
(@mul_zero_class.to_has_zero R
(@mul_zero_one_class.to_mul_zero_class R
(@monoid_with_zero.to_mul_zero_one_class R
(@semiring.to_monoid_with_zero R (@comm_semiring.to_semiring R _inst_1)))))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@mul_action_with_zero.to_smul_with_zero R (@mv_polynomial S₁ R _inst_1)
(@semiring.to_monoid_with_zero R (@comm_semiring.to_semiring R _inst_1))
(@add_zero_class.to_has_zero (@mv_polynomial S₁ R _inst_1)
(@add_monoid.to_add_zero_class (@mv_polynomial S₁ R _inst_1)
(@add_comm_monoid.to_add_monoid (@mv_polynomial S₁ R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1))))))))
(@module.to_mul_action_with_zero R (@mv_polynomial S₁ R _inst_1) (@comm_semiring.to_semiring R _inst_1)
(@non_unital_non_assoc_semiring.to_add_comm_monoid (@mv_polynomial S₁ R _inst_1)
(@non_assoc_semiring.to_non_unital_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@semiring.to_non_assoc_semiring (@mv_polynomial S₁ R _inst_1)
(@comm_semiring.to_semiring (@mv_polynomial S₁ R _inst_1)
(@mv_polynomial.comm_semiring R S₁ _inst_1)))))
(@mv_polynomial.module R R S₁ (@comm_semiring.to_semiring R _inst_1) _inst_1
(@semiring.to_module R (@comm_semiring.to_semiring R _inst_1))))))
The chain of reductions has become longer since the inclusion of non_unital_non_assoc_semiring and non_assoc_semiring in our main spine of typeclass inclusions. Together with old type classes, this is not surprising it is getting slow to handle. May I suggest that, in Lean 4, we keep the main spine as short as possible (to make sure that most mainstream applications are as fast as possible), and register instances from more exotic classes with just slightly lower priority, to make sure this doesn't bite us again?
Sebastien Gouezel (Jun 08 2021 at 06:12):
#7840. Might be worth merging with priority 37 once the current batch is finished.
Sebastien Gouezel (Jun 08 2021 at 06:12):
(goes down from 13s to 144ms on my computer)
Sebastien Gouezel (Jun 08 2021 at 06:33):
The current batch just failed. @Eric Wieser , @Scott Morrison , what about merging #7840 now?
Eric Wieser (Jun 08 2021 at 06:37):
In what way are they part of the "main spine"?
Eric Wieser (Jun 08 2021 at 06:37):
Is there a simple priority change that would eject them from that spine?
Johan Commelin (Jun 08 2021 at 06:38):
@Sebastien Gouezel thanks for debugging this!
Sebastien Gouezel (Jun 08 2021 at 06:47):
Eric Wieser said:
Is there a simple priority change that would eject them from that spine?
I am not sure how Lean manages things for old style structures. The definition of a semiring is that it extends non_unital_semiring α, non_assoc_semiring α, monoid_with_zero α, so if you're looking for the addition in a semiring you will have to pass through either non_unital_semiring or non_assoc_semiring. It's in this sense that I am saying they are part of the main spine. But we shouldn't add a shortcut from semiring to has_add, because we have already seen that adding shortcuts only makes things worse most of the time.
Sebastien Gouezel (Jun 08 2021 at 06:48):
Things will be completely different in Lean 4 since we can't extend things in all directions at the same time because of new style structures. Hopefully, this will lean to a cleaner design.
Eric Wieser (Jun 08 2021 at 07:05):
I didn't think we used extends there
Eric Wieser (Jun 08 2021 at 07:05):
Yaël Dillies (Oct 14 2021 at 16:31):
It's the second time that bors fails to merge #9706 without any apparent reason. Any idea?
Bryan Gin-ge Chen (Oct 14 2021 at 16:40):
I tried clearing the temp files as some of the runners were running out of space: https://leanprover.zulipchat.com/#narrow/stream/113538-CI/topic/CI.20runner.20status/near/257562907
Hopefully that will fix things...
Yaël Dillies (Oct 14 2021 at 16:41):
Note that other PRs went through in the meantime without problems :thinking:
Bryan Gin-ge Chen (Oct 14 2021 at 18:22):
I don't understand the latest failure in the "export as low-level text file" step: https://github.com/leanprover-community/mathlib/runs/3897800798#step:11:4
Run lean --recursive --export=mathlib.txt src/
<unknown>:1:1: error: unknown declaration '_private.2353234301.add'
Error: Process completed with exit code 1.
Last updated: Dec 20 2023 at 11:08 UTC