vscode very slow

Stream: new members

[Lambert A'Campo]

I have roughly 20 lines of lean code and my vscode gets stuck on checking it. Are there some tricks to speed it up or some tactics I need to avoid to be able to use the interactive mode?

[Johan Commelin]

Have you precompiled the library?

[Johan Commelin]

Otherwise it will be checking lots of stuff in the background as soon as you do anything

[Johan Commelin]

Useful info to provide in this chat: how did you install Lean? Did you install mathlib? If so, how?

[Bryan Gin-ge Chen]

The recommended way is here. If you already followed that, then probably we need to see your code to be able to say anything useful.

[Kevin Buzzard]

Lambert are you at Imperial? These things are often not hard to debug if I can actually get my hands on the machine you're using. It shouldn't be slow with 20 lines of code.

[Lambert A'Campo]

I am, but I am in class. Thanks for offering! I will check if I precombiled mathlib later.

[Lambert A'Campo]

I recreated the project, following all the steps on the tutorial and that seems to have helped.