Tips for Running Lean on Bad Hardware

Stream: general

[Husnain Raza]

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]

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]

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]

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]

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]

I believe that 8 GB should be more than enough.