Stream: new members
Topic: Weird bugs
Hanting Zhang (Dec 31 2020 at 02:56):
Hi again. For some reason Lean has become extremely slow and keeps giving me
vm check failed: is_mpz(o) (possibly due to incorrect axioms, or sorry) errors.
simp also does not seem to work properly, but only sometimes. I've tried redownloading mathlib and restarting vscode. Does anyone have any idea what is going on?
Bryan Gin-ge Chen (Dec 31 2020 at 02:57):
I don't think I've ever seen that before. Is there anything you can tell us about your system or setup that could help us reproduce it?
Julian Berman (Dec 31 2020 at 03:05):
(I likely know even less about that, but just looking at what that function is, it looks like it's how the Lean VM wraps some libgmp things -- so perhaps you or your OS/package manager have recently updated libgmp and Lean is confused with the new version?)
Hanting Zhang (Dec 31 2020 at 03:06):
I'm on macOS. For my setup, I downloaded Lean with the instructions online. The only thing I can think of is that I edited files in .elan and that I didn't build my project. The slowdowns started happening after I tried to split up my
fib work between two files. The bugs didn't happen until after I tried to delete and redownload things, though.
I don't know anything about libgmp, unfortunately.
Bryan Gin-ge Chen (Dec 31 2020 at 03:10):
You added mathlib to your project using
leanproject right? What exactly do you mean by "tried to delete and redownload things"?
Hanting Zhang (Dec 31 2020 at 03:12):
Yes, I used leanproject. I mean I deleted my project and created a new one.
Bryan Gin-ge Chen (Dec 31 2020 at 03:17):
What did you edit in
Hanting Zhang (Dec 31 2020 at 03:20):
init.data.nat.gcd.lean and added
@[simp] lemma gcd_add_self (m n : ℕ) : gcd m n = gcd m (n + m) := by simp [gcd_rec m (n + m), gcd_rec m n]
Hanting Zhang (Dec 31 2020 at 03:25):
fib file in mathlib I was working on complained about
gcd_add_self not taking arguments properly. When I tried to fix, Lean slowed down. Instead of deleting
gcd_add_self though, I did a bunch of other stuff, and that's when the bugs started appearing.
Bryan Gin-ge Chen (Dec 31 2020 at 03:30):
Editing a file in
init without recompiling would cause all of Lean's standard library to recompile in your editor, and then mathlib would have to recompile as well, and that would definitely slow things down. I would suggest reverting the change to
init and then recompiling the standard library by running
lean --make library/ in
.elan/toolchains/leanprover-community-lean-3.23.0/lib/lean (modify the path to point to whatever toolchain you're working with).
Alternatively you could
elan toolchain uninstall the messed up version of Lean and then reinstall it.
I'm not sure I understand the
vm check failed error though, but doing the above (and then possibly recreating your project / downloading new mathlib oleans using leanproject) should make things fast again.
Hanting Zhang (Dec 31 2020 at 03:56):
Well, it took a while, but everything has reset and Lean is running fast again. Thanks!
Last updated: May 06 2021 at 21:09 UTC