Bryan Gin-ge Chen
Bryan Gin-ge Chen
Two of our batches (running on the public instance) have crashed today due to timeouts: https://app.bors.tech/repositories/24316/log I'm reporting them here in case it helps. Mon, 04 Oct 2021 13:19:04 GMT:...
See the sequence of events starting just before this comment: https://github.com/leanprover-community/mathlib/pull/5672#issuecomment-761586085 The failure that occurred [here](https://github.com/leanprover-community/mathlib/pull/5672#issuecomment-761679567) was Batch 119110.
This would make it easier to track those PRs.
This batch has been stuck on Waiting to Run for several hours: https://app.bors.tech/batches/114772 Is there something we can do to get it running again?
bors seems to comment with "Already running a review" when a closed PR gets approved, instead of something like "Cannot merge a closed PR". See the sequence of events [starting...
I had to add a bunch of ugly well-founded proofs here. Related Zulip threads: - [Mario's suggestion in "moving algebra out of core"](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/moving.20algebra.20out.20of.20core/near/197122044), - ["well founded tactics"](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/well_founded_tactics)
One of the tests under `leanruntest_all` seems to be failing sometimes on macos debug: https://github.com/leanprover-community/lean/pull/617#issuecomment-918406979 https://github.com/leanprover-community/lean/pull/622#issuecomment-925204586
See https://github.com/leanprover-community/lean/issues/501#issuecomment-753499459
leanprover-community/mathlib#3185 exposed a bug in leanchecker. [See zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/3185.20leanchecker.20failure/near/202224327).
> It could either be an extra argument to the `environment.add_decl` function, or a free function `set_decl_pos`, depending on the constraints in the C++. From https://github.com/leanprover-community/mathlib/issues/4778