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.

Estimated changes