Zulip Chat Archive

Stream: general

Topic: Tips for Running Lean on Bad Hardware

Husnain Raza (Jan 22 2023 at 21:45):

I'm currently trying to run lean with vscode - however, with 8 GB of RAM, it is horrendously slow
Anyone have any tips on how to improve performance? Should I use something else besides vscode? Thanks in advance

Alex J. Best (Jan 22 2023 at 21:55):

Using vscode itself shouldn't really affect the speed of lean, and 8gb should be enough for most projects (I have an 8gb laptop too right now), though more is better of course. What sort of thing are you running and finding too slow?

Husnain Raza (Jan 22 2023 at 22:00):

I'm just trying some intro proofs - nothing too complicated as I am new to this but I frequently get this error that leads me to believe that I don't have good enough hardware

Alex J. Best (Jan 22 2023 at 22:04):

Are you working on mathlib itself? Or a project building on mathlib? Are you sure you have the project set up correctly, and downloaded mathlib oleans in that case?

Gareth Ma (Jan 23 2023 at 05:20):

Also check your bottom left, does it say "checking project files" or "checking open/visible files"? The first one nearly crashed my lapotp after starting to check 180k files

Martin Dvořák (Jan 23 2023 at 11:00):

I believe that 8 GB should be more than enough.

Last updated: Dec 20 2023 at 11:08 UTC