Skip to content

feat: pretty print level metavariables using index#13030

Merged
kmill merged 4 commits intomasterfrom
kmill_pp_lmvars
Apr 1, 2026
Merged

feat: pretty print level metavariables using index#13030
kmill merged 4 commits intomasterfrom
kmill_pp_lmvars

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Mar 22, 2026 •
edited
Loading

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 metaprogramming change: level pretty printing should use delabLevel or MessageData.ofLevel; functions such as format or toString do not have access to the indices, since they are stored in the current metacontext. Absent index information, metavariables print with the raw internal identifier as ?_mvar.nnn. Note: The heartbeat counter also increases quicker due to counting allocations that record level metavariable indices. In some tests we needed to increase maxHeartbeats by 20–50% to compensate, without a corresponding slowdown.

@kmill kmill added the changelog-pp Pretty printing label Mar 22, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 22, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 22, 2026 •
edited
Loading

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)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1aa860af33e1aa30fb8aff6339816999e89f921b --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-04-01 14:51:25)

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 22, 2026
Update lean-toolchain for testing leanprover/lean4#13030
d3963c6
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 22, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 22, 2026
Update lean-toolchain for testing leanprover/lean4#13030
21ec250
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 22, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 22, 2026 •
edited
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-13030 build failed against this PR. (2026-03-22 02:31:47) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1aa860af33e1aa30fb8aff6339816999e89f921b --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-01 14:51:23)

@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 22, 2026

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 22, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 22, 2026

Mathlib CI status (docs):

@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Mar 22, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 22, 2026 •
edited
Loading

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-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 22, 2026
Update lean-toolchain for leanprover/lean4#13030
e66517c
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 22, 2026
Update lean-toolchain for leanprover/lean4#13030
7a0530e
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Mar 22, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 22, 2026

Mathlib CI status (docs):

@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Mar 23, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 23, 2026 •
edited
Loading

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
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 23, 2026

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 23, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 23, 2026

Mathlib CI status (docs):

kmill added 2 commits April 1, 2026 05:45
@kmill
feat: pretty print level metavariables using index
485c734 
This PR introduces level metavariable indices to the metavariable context and uses these for pretty printing level metavariables. The upshot is that level metavariables pretty print with smaller numerical suffixes, which are per-definition rather than per-module.
@kmill
add LevelMetavarDecl, see what this does to benchmarks
9dc923a
@kmill kmill force-pushed the kmill_pp_lmvars branch from 23bb157 to 9dc923a Compare April 1, 2026 13:33
kmill
kmill commented Apr 1, 2026
View reviewed changes
Comment thread src/Lean/Level.lean Outdated
@kmill
reinstate Quote Level
6b6899b 
Quoting a level is only really correct if there are no metavariables, so may as well keep it. The risk to downstream users is that they may see `?_mvar.nnn` in output.
@kmill kmill enabled auto-merge April 1, 2026 14:52
@kmill kmill disabled auto-merge April 1, 2026 19:56
kmill
kmill commented Apr 1, 2026
View reviewed changes
Comment thread src/Lean/Level.lean Outdated
@kmill kmill added this pull request to the merge queue Apr 1, 2026
Merged via the queue into master with commit 8f1c18d Apr 1, 2026
19 checks passed
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
@kmill @volodeyka
feat: pretty print level metavariables using index (#13030)
77010eb 
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 metaprogramming change:** level
pretty printing should use `delabLevel` or `MessageData.ofLevel`;
functions such as `format` or `toString` do not have access to the
indices, since they are stored in the current metacontext. Absent index
information, metavariables print with the raw internal identifier as
`?_mvar.nnn`. **Note:** The heartbeat counter also increases quicker due
to counting allocations that record level metavariable indices. In some
tests we needed to increase `maxHeartbeats` by 20–50% to compensate,
without a corresponding slowdown.
@srghma srghma mentioned this pull request Apr 21, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-pp Pretty printing mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@kmill @leanprover-bot @leanprover-radar