Zulip Chat Archive
Stream: mathlib4
Topic: !4#5022, forward port of #19179
Scott Morrison (Jun 14 2023 at 00:09):
A maxHeartbeats had been cranked down to the bare minimum here, and then this PR has caused it to go over again.
Scott Morrison (Jun 14 2023 at 00:09):
@Riccardo Brasca, I see you self-assigned this PR. Are you planning on making further changes?
Riccardo Brasca (Jun 14 2023 at 00:11):
Not really, but I can review/finish it tomorrow if it's needed.
Eric Wieser (Jun 14 2023 at 00:15):
I haven't yet checked that the changes are correct here, which is why I've left !4#5022 as awaiting-author
Eric Wieser (Jun 14 2023 at 00:17):
The failing proof is one that I "simplified" compared to the version in Chris's PR
Eric Wieser (Jun 14 2023 at 00:18):
It might be interesting to compare the proofs more closely, but I'm out of time today
Last updated: Dec 20 2023 at 11:08 UTC