lean killed my machine

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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.