lake build limit cores

Stream: new members

[Jakub Nowak]

Is there an option to limit the number of cores lake build uses? Building mathlib takes a few hours, and because it uses all threads it makes my desktop unrensponsive. Tried lake build -j10 but it didn't work.

[Jireh Loreaux]

Do you know about the cache? Generally you don't build all of Mathlib yourself.

[Jireh Loreaux]

lake exe cache get

[Jakub Nowak]

I did run this command. Even with this lake build takes a few hours.

[Jakub Nowak]

It shouldn't build anything with the cache downloaded?

[Damiano Testa]

It should only build files that are not from mathlib.

[Jakub Nowak]

I just built clean repo.

[Jakub Nowak]

So I guess that means cache isn't working for me?

[Damiano Testa]

I imagine so: running lake build on a project with a successfully downloaded cache should zoom by the mathlib files and then spend time on your local files.

[Damiano Testa]

Try using lake exe cache get! and see if that helps.

[Damiano Testa]

The ! forces redownloading files, even if they are already there (or some approximation to this).

[Jakub Nowak]

I removed .lake and run lake exe cache get! and now it works! Thanks!

[Jakub Nowak]

I also remember, that when I created new project depending on mathlib in vscode, it was also compiling mathlib for a few hours. Does the cache also works when mathlib is dependency, and does vscode downloads it automatically?

[Michael Rothgang]

Yes, the cache also works when mathlib is a dependency --- but right now, it only works for mathlib files. (My understanding is that this will change in the future.)