Zulip Chat Archive

Stream: general

Topic: lean killed my machine

Kevin Buzzard (Apr 19 2019 at 16:06):

The perfectoid project is now 11,000 lines long. A couple of times recently I have idly typed "lean --make" to compile it, and brought my (16 gigs of ram) machine down -- it becomes unresponsive, the keyboard lights don't work and I can't ssh into it, and I've had to reboot. More recently (I'm on Ubuntu) I've been typing ulimit -Sv 8000000 in the terminal window I use to compile the project, and this stopped the problem occurring until today, where I wasn't even compiling: VS Code just decided to recompile a few files and my system was taken down again.

I am on Ubuntu 18.04 with no swap (because I have an SSD). I am wondering whether enabling swap will give me extra time to survive the next time this happens; I have an external HDD drive now.

Kenny Lau (Apr 19 2019 at 16:16):

I mean every time I run Lean my laptop turns scorching hot

Kevin Buzzard (Apr 19 2019 at 16:17):

Yes but that just means it's using all the cores. Lean shouldn't take your system down; that means it's filled all the memory.

Kevin Buzzard (Apr 19 2019 at 16:18):

Now when this happens Lean will start using my swap space, so I'll hear the external HD fire up and start going like crazy, and that will be the signal to kill everything.

matt rice (Apr 19 2019 at 17:23):

could try https://github.com/rfjakob/earlyoom

Kevin Buzzard (Apr 19 2019 at 17:27):

Well, I now have a 4GB swapfile on my external hard drive. Let's see how things go now. I like the look of earlyoom though.

Last updated: Aug 03 2023 at 10:10 UTC