Zulip Chat Archive

Stream: new members

Topic: Lean being slow


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Alena Gusakov (Nov 07 2020 at 17:48):

It works in other project directories

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 07 2020 at 18:29):

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

view this post on Zulip Adam Topaz (Nov 07 2020 at 18:30):

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

view this post on Zulip 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.

view this post on Zulip 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