lean in gitpod: excessive memory consumption

Stream: general

[Bernd Losert]

I trying to use a gitpod to work on my project, but I keep getting "excessive memory consumption". I can run lean on my files just fine though. I guess this is a problem with the lean extension in vscode?

[Eric Wieser]

I've seen this a bunch too - usually restarting lean works

[Eric Wieser]

In some files though, it seems there's just not enough memory available on gitpod to give to the language server

[Bernd Losert]

I closed the tab and opened it again. That did fix it.

[Bernd Losert]

Those pods have 64 GB of memory though.

[Eric Wieser]

Hmm, maybe either a memory leak or a weird vscode default setting then