Commit 2025-01-11 10:05 3a798ee6
View on Github →feat: use scoped trace nodes in linarith (#19855) Inspired by hacking done with @robertylewis and @hrmacbeth which resulted in #19771. The effect is that the traces messages are now hierarchical; though it's easy not to notice in VSCode without a better version of https://github.com/leanprover/lean4/pull/6345. See https://profiler.firefox.com/public/smkc5ffh9318w177gps2x9e5b6wy117s6f18e6g/flame-graph/?globalTrackOrder=0&thread=0&transforms=ff-2659&v=10 for an example output produced with
lake lean MathlibTest/linarith.lean -- \
-Dtrace.profiler=true \
-Dtrace.profiler.threshold=1 \
-Dtrace.profiler.output.pp=true \
-Dtrace.profiler.output=linarith-profile.json
Some inconclusive discussion about best practices for withTraceNode
is on Zulip here.