lake build parallelism limit?

Stream: new members

[Barry Moore II]

Hey, I'm new here :smiley:. Question, can I limit the parallelism when building with lake build?

[Barry Moore II]

Additional context, I was compiling mathlib and my computer was struggling. Would have been nice to just add -j 10 and save some cores for my other work

[Arthur Paulino]

You can save much more with lake exe cache get

[Michael Rothgang]

Use the above first. Only compile mathlib/files if you have to.

[Michael Rothgang]

If you need to compile a set of files, something like the j option exists. I don't remember the syntax, but @Floris van Doorn does

[Floris van Doorn]

You can use e.g. export LEAN_NUM_THREADS=10 && lake build

[Barry Moore II]

Nice. I couldn’t find that in the docs is it at all useful to add as a PR?

[Michael Rothgang]

I think it would, but I'm not sure where to add it...

[Barry Moore II]

Fair, it might also be useful to stick it into the lake build —help but then you have to decide which flags make the most sense to put there.

[Barry Moore II]

Anyway, both of these solve my immediate issues and I learned about the cache so thanks everyone!

[Floris van Doorn]

It is mentioned in the language reference: https://lean-lang.org/doc/reference/latest/IO/Tasks-and-Threads/?terms=LEAN_NUM_THREADS#concurrency

[Barry Moore II]

As a new user, I wouldn’t know to look there