Zulip Chat Archive

Stream: general

Topic: lean killed my machine


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 19 2019 at 16:16):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip matt rice (Apr 19 2019 at 17:23):

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

view this post on Zulip 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: May 18 2021 at 16:25 UTC