Zulip Chat Archive
Stream: general
Topic: leanchecker error
Yury G. Kudryashov (Oct 11 2023 at 14:13):
Hi, I get a leanchecker error in #7620 and I have no idea why it happens and how to fix it. Any help is welcome.
Alex J. Best (Oct 11 2023 at 14:15):
Merge master and it should dissapear
Yury G. Kudryashov (Oct 11 2023 at 14:20):
I see now. Why the test is non-deterministic?
Alex J. Best (Oct 11 2023 at 14:26):
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/soundness.20bug.3A.20native_decide.20leakage/near/396065886 is the thread on all this, this shoul just have been a temporary issue
David Loeffler (Oct 11 2023 at 17:25):
I'm getting a similar error from a CI run on #7628.
Yury G. Kudryashov (Oct 11 2023 at 20:14):
Did you merge master?
Scott Morrison (Oct 12 2023 at 03:28):
Apologies everyone for the difficulties here. As said above, as far as I'm aware merging master fixes all problems.
lean4checker is new, and likely the way you run it will change again soon. Teething problems!
Last updated: Dec 20 2023 at 11:08 UTC