Zulip Chat Archive

Stream: new members

Topic: vscode very slow


view this post on Zulip Lambert A'Campo (Nov 08 2019 at 14:51):

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?

view this post on Zulip Johan Commelin (Nov 08 2019 at 14:52):

Have you precompiled the library?

view this post on Zulip Johan Commelin (Nov 08 2019 at 14:52):

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

view this post on Zulip Johan Commelin (Nov 08 2019 at 14:54):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 08 2019 at 14:58):

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.

view this post on Zulip Kevin Buzzard (Nov 08 2019 at 15:12):

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.

view this post on Zulip Lambert A'Campo (Nov 08 2019 at 15:33):

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

view this post on Zulip Lambert A'Campo (Nov 08 2019 at 18:37):

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


Last updated: May 18 2021 at 17:44 UTC