Lean being slow

Stream: new members

[Alena Gusakov]

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]

Are you having trouble just in one project directory or does Lean work in VS Code in e.g. another test project?

[Alena Gusakov]

It works in other project directories

[Alena Gusakov]

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]

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]

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]

I think things like Dropbox can interfere with the way lean decides which files to compile

[Adam Topaz]

It's based on when the lean/Olean files were created, I think

[Filippo A. E. Nuccio]

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]

As for backups, I REALLY like borg: https://www.borgbackup.org/