Code is not live compiling

Stream: new members

[Samyak Tuladhar]

I'm having an issue with Lean 4 in VSCode. I'm taking a course using the book by Heather Macbeth , which I don't think is causing the trouble, but the code is not live compiling. I need to restart the file every time just to check any errors. Oh, I'm using ErrorLens to see errors. Has anyone had this problem or does anyone know why this might be happening? Thanks!

[Matt Diamond]

@Samyak Tuladhar do you have the Lean 4 plugin installed?

[Jon Bannon]

Matt Diamond I think Samyak has the plugin installed, since Lean is running otherwise normally in VSCode. (Samyak is my student.) It's really a weird situation where the tactic state just starts going wacky after a certain point in his proof. He has a rather old laptop, though, so I am wondering if there are issues with his laptop not being up to par.

[Xiyu Zhai]

(deleted)

[Samyak Tuladhar]

Matt Diamond said:

Samyak Tuladhar do you have the Lean 4 plugin installed?

Yes, I have Lean 4 installed