linux scheduler

Stream: general

[Johan Commelin]

Is there some way to tell the linux scheduler that it should never allow Lean to freeze my system? I want Lean to use all the available juice it can get, but as soon as something else asks for attention, that should get higher prio.

[Johan Commelin]

For example X should always be able to kill VScode

[Kevin Buzzard]

Just renice it?

[Johan Commelin]

Can this be automated?

[Johan Commelin]

As you can guess... Lean just froze my desktop machine

[Mario Carneiro]

I have to routinely set the process priority for lean to "below average" on windows so it doesn't kill vscode responsiveness (on windows)

[Johan Commelin]

Aaah, I guess RightAlt + SysRq + f is exactly what I need for these situations

[Keeley Hoek]

When this happens to me it's because my memory has been exhausted and the kernel is busy writing gigabytes to disk, and as a lazy defence I've swapoff'd the swap so the oom killer is forced to come in automatically. I think a more legit thing to do would be to ulimit the lean process, but I've never been bothered enough to do this---and recently I've bought a bucket of RAM so the problem's gone away

[Kevin Buzzard]

I have 16 gigs of ram on the desktop I'm using now and twice recently Lean has taken it down when compiling mathlib. Do you have a bigger bucket?

@Johan Commelin when I used to run big magma processes I used the ulimit trick. Maybe this is worth looking into.

[Edward Ayers]

Might help: I was having Lean freezing issues on my linux box and I found that adding more swap space at least kept the system responsive enough that I could kill Lean.

[Keeley Hoek]

Yeah kevin Lean usage inspired me to 8gb -> 32gb upgrade

[Kevin Buzzard]

Lean has taken down my 16gb system three times in the last month, and this thing never normally crashes. I'll try bumping up swap. It's pretty hideous. I go from completely fine to essentially totally unresponsive instantly, and I can't ssh in and the lights on the keyboard stop working. Funnily enough I can still move my mouse cursor, very slowly, but clicks don't seem to register

[Patrick Massot]

Why Lean needs so much RAM? I would have thought that having many CPU would be the crucial Lean speed factor

[Kevin Buzzard]

I think it's a memory leak. I think every time it happened I was compiling mathlib -- I am making a few mathlib PR's now so I edit mathlib source and then recompile before I push. It has been a change in behaviour for me -- I did not usually make mathlib PR's until recently when I felt that the perfectoid project's for_mathlib directory was getting a bit out of hand.

[Kevin Buzzard]

But it's not the classic "get slower, get slower, you know there's a problem, quick killall lean before they kill you" thing, it's an instantaneous "you are now screwed, things were working fine 1 second ago but now you just may as well reboot"

[Patrick Massot]

Yes, I've seen that too. But in this case I don't see how buying RAM could help

[Johan Commelin]

My Lean process is currently using 45% of my GB RAM. That means its very risky to run two compiles at the same time.

[Johan Commelin]

I guess leanpkg build -M 3072 might be helpful. That means that if I run two compiles in parallel, I will be sure to have 2GB left for my system.

[Johan Commelin]

Can the amount of memory for the lean server process be changed while the server is live? If so, we could have a dial for VScode where you can increase/decrease the amount of memory.

[Johan Commelin]

Is there an easy way to know the minimum amount of memory that Lean needs to compile current mathlib?

[Gabriel Ebner]

There is a configuration setting for the memory limit in the vscode extension. Any change requires a server restart though. And this limit is only enforced cooperatively: the Lean server regularly checks if it uses more memory than the limit, and raises an exception if it exceeds the limit.

[Kevin Buzzard]

And for manual compilation with lean --make I can run ulimit beforehand

[Johan Commelin]

I can confirm that RightAlt + SysRq + f can unfreeze a box and kill Lean if it turns into a RAM-hoarder.

[Edward Ayers]

Why exactly does lean need so much memory in the first place?

[Johan Commelin]

I don't know... this was on a broken project...

[Johan Commelin]

It was stuck parsing some line

[Edward Ayers]

If I compile mathlib it consumes like 4gb of ram. Does anyone know what is consuming most of that space? Is it proof terms?