Lean eats 6 GB of RAM on WSL in Windows

Stream: lean4

[Yongyi Chen]

I originally posted about this issue here, but I think it's important enough to deserve its own thread.

For comparison, for Lean running on Windows itself and on actual Linux, the memory usage is around a modest 1-2 GB.

[Sebastian Ullrich]

Does the consumption double if you open two files with the same imports or is this merely different measures of shared .olean pages?

[Yongyi Chen]

It doesn't double if I open two files with the same imports.

[Sebastian Ullrich]

Then I wouldn't worry about it

[Yongyi Chen]

OK, I was looking in the wrong place when checking Linux -- WSL and Linux both report 6 GB usage. So it's not a bug as I thought. I'll still say the RAM usage can be optimized but I don't know enough about compilers and language servers to really say anything about that.