Stream: new members
Topic: Lean being slow
Alena Gusakov (Nov 07 2020 at 17:44):
I'm trying to work on a PR in VSCode and for some reason Lean isn't working for me - it just keeps loading. I've tried restarting Lean, switching to master and doing
leanproject get-cache, quitting and reopening VSCode, etc, all stuff that has worked for me in the past. I'm wondering if there is something else I can try before I start looking into whether my computer is causing the problem.
Bryan Gin-ge Chen (Nov 07 2020 at 17:46):
Are you having trouble just in one project directory or does Lean work in VS Code in e.g. another test project?
Alena Gusakov (Nov 07 2020 at 17:48):
It works in other project directories
Alena Gusakov (Nov 07 2020 at 17:50):
Okay, with the knowledge that it works in other directories, I deleted the repository and re-cloned my branch. It's working now!
Filippo A. E. Nuccio (Nov 07 2020 at 18:03):
I had a similar issue for very long and eventually realised that my Lean folder was in an automatically backing-up location (like Dropbox or Google Drive). That was creating big issues (and was totally stupid, as
git ensures all the back-up I need). I don't know if this is the case for you, but give it a look!
Alena Gusakov (Nov 07 2020 at 18:13):
Ahhh that might be it, I have my desktop set up to move stuff to my iCloud drive cause I'm constantly running out of storage space lol
Adam Topaz (Nov 07 2020 at 18:29):
I think things like Dropbox can interfere with the way lean decides which files to compile
Adam Topaz (Nov 07 2020 at 18:30):
It's based on when the lean/Olean files were created, I think
Filippo A. E. Nuccio (Nov 07 2020 at 18:31):
Yes, most of the issues came from many
olean files getting modified. I realised this when I noticed that a certain point I was committing modifications to some >4000 files, although I had worked on one file only.
Adam Topaz (Nov 07 2020 at 18:33):
As for backups, I REALLY like borg: https://www.borgbackup.org/
Last updated: May 17 2021 at 23:14 UTC