Error on memory consumption

Stream: general

[Morgen]

I am new to lean and leanring tutorials-master on VSCode. The program is stuck with error message "excessive memory consumption detected at 'type checker' (potential solution: increase memory consumption threshold)".

[Johan Commelin]

Welcome! How did you obtain the tutorials? Using leanproject?

[Johan Commelin]

Point is: the tutorials depend on mathlib: and if you didn't download a compiled version of mathlib, then your computer might be going crazy trying to compile mathlib while you are opening the tutorials files

[Huỳnh Trần Khanh]

Run leanproject get-mathlib-cache

[Morgen]

I obtain the tutorials by downing zip file for github. It works by Run leanproject get-mathlib-cache. Thanks a lot.

[Johan Commelin]

Aha, the recommended way is: https://leanprover-community.github.io/install/project.html#working-on-an-existing-project

[Cayden Codel]

I also ran into this issue today. Apparently it is addressed here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/memory.20usage.20with.20vscode.2C.20lean.20and.20mathlib/near/238678879