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

[yangky11]

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

[timechess]

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

[yangky11]

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.