Zulip Chat Archive

Stream: general

Topic: Tell leanpkg to use (n-1) cpu cores


Johan Commelin (Aug 07 2018 at 08:02):

Yesterday I rebuilt mathlib and it froze my desktop for > 2hrs. I would like to tell leanpkg to use only 3 of my 4 cores. I'm on Linux. Should I use fancy cgroups for this, or is there some easy method?

Johan Commelin (Aug 07 2018 at 08:15):

Hmm, maybe nice leanpkg build will do the job.

Johan Commelin (Aug 07 2018 at 08:15):

Let's see if I stay responsive (-;

Johan Commelin (Aug 07 2018 at 08:23):

Nope... on my laptop again...

Johan Commelin (Aug 07 2018 at 08:24):

Stupid nice

Gabriel Ebner (Aug 07 2018 at 08:24):

You can use lean -j3 --make. But I don't think that using all cores is the cause for your computer freezing. It's much more likely to be memory usage.

Johan Commelin (Aug 07 2018 at 08:24):

I've got 8 GB, shouldn't that be sufficient?

Mario Carneiro (Aug 07 2018 at 08:25):

the answer is always no

Johan Commelin (Aug 07 2018 at 08:26):

Whelp... it is indeed using >7 GB

Johan Commelin (Aug 07 2018 at 08:27):

No, something is off. The lean process with niceness 10 is using only 10% of my memory.

Johan Commelin (Aug 07 2018 at 08:28):

I've got to kill some other memory hog.

Johan Commelin (Aug 07 2018 at 08:29):

So, do you guys have a strategy for keeping your system responsive during rebuilds? Or you only rebuild during lunch?

Gabriel Ebner (Aug 07 2018 at 08:32):

What are you building? I know that Lean eats memory for breakfast, but mathlib takes only 7 minutes and 1.5G of RAM here.

Johan Commelin (Aug 07 2018 at 08:36):

I am trying to rebuild mathlib. The 1.5GB seems to be what my system is using as well.

Johan Commelin (Aug 07 2018 at 08:36):

The 7 minutes... not really.

Johan Commelin (Aug 07 2018 at 08:36):

It is still frozen to the core.

Johan Commelin (Aug 07 2018 at 08:40):

Might it be a problem that I launched the rebuild from a feature branch?

Johan Commelin (Aug 07 2018 at 08:41):

It only had changes in 1 file, compared to mathlib HEAD.

Gabriel Ebner (Aug 07 2018 at 08:42):

No the small change should make it faster. But maybe the change causes a by simp to time out?

Gabriel Ebner (Aug 07 2018 at 08:42):

Wait, by frozen you just mean that lean is frozen, not your whole machine? What is the last line that lean printed?

Johan Commelin (Aug 07 2018 at 08:43):

No, the machine is frozen.

Johan Commelin (Aug 07 2018 at 08:43):

I currently have a frozen top in front of me. I can't even issue a kill.

Mario Carneiro (Aug 07 2018 at 08:44):

you are awfully chatty for someone with a bricked computer

Johan Commelin (Aug 07 2018 at 08:44):

I'm on a laptop...

Johan Commelin (Aug 07 2018 at 08:45):

People have >3 devices with Zulip on it nowadays, don't they?

Johan Commelin (Aug 07 2018 at 08:45):

Ok, so the last line that lean printed says that it is making stuff on Turing machines.

Johan Commelin (Aug 07 2018 at 08:45):

That shouldn't get me stuck.

Gabriel Ebner (Aug 07 2018 at 08:46):

Which branch are you on?

Johan Commelin (Aug 07 2018 at 08:47):

map2

Johan Commelin (Aug 07 2018 at 08:48):

It is a feature branch that I'm trying to PR containing about 25 lines of changes in linear_algebra/multivariate_polynomial.lean

Gabriel Ebner (Aug 07 2018 at 08:56):

Good news! The branch builds! (Not very helpful, I know.)
Can you try rm **/*.olean and build again?

Johan Commelin (Aug 07 2018 at 08:58):

Nope, I can't... It is still frozen...

Kevin Buzzard (Aug 07 2018 at 09:07):

isn't it time to reboot?

Johan Commelin (Aug 07 2018 at 09:08):

It made a bit of progress! But it is still really slow.

Johan Commelin (Aug 07 2018 at 09:08):

I'm one of those guys that don't like to reboot a linux box. It feels like epic failure.

Johan Commelin (Aug 07 2018 at 09:35):

Yoochai! It survived. I managed to execute killall code, which closed 3 instances of VScode working on different Lean projects.

Johan Commelin (Aug 07 2018 at 09:36):

Now the compile is running smoothly again!

Johan Commelin (Aug 07 2018 at 09:36):

I guess I need more RAM


Last updated: Aug 03 2023 at 10:10 UTC