Zulip Chat Archive

Stream: general

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


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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:15):

Hmm, maybe nice leanpkg build will do the job.

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:15):

Let's see if I stay responsive (-;

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:23):

Nope... on my laptop again...

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:24):

Stupid nice

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:24):

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

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:25):

the answer is always no

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:26):

Whelp... it is indeed using >7 GB

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:28):

I've got to kill some other memory hog.

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

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

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:36):

The 7 minutes... not really.

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:36):

It is still frozen to the core.

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:40):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:41):

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

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

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:43):

No, the machine is frozen.

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

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:44):

you are awfully chatty for someone with a bricked computer

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:44):

I'm on a laptop...

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:45):

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

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:45):

That shouldn't get me stuck.

view this post on Zulip Gabriel Ebner (Aug 07 2018 at 08:46):

Which branch are you on?

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:47):

map2

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

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 08:58):

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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 09:07):

isn't it time to reboot?

view this post on Zulip Johan Commelin (Aug 07 2018 at 09:08):

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

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

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 09:36):

Now the compile is running smoothly again!

view this post on Zulip Johan Commelin (Aug 07 2018 at 09:36):

I guess I need more RAM


Last updated: May 12 2021 at 23:13 UTC