lean --make

Stream: general

[Johan Commelin]

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]

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

[Chris Hughes]

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]

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]

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]

That's with 8 threads?

[Gabriel Ebner]

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

[Johan Commelin]

[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]

did that actually take an hour or 7 minutes

[Johan Commelin]

7m39

[Johan Commelin]

The user time is measured across all cores and threads.

[Mario Carneiro]

have you tried running with the -j option?

[Johan Commelin]

How would -j help?

[Johan Commelin]

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

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

[Johan Commelin]

[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]

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

[Mario Carneiro]

I'll get back to you in an hour

[Mario Carneiro]

$ time lean --make

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

windows

[Mario Carneiro]

running MSYS2

[Kenny Lau]

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

[Reid Barton]

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]

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

[Reid Barton]

Interesting. I think I was using 3.4.1.

[Kenny Lau]

I already git pulled

[Mario Carneiro]

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

[Mario Carneiro]

I think the terminal detection is broken