Catastrophic performance issue leading to lockup

Stream: lean4

[Wrenna Robson]

In the github repo linesthatinterlace/controlbits, in the file ArrayPerm.lean, I've recently done what felt like a fairly minor refactor, adding a GetElem instance for the type I define there. Now I'm getting catastrophic performance issues, like full on "my file is locking up and I have to force a computer reboot" issues which looks like it's totally consuming all my memory, and I do not understand why. It's very difficult to diagnose or fix the issue because of the lockups. I would really appreciate any urgent help with this - I'm tearing my hair out at it! I could probably walk back the refactor slowly but it'll be pretty hard to do.

At a minimum if there's a way to stop Lean evaluating the whole file and instead type checking line by line, that might help with diagnosis.

[Sebastian Ullrich]

Which OS are you on? On Linux, it is relatively easy to limit memory usage of a process (tree)

[Wrenna Robson]

Linux

[Wrenna Robson]

It would be good to understand why it's running out of memory suddenly but I'll take that too.

[Sebastian Ullrich]

Having your system still available when that happens seems like a good first debugging step to me :) . Something like (ulimit -v 4000000; code .) for a 4GB limit might work, but I haven't tried. Just make sure it's not reusing any existing VS Code process.

[Wrenna Robson]

My computer is now not restarting (!)

[Wrenna Robson]

Really XKCD shark comic hours over here

[Wrenna Robson]

I'm wondering if it's to do with the VS code update that just dropped somehow

[Wrenna Robson]

I would be grateful to see if the performance issues replicate on other machines. I thought I'd fixed this before I went to bed last night but now on my work computer they're recurring.

[Wrenna Robson]

I have enabled Magic SysReq out-of-memory killing which ought to help

[Wrenna Robson]

rather than hard REISUBing it

[Shreyas Srinivas]

Is this related to lean4#4920 ?

[Wrenna Robson]

Hmm, interesting. I think I've tracked it down to one of my definitions - I think it was having to run get_elem_tactic every time and that was causing slowness... we'll see if giving the proof term directly has fixed it

[Wrenna Robson]

Shreyas Srinivas said:

Is this related to lean4#4920 ?

I can't see an obvious link but it is in an adjacent area.