Visual Studio Code: performance

Stream: general

[François Sunatori]

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!

[Bryan Gin-ge Chen]

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?

[François Sunatori]

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

[Bryan Gin-ge Chen]

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

[François Sunatori]

no I didn't..

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[François Sunatori]

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

[Bryan Gin-ge Chen]

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.

[François Sunatori]

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

[François Sunatori]

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.

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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.

[François Sunatori]

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

[Bryan Gin-ge Chen]

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

[François Sunatori]

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)

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[François Sunatori]

Oh it's so much faster now!

[François Sunatori]

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

[Bryan Gin-ge Chen]

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.

[François Sunatori]

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

[Bryan Gin-ge Chen]

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

[François Sunatori]

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!)

[Bryan Gin-ge Chen]

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

[François Sunatori]

Hi, I just pulled master and ran

$ leanproject get-cache

and I got:

Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/14d71874fa87c8cf108e6f1441fb963c5363522a.tar.xz to /Users/fss/.mathlib/14d71874fa87c8cf108e6f1441fb963c5363522a.tar.xz
Failed to fetch cached oleans

am I missing something for it to be able to fetch the cached oleans?
Thanks!

[Bryan Gin-ge Chen]

What does git status say? 14d71874fa is not a commit in our mathlib repo as far as I can tell.

[François Sunatori]

oh my bad I switched to my working branch before running $ leanproject get-cache

[François Sunatori]

thanks for the hint :)