François Sunatori (Mar 09 2021 at 03:47):
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.
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?
François Sunatori (Mar 09 2021 at 03:52):
I created a short file in analysis/complex that imports
Bryan Gin-ge Chen (Mar 09 2021 at 03:52):
Did you edit any files that are imported by that file?
François Sunatori (Mar 09 2021 at 03:53):
no I didn't..
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".
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.
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?
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.
François Sunatori (Mar 09 2021 at 03:59):
Ok for now (after restarting the Lean server) it's taking forever to load...
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.
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
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.
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
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?
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)
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).
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.
François Sunatori (Mar 09 2021 at 04:11):
Oh it's so much faster now!
François Sunatori (Mar 09 2021 at 04:11):
I hadn't restarted the server after the
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.
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
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).
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!)
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