lake tracing

Stream: lean4

[Chris Lovett]

many other build systems provide a verbose trace of every command line being invoked, like make --trace. Does Lake have something like that? I'm trying to debug something and a trace of all command might be useful...

[Henrik Böving]

Doesn't lake print this trace already per default? When I run a lake build from scratch I see a lean compiler invocation per file and the final one that links things together

[Mac]

Yeah, as Henrik says, that should be default. My future goal in this regard has been to do the opposite (print a nice file by file percent progress without the verbose trace as the new default).