Zulip Chat Archive

Stream: general

Topic: Visual Studio Code: performance


view this post on Zulip François Sunatori (Mar 09 2021 at 03:47):

Hi,
I'm using Lean 3 in Visual Studio Code on a 2015 MacBook and find that it can get very slow when checking certain files. The only trick I found that helps a little is to set Lean to "checking visible lines". It helps sometimes but for certain files it still takes minutes until I see the proof state appear... It also slows down my computer as a whole and I need to quit Visual Studio Code sometimes when having it in the background and navigating in Chrome. I was wondering if there is anything I can do to make it faster.
Thanks!

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 03:50):

If you're editing mathlib files that are far apart in the import chain, this is expected, as the Lean server has to recompile all files that depend on any edited file. What files are you editing?

view this post on Zulip François Sunatori (Mar 09 2021 at 03:52):

I created a short file in analysis/complex that imports analysis.complex.basic.

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 03:52):

Did you edit any files that are imported by that file?

view this post on Zulip François Sunatori (Mar 09 2021 at 03:53):

no I didn't..

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 03:53):

If not, then you can try restarting the Lean server in VS Code: hit cmd+shift+P and then search for "Lean: restart".

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 03:54):

I think sometimes opening lots of files can cause Lean to think that something has been edited.

view this post on Zulip François Sunatori (Mar 09 2021 at 03:56):

Oh I see. So is it better then to only keep one file open at a time?

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 03:58):

It usually doesn't matter too much, but I think I usually don't have more than 5 Lean files open at a time either. If you can reliably reproduce the issue, let us know; maybe there's a bug somewhere that can be fixed.

view this post on Zulip François Sunatori (Mar 09 2021 at 03:59):

Ok for now (after restarting the Lean server) it's taking forever to load...

view this post on Zulip François Sunatori (Mar 09 2021 at 04:00):

In terms of the "checking ..." settings, is there one that is preferable for performance? I guessed that "checking visible lines" might be the one taking the least time.

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:01):

I suspect some Lean files were touched or changed inadvertently. You can try stashing your work with git stash and then running leanproject get-cache to reset the compiled olean files. (And then git stash pop afterwards). If that doesn't help you might have to build mathlib yourself with leanproject build.

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:04):

You can play around with the various checking ... settings but I don't think they'll solve your issue (to be honest, I don't remember what the differences are between them). If you have the correct compiled "olean" files for mathlib, it should take only a few seconds to open any file in mathlib. Now, your file itself might have some very slow proofs, but presumably that's not what you're seeing.

view this post on Zulip François Sunatori (Mar 09 2021 at 04:07):

Ok good to know. It definitely isn't taking just a few seconds for me... even after doing leanproject get-cache

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:08):

Out of curiosity, what does git status say after you pop your changes off the stash?

view this post on Zulip François Sunatori (Mar 09 2021 at 04:09):

On branch master
Your branch is behind 'origin/master' by 12 commits, and can be fast-forwarded.
  (use "git pull" to update your local branch)

Untracked files:
  (use "git add <file>..." to include in what will be committed)

        src/analysis/complex/isometry.lean

nothing added to commit but untracked files present (use "git add" to track)

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:09):

(Also, after you run leanproject get-cache don't forget to restart the Lean server).

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:11):

If it's still slow after that, then I wonder if a file in the core Lean library got modified somehow.

view this post on Zulip François Sunatori (Mar 09 2021 at 04:11):

Oh it's so much faster now!

view this post on Zulip François Sunatori (Mar 09 2021 at 04:11):

I hadn't restarted the server after the leanproject get-cache

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:13):

OK, great! I think we should add some documentation suggesting to restart the server after running leanproject, as it seems to be a common issue.

view this post on Zulip François Sunatori (Mar 09 2021 at 04:13):

Thanks so much! I'm still new to Lean so I didn't know about leanproject get-cache.. Thanks for letting me know about it

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:14):

Yeah, there's some documentation for leanproject here: it suggests running leanproject get-mathlib-cache (which is equivalent, when run in mathlib itself).

view this post on Zulip François Sunatori (Mar 09 2021 at 04:15):

Thanks for the link... maybe I should have gone through that doc before getting too deep into Lean.. (I guess I was too impatient to start writing some Lean code!)

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2021 at 04:16):

No problem and good luck! Feel free to ask again if you have more questions.


Last updated: May 10 2021 at 00:31 UTC