Zulip Chat Archive

Stream: new members

Topic: Weird bugs


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip Hanting Zhang (Dec 31 2020 at 03:12):

Yes, I used leanproject. I mean I deleted my project and created a new one.

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 03:17):

What did you edit in .elan?

view this post on Zulip Hanting Zhang (Dec 31 2020 at 03:20):

I edited 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]

after gcd_rec.

view this post on Zulip Hanting Zhang (Dec 31 2020 at 03:25):

Then the 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.

view this post on Zulip 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.

view this post on Zulip 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