Issues with Running Tactics on Repos Using Lean `>= v4.12.0`

Open yangky11 opened this issue 1 year ago • 2 comments

We're working with the Lean community to address the issue: See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Weird.20IO.20Behavior.20Introduced.20in.20v4.2E12.2E0

Oct 13 '24 17:10 yangky11

Is there any progress? Just fail to interact with theorem in mathlib using v4.14.0.

Dec 09 '24 15:12 timechess

If you have a minimal example for reproducing the error, it would be very helpful to paste it here.

Unfortunately, I don't think this error is going to be solved anytime soon, due to its complexity and my lack of bandwidth.

Dec 11 '24 18:12 yangky11