Zulip Chat Archive

Stream: new members

Topic: non decreasing memory usage


view this post on Zulip Lucas Viana (Jun 16 2020 at 18:42):

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?

view this post on Zulip Jalex Stark (Jun 16 2020 at 18:46):

you can restart lean from within vscode

view this post on Zulip Jalex Stark (Jun 16 2020 at 18:48):

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

view this post on Zulip Jalex Stark (Jun 16 2020 at 18:49):

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)

view this post on Zulip Jalex Stark (Jun 16 2020 at 18:50):

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

view this post on Zulip Pedro Minicz (Jun 16 2020 at 21:53):

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?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:08):

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

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:08):

I fixed freezes by creating some swap space

view this post on Zulip Bryan Gin-ge Chen (Jun 16 2020 at 22:16):

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.

view this post on Zulip Reid Barton (Jun 16 2020 at 22:17):

I thought it was limited by default.

view this post on Zulip Bryan Gin-ge Chen (Jun 16 2020 at 22:19):

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

view this post on Zulip Rob Lewis (Jun 16 2020 at 22:22):

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.

view this post on Zulip Rob Lewis (Jun 16 2020 at 22:23):

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? ;) )

view this post on Zulip Rob Lewis (Jun 16 2020 at 22:24):

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.

view this post on Zulip Reid Barton (Jun 16 2020 at 22:39):

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.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 22:59):

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

view this post on Zulip Pedro Minicz (Jun 17 2020 at 00:54):

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.

view this post on Zulip Lucas Viana (Jun 17 2020 at 02:13):

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.

view this post on Zulip Lucas Viana (Jun 17 2020 at 02:15):

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)

view this post on Zulip Lucas Viana (Jun 17 2020 at 02:16):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 17 2020 at 02:16):

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

view this post on Zulip Yakov Pechersky (Jun 17 2020 at 17:56):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 17 2020 at 17:59):

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

view this post on Zulip Yakov Pechersky (Jun 17 2020 at 18:01):

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

view this post on Zulip Yakov Pechersky (Jun 17 2020 at 18:01):

I'll try setting memory limit to 1024 MB

view this post on Zulip Yakov Pechersky (Jun 17 2020 at 18:01):

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


Last updated: May 14 2021 at 07:19 UTC