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: Dec 20 2023 at 11:08 UTC