Weird bugs

Stream: new members

[Hanting Zhang]

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]

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]

(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]

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]

You added mathlib to your project using leanproject right? What exactly do you mean by "tried to delete and redownload things"?

[Hanting Zhang]

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

[Bryan Gin-ge Chen]

What did you edit in .elan?

[Hanting Zhang]

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.

[Hanting Zhang]

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.

[Bryan Gin-ge Chen]

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]

Well, it took a while, but everything has reset and Lean is running fast again. Thanks!