memory leak in tactic mode

Stream: mathlib4

[Sky Wilshaw]

I've been occasionally encountering problems while writing proofs where my memory usage will increase over the course of a couple of minutes even with no user input, and I need to restart VSCode otherwise my computer softlocks from trying to move all of the memory to my HDD. The leak is consistent - if I restart VSCode and don't change my proof, the same leak will occur. I have no idea how to make a #mwe, does anyone else have this issue?
image.png

[Sky Wilshaw]

Even if I replace the proof with sorry it seems like some background lean.exe task is continuing to process anyway and use up memory.

[Alex J. Best]

What is the smallest / simplest file you see this behaviour on? (an empty file, a file with one check statement, a file with one nontrivial proof, a file with an import, a file importing something from mathlib, etc.) thats the way to make a #mwe to help isolate this

[Sky Wilshaw]

I've only encountered this problem in one file, in a pretty large project, pulling in quite a few imports. The proofs heavily depend on Lean unifying a lot of things.

[Sky Wilshaw]

That's why I'm mostly asking if anyone else has the same problem, at least to find mitigations.

[Alex J. Best]

My lean/vscode does eat a lot of memory, I never stopped to observe if there was a clear leak like this, but I normally keep a terminal open somewhere ready to type pkill lean if the computer gets choppy.

[Kevin Buzzard]

Is this Lean 3 or Lean 4? I only ask because I know you've been working on a Lean 3 project for a while.

[Sky Wilshaw]

Lean 4 - I'm almost done porting the project in question to Lean 4 and this is stopping me from finishing it.

[Sky Wilshaw]

I can work around the problem somewhat by being very careful with when I tell Lean to unify complicated things. But I'm not sure why there's some background process running when I've already killed the proof term.

[Sky Wilshaw]

I feel like I'm playing a game against a time bomb, I only get about 3 minutes of programming time before everything needs a reset (which takes about 2 minutes).

[Alex J. Best]

In that case I really think it would be worth your time to try to find a mwe so someone can try and diagnose and suggest workarounds or maybe even fix this

[Sky Wilshaw]

I believe that the hanging only occurs when a subgoal is closed, regardless whether an actual proof or just a sorry was given. If I solve the goal then insert another tactic (which Lean complains about, since there are no goals), the program does not hang.

[Sky Wilshaw]

Is Lean perhaps trying to unify the type of its generated proof term with my problem statement, and running into some kind of loop?

[Sky Wilshaw]

The problem's fixed. I added in a change that wasn't needed in Lean 3, but adding it seems to satisfy the new kernel. I think the defeq checking was being a bit too powerful or something?

[Sky Wilshaw]

Sorry I couldn't make a mwe, if I get this problem in a simpler context I'll see what's possible.

[Bhavik Mehta]

Is there a way to limit how much memory Lean 4 is using like we could in Lean 3? I've also experienced memory leaks like this

[Sky Wilshaw]

I don't seem to experience this problem on Linux, only Windows.

[Scott Morrison]

This is happening while you're editing the proof in VSCode, right? We certainly had a problem in the past that old elaborations were not being killed as you kept typing, and I forget if this still happens or has been definitively fixed. This can result in linear (in keystrokes, essentially) growth of memory and CPU demand up until the point that old elaborations start finishing (assuming they ever do).

[Sky Wilshaw]

This sounds exactly like what's happening!

[Sky Wilshaw]

Although the memory would keep increasing even with no user input once I'd typed a certain prompt that caused it to loop infinitely in the background. I'm not sure if that'ssomething you've observed in that case too?

[Sky Wilshaw]

I have seen in general that as I keep editing a proof (in Windows, I don't know if this happens on Linux), my memory usage goes up, but once the definition is certified the memory usage seems to drop.

[Anne Baanen]

Bhavik Mehta said:

Is there a way to limit how much memory Lean 4 is using like we could in Lean 3? I've also experienced memory leaks like this

I assume you're asking for Windows, but on Linux I use cgroups to limit the total amount of memory all Lean processes together are allowed to use: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Elan.20cgroup.20hacks

[Sebastian Ullrich]

Scott Morrison said:

We certainly had a problem in the past that old elaborations were not being killed as you kept typing, and I forget if this still happens or has been definitively fixed.

No, that hasn't been addressed yet

[Sky Wilshaw]

Anne Baanen said:

on Linux I use cgroups to limit the total amount of memory all Lean processes together are allowed to use

I use Linux as well, thanks for the suggestion!