Speeding up compilation

Stream: lean4

[Leni Aniva]

I have a Lean library and some of the files take a long time to compile. These files don't contain many tactics and are metaprogramming heavy. Is there a way to speed up compilation? Is there a way to check which part of the code takes so long to compile.

[Henrik Böving]

You can use set_option trace.profiler true to get a first picture