Bulding Mathlib4

Stream: general

[Rudy Peterson]

Hello,

I have been working on different branches of mathlib4, and when I need to rebase and rebuild with lake build it's quite slow on my machine.

Is there a way to give the build script more cores, like lake build -j17 or something?

Sorry if this has een addresses already somewhere before.

Thanks!

[Ruben Van de Velde]

Doesn't it use them all already? Most people let CI deal with it and use lake exe shake

[Rudy Peterson]

What do you mean?

[Kevin Buzzard]

You can push to a branch of mathlib, have a cup of tea, and then do lake exe cache get and someone else's machine does the work for you.

[Kevin Buzzard]

(I conjecture that Ruben misspoke because I've been talking about shake in another thread)

[Rudy Peterson]

Thanks @Kevin Buzzard !

lake exe cache get followed by lake build is awesome!

[Rudy Peterson]

How well does this work when you make local changes to something deep in the dependency graphy, like in the Lists modules, push it to mathlib4 then do lake exe cache get.

This is still taking a long time for me...

[Kevin Buzzard]

Sure, mathlib takes a while to build, you can't expect miracles. Did you remember the "have a cup of tea" step? The other approach is to buy a super-high-spec machine.

[Kevin Buzzard]

After you push, you can watch the progress of your branch building on github.com

[Rudy Peterson]

Ha ha, fair :smile:

[Rudy Peterson]

This is an awesome feature for sure!

[Rudy Peterson]

I just wanted to make sure I wasn't missing something or doing something wrong :sweat_smile:

[Ruben Van de Velde]

Kevin Buzzard said:

(I conjecture that Ruben misspoke because I've been talking about shake in another thread)

I didn't even realise I got it wrong until you pointed it out :see_no_evil: