feat: pretty print level metavariables using index

[kmill]

This PR improves pretty printing of level metavariables: they now print with a per-definition index rather than their per-module internal identifiers. Furthermore, + is printed uniformly in level expressions with surrounding spaces. Breaking change: level pretty printing should use delabLevel or MessageData.ofLevel, since functions such as format or toString will now print metavariables with raw internal identifiers, as the indices are stored in the current metacontext. The heartbeat counter also increases quicker from counting allocations recording level metavariable indices. In some tests we needed to increase maxHeartbeats by 20–50% to compensate, without observing a slowdown.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-19 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-03-22 02:27:26)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13030 build failed against this PR. (2026-03-22 02:31:47) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-13030 built against this PR, but testing failed. (2026-03-22 16:12:44) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13030 has successfully built against this PR. (2026-03-22 18:24:16) View Log

[kmill]

!bench

[leanprover-radar]

Benchmark results for 0f5705a against 87180a0 are in. Significant changes detected! @kmill

• 🟥 build//instructions: +23.1G (+0.19%)

Medium changes (2🟥)

• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +2.3G (+1.95%) (reduced significance based on absolute threshold)
• 🟥 elab/big_do//instructions: +63.5M (+0.26%)

Small changes (76🟥)

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

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13030 build failed against this PR. (2026-03-22 23:11:46) View Log

[kmill]

!bench

[leanprover-radar]

Benchmark results for 23bb157 against 87180a0 are in. There are no significant changes. @kmill

• 🟥 build//instructions: +3.6G (+0.03%)

Small changes (5✅, 7🟥)

• 🟥 build/module/Lean.Level//instructions: +156.2M (+1.51%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Meta.AppBuilder//instructions: -40.3M (-0.43%)
• ✅ build/module/Lean.Meta.LevelDefEq//instructions: -48.8M (-2.00%)
• ✅ build/module/Lean.Meta.Tactic.Contradiction//instructions: -54.0M (-0.96%)
• ✅ build/module/Lean.Meta.Tactic.Grind.MatchCond//instructions: -52.7M (-0.30%)
• ✅ build/module/Lean.Meta.Tactic.Simp.Main//instructions: -55.7M (-0.26%)
• 🟥 build/module/Lean.MetavarContext//instructions: +80.7M (+0.78%)
• 🟥 build/module/Lean.PrettyPrinter.Delaborator.Basic//instructions: +97.6M (+1.37%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.PrettyPrinter//instructions: +44.6M (+1.91%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Util.PPExt//instructions: +68.2M (+4.92%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +41.6M (+0.17%)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +186.2M (+0.16%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13030 build failed against this PR. (2026-03-23 01:25:24) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13030 has successfully built against this PR. (2026-03-23 02:34:32) View Log