chore: inline trace nodes

[eric-wieser]

This extracts a postCallback helper so that only the actual callback is inlined.

Part of the motivation here is to exclude these tracing frames from flame graph profiles.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 5b9e69e against e766839 are in! @Kha @eric-wieser

Runs (2🟥)

• 🟥 build exited with code -1
• 🟥 other exited with code -1

[Kha]

!bench

[leanprover-radar]

Benchmark results for 663d1e7 against e766839 are in! @Kha

Large changes (4🟥)

• 🟥 build/module/Lean.Meta.Tactic.Backtrack//bytes .olean.private: +718kiB (+102.8%)
• 🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +32.9G (+51.9%)
• 🟥 size/all/.ir//bytes: +3MiB (+0.8%)
• 🟥 size/libleanshared.so//bytes: +1MiB (+0.6%)

Medium changes (6✅, 22🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (211✅, 32🟥)

Too many entries to display here. View the full report on radar instead.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e76683934532e7fca1ade9a4a498176c2f76194b --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-09 11:30:51)
• ✅ Mathlib branch lean-pr-testing-11954 has successfully built against this PR. (2026-01-11 13:46:03) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase e76683934532e7fca1ade9a4a498176c2f76194b --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force reference manual CI using the force-manual-ci label. (2026-01-09 11:30:52)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-11 12:46:00)

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@0022380 against leanprover-community/mathlib4-nightly-testing@7c43efe are in! @Kha

No significant changes detected.