## 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?

#### 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?

#### 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: May 12 2021 at 23:13 UTC