recompiling mathlib

Stream: general

[Johan Commelin]

Say that I make a change in X.lean. This might make Lean think that 50% of mathlib needs to be recompiled. But I'm convinced that 99% of all potential errors will occur in a file containing the string zero. So I run

rg -l zero

which returns a list of files that contain zero. This is again, say, 50% of mathlib. But the overlap is presumably only 25%. How do I figure out this overlap, so that I can pass it to lean --make and find my errors faster?

[Yakov Pechersky]

Is there a way to get lean to say which files it will touch to compile? Probably not until it actually does the compilation

[Reid Barton]

If Lean doesn't think it needs to recompile some file then recompiling it should be fast.

[Reid Barton]

But most likely your 50% of files containing zero will collectively import ~90% of mathlib

[Yakov Pechersky]

rg -l zero | xargs -I{} lean --make {}

to make those files.
Really, you want something like

lean --which-files-need-recompilation-bfs-order | rg zero | xargs -I{} lean --make {}

[Johan Commelin]

But if you pass it explicitly to lean --make it will ignore the olean, right? I think that at least matches my anecdotal experience.

[Eric Rodriguez]

I don't think so, from a quick test with a slow file

[Johan Commelin]

Hmm, then I must be an impatient person :see_no_evil:

[Julian Berman]

(GNU parallel should be faster than xargs since I think lean --make is single-core by default. [xargs does have a crappy -P but yeah parallel ftw]) -- e.g. rg -l zero | parallel lean --make {}

[Eric Rodriguez]

I thought it launched system threads+2 as default? You can pass lean --make -j (number) instead, I think that's better because if not some of those parallel invocations are surely going to tread on each others' toes

[Julian Berman]

I thought I tried -j with make yesterday and it ignored it... /me tries again

[Julian Berman]

Yeah here it ignores it I think. And I only get 1 CPU used (both with and without it)

[Eric Rodriguez]

that's weird, are you on your mobile setup?

[Julian Berman]

No this is on my laptop -- for you you get multicore?

[Julian Berman]

Aha, interesting, at some different point in the compilation now it's using multiple cores, but not consistently saturating them

[Eric Rodriguez]

image.png

[Eric Rodriguez]

yeah, it depends whether files are needed or not. if everything needs logic/basic it has to compile that first and i'm not sure how coarse the threading is on a file like that

[Julian Berman]

Aha.