perf: avoid spawning a new thread per worker output message

[Kha]

Also reduces number of samply tracks for re-elab tests from ~3000 to ~40

[Kha]

!bench

[leanprover-radar]

Benchmark results for 776f9fb against 08c8b6a are in. No significant results found. @Kha

• 🟥 build//instructions: +207.6M (+0.00%)

Medium changes (1🟥)

• 🟥 misc/re-elab Init.Data.BitVec.Lemmas//instructions: +79.9G (+9.85%)

Small changes (5✅, 2🟥)

• ✅ build/profile/grind dsimp//wall-clock: -7ms (-58.32%)
• ✅ elab/bv_decide_realworld//wall-clock: -53ms (-4.47%)
• ✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -5s (-5.26%)
• ✅ misc/re-elab Init.Data.List.Basic//task-clock: -1s (-7.53%)
• 🟥 misc/re-elab Init.Data.List.Sublist//instructions: +8.1G (+5.79%)
• ✅ misc/re-elab Init.Data.List.Sublist//task-clock: -1s (-5.80%)
• 🟥 misc/re-elab watchdog Init.Data.List.Sublist//instructions: +9.7G (+2.04%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 08c8b6a4546e37a66c1b90cf12f7572216faf38d --onto 0758b1d2e33c65ccea578abb0c668aab1f811608. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-25 21:36:28)

[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 08c8b6a4546e37a66c1b90cf12f7572216faf38d --onto 2e72131c7f007ab9d2538b676106c5141b24ba22. You can force reference manual CI using the force-manual-ci label. (2026-06-25 21:36:29)

[Kha]

Instructions increases might be from additional parallelism? Certainly look harmless when all -clocks are pointing in the right direction

[Kha]

Tangentially, it would probably make sense to avoid the JSON roundtrip in at least this case at it happens so often