lake build takes a long time

Stream: new members

[Kajani Kaunda]

New to LEAN. So I run the following commands on the MSDOS prompt. lake new test math; lake build; the command lake build is taking a long time even for my slow machine. is it because mathlib is big?

[Notification Bot]

A message was moved here from #mathlib4 > (simp) normal forms for expressions about Filters by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Kajani Kaunda Please don't post to random topics. Did you run lake exe cache get?