non decreasing memory usage

Stream: new members

[Lucas Viana]

Hi!

I am using Lean with the vscode extension on linux, with compiled mathlib etc. I have no problems when I am editing a few files, even when I use imports from mathlib. But after a few minutes/hours of editing my files and pressing F12 to open the source of stuff, the lean process memory is consuming 30%-40% of my (8GB) memory, and even if I close all the vscode tabs the memory usage never goes down. So I have to periodically kill and restart the lean process. Is this normal? Is there something I can do?

[Jalex Stark]

you can restart lean from within vscode

[Jalex Stark]

ctrl-shift-p "restart lean" should find it

[Jalex Stark]

i think these issues are common, but if you have things set up correctly, then restarting lean is actually not so expensive (so the common solution is just to restart lean when there's an issue)

[Jalex Stark]

I don't have any insights in to the nature of the problem, but it's probably the sort of thing where working on it for Lean 3 is duplicating efforts of the Lean 4 folks

[Pedro Minicz]

I am also having this problem. But in my case Lean is consuming so much memory my computer eventually freezes. Is there a way to limit the amount of memory used by the server?

[Kevin Buzzard]

There's a -M switch which you can tell VS Code to use. I remember but having much success with it though

[Kevin Buzzard]

I fixed freezes by creating some swap space

[Bryan Gin-ge Chen]

It is possible that there is some bug that can be fixed. Is there a reliable way of reproducing this? e.g. a list of steps that someone can take to get the memory usage to go up by X GB over and over.

[Reid Barton]

I thought it was limited by default.

[Bryan Gin-ge Chen]

We've discussed the -M flag before, see this post. If it's not working, that's a problem.

[Rob Lewis]

I've definitely seen Lean eat up all my memory and lock up my computer. It happened a lot when I was working on linter stuff and had multiple copies of mathlib in memory at once. I suspected at the time that there was a memory leak with opening and closing many different files in the same VSCode session. But I never spent the time to find a reliable way to reproduce it.

[Rob Lewis]

This kind of memory issue is above my paygrade, but if anyone is interested in investigating, I can try again to find a way to reproduce it. (@Gabriel Ebner if you're feeling bored? ;) )

[Rob Lewis]

But generally, restarting the Lean server will clean things up. I have that bound to a hotkey and hit it now and then out of instinct.

[Reid Barton]

If you have multiple copies of mathlib open, maybe they correspond to multiple lean server processes (with different LEAN_PATHs, or even different versions of Lean) each separately limited to 4G or whatever it is.

[Kevin Buzzard]

I'm not as much of a pro as Rob, I only ever have one VS Code open and no command line lean running, and I've still seen lean take down my work computer with 8 gigs -- indeed this was commonplace earlier this year and the -M flag wouldn't fix it for me. In the end I just used my laptop when at work. 16 gigs is enough for me

[Pedro Minicz]

Reid Barton said:

I thought it was limited by default.

I was going to follow @Kevin Buzzard's advice, but noticed that -M 4096 is set by default for me.

[Lucas Viana]

I have just tested the memory limit and it is working; here it was set to 4GB too but when things start moving to swap my computer freezes. It seems to me that the vscode extension keeps the files you closed "in cache", so if you reopen them there is no need to check them again. But to me this can turn into a problem when I peek and close multiple files from mathlib in the same session.

[Lucas Viana]

I made lean use all the 4GB limit just by opening and closing random mathlib files (when I open them, lean does the checking even if I have them compiled in the project)

[Lucas Viana]

It would be useful if I could disable the checking of files inside the mathlib folder

[Bryan Gin-ge Chen]

There's the --old command line option (in Lean 3.10.0c and newer), which might help with this.

[Yakov Pechersky]

I've been getting complete computer freezes recently with VSCode and Lean as well.

[Bryan Gin-ge Chen]

Does it just happen when you have a lot of files open?

[Yakov Pechersky]

I have 3 files open, only 1 mathlib file, and the extension is set to check visible files

[Yakov Pechersky]

I'll try setting memory limit to 1024 MB

[Yakov Pechersky]

If that won't work, I'll try remote VSC on a DigitalOcean droplet