Memory consumption

Stream: new members

[Martin Dvořák]

I am building a project of circa 10k lines and lean.exe is using more than 11 GB of my RAM. Is it normal?

[Martin Dvořák]

Actually it is even more because it is swapping to my SSD now.

[Floris van Doorn]

Depending on what you do, this is the expected behavior. This is the case especially if you import large parts of mathlib, since all (compiled versions of) imported files are loaded in your RAM, I believe.

I think that Lean 4 will be better w.r.t. memory management (only loading the imported files in memory that you use).