Zulip Chat Archive

Stream: general

Topic: lean --make


Johan Commelin (Aug 15 2018 at 17:29):

When I rebuild mathlib, I get the impression that it is recreating olean files for all lean files, even if they (and their dependencies) were not touched since the last build. Is that impression correct?

Gabriel Ebner (Aug 15 2018 at 17:32):

Only touched files will be recompiled. Touched = changed modification time.

Chris Hughes (Aug 15 2018 at 17:35):

I think it recompiles anything that depends on a file that changed, so if there's a change in nat.basic that pretty much means everything is recompiled.

Johan Commelin (Aug 17 2018 at 05:19):

time leanpkg build
configuring mathlib 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    70m6.346s
user    135m39.224s
sys     0m24.410s

Is this normal? This is on my (t)rusty Thinkpad X61 with > 3GB of free RAM. Does this mean I'm doomed to replace it?

Gabriel Ebner (Aug 17 2018 at 06:30):

It only takes 7 minutes here. This is with a i7-6700K and 16G RAM (not that it matters).

± time leanpkg build
configuring mathlib 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .
3200.96user 8.01system 7:18.76elapsed 731%CPU (0avgtext+0avgdata 1617680maxresident)k
37824inputs+53080outputs (77major+2781504minor)pagefaults 0swaps

Johan Commelin (Aug 17 2018 at 06:31):

That's with 8 threads?

Gabriel Ebner (Aug 17 2018 at 06:33):

The cpu has only 4 cores. Each core can run two threads (via hyperthreading), but that doesn't improve performance by much.

Johan Commelin (Aug 18 2018 at 11:52):

[jmc@atarrimbo mathlib]$ time leanpkg build
configuring mathlib 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
> lean --make .

real    7m39.967s
user    102m20.003s
sys     0m46.845s

That's on my (still rather ancient) server with 8 cores. I'll see if I can offload compilation to this mammoth.

Mario Carneiro (Aug 18 2018 at 11:52):

did that actually take an hour or 7 minutes

Johan Commelin (Aug 18 2018 at 11:53):

7m39

Johan Commelin (Aug 18 2018 at 11:53):

The user time is measured across all cores and threads.

Mario Carneiro (Aug 18 2018 at 11:53):

have you tried running with the -j option?

Johan Commelin (Aug 18 2018 at 11:53):

How would -j help?

Johan Commelin (Aug 18 2018 at 11:55):

[jmc@atarrimbo mathlib]$ echo $((7*16))
112

So there were 16 threads running almost full-time for 7 minutes.

Johan Commelin (Aug 18 2018 at 11:59):

[jmc@atarrimbo mathlib]$ cat /proc/cpuinfo | grep name | uniq
model name      : Intel(R) Xeon(R) CPU           E5540  @ 2.53GHz

I guess these are about 10 years old. All those modern i7's probably beat 4 of these hands-down. And I have only 16 of them. So if you have a quad-core...

Johan Commelin (Aug 18 2018 at 12:00):

Mario, did you ever time a fresh build of mathlib on your hardware?

Mario Carneiro (Aug 18 2018 at 12:03):

I'll get back to you in an hour

Mario Carneiro (Aug 18 2018 at 13:07):

$ time lean --make

real    18m43.275s
user    0m0.000s
sys     0m0.015s

Mario Carneiro (Aug 18 2018 at 13:10):

I have 2 cores, 4 logical processors @ 2.90 GHz on my laptop

Johan Commelin (Aug 18 2018 at 13:17):

Ok cool. But why is user equal to 0? What OS do you have?

Mario Carneiro (Aug 18 2018 at 13:24):

windows

Mario Carneiro (Aug 18 2018 at 13:25):

running MSYS2

Kenny Lau (Nov 01 2018 at 11:03):

I wish lean --make could have some debugging output, like at least how many files have been compiled

Reid Barton (Nov 01 2018 at 13:01):

It actually does print a bunch of output, just apparently not on Windows? I was really confused when I tried Lean on a Windows machine for the first time and lean --make was silent

Chris Hughes (Nov 01 2018 at 13:05):

It prints a bunch of output on my windows machine with the latest nightly. With April nightly it didn't

Reid Barton (Nov 01 2018 at 13:08):

Interesting. I think I was using 3.4.1.

Kenny Lau (Nov 01 2018 at 14:25):

I already git pulled

Mario Carneiro (Nov 01 2018 at 15:20):

I have to use winpty lean --make on msys2 to get output

Mario Carneiro (Nov 01 2018 at 15:21):

I think the terminal detection is broken


Last updated: Dec 20 2023 at 11:08 UTC