Why long identifiers like ?m.344685?

Stream: new members

[Dan Abramov]

I've been wondering about this for a while. The question is: why these long scary identifiers?

Screenshot 2025-08-07 at 02.13.05.png

I get that we need to show something and we don't have names for them. But these are particularly frustrating because the number gets super long and that kind of makes them hard to scan for up and down. So you have to mentally sort of tune them out. Except that they are also some of the longest things painted on the screen. So they clutter everything up.

I was wondering whether it would be possible to partially elide them in the UI where you don't have more than 10-20 showing up at a given time (in most cases; I get that exceptions and different printing modes exist). I could imagine "local" numbering being used if these identifiers can't be relied on in code (like ?m.1 etc). Maybe a "global" system is better when debugging issues or coordinating some kind of internal representation? And maybe there's a downside to showing something different to the user (like when trying to correlate types of holes across multiple files)? I'm not sure but I would've appreciated seeing much smaller numbers on the screen.

It's also possible I'm thinking about this from the wrong end and maybe their placeholder names could've been better somehow? Like inferred from usage somehow? I'm not sure if this is a case where it's impossible to even describe the hole because we don't know anything about it, or if there's some inference of intent we could make to show a friendlier label.

[Aaron Liu]

set_option pp.mvars.anonymous false to turn off the numbers

[Aaron Liu]

I don't know of any way to make them "better" without turning them off completely

[Dan Abramov]

Yea this seems a bit too much maybe. I guess I wouldn't mind tiny colored squares with unique color per number :D

But in any case ideally, if something better can be done (e.g. short normalized numbers, or good inferred friendly labels), I'd want that to be a default rather than an option. Since options aren't very discoverable and require people to have to agree with each other.

[Kyle Miller]

We've thought about trying to do local renumbering when pretty printing. The problem is correlation across Infoview states and across messages. You don't want these things to change numbers as you go from state to state, and also you want hovers to have consistent numbering.

I have a draft PR somewhere that tries to give these more informative names, drawing the names from what the metavariable stands for, for example an argument for parameter x to a function could be represented as ?x.22. That one needs some more work though.

The internal detail here is that every metavariable has a "metavariable ID" (or "mvarid") that's of the form _uniq.nn where nn is a number drawn from a source of fresh numbers. The number generator is reset at the beginning of each file. When pretty printing, if there's no registered name for the metavariable, then a metavariable with mvarid _uniq.22 gets pretty printed as ?m.22. Metavariables don't survive across modules, or even across commands, so it should be safe to reset this generator per command, but the generator is also shared by a couple other features, and I'm not sure whether or not it's safe to reset it for them. There probably should be an option to keep the current behavior at least, to help catch caching bugs that accidentally use metavariables across multiple commands.

[Kyle Miller]

Maybe there's a way to improve things without touching the name generator.

The "metavariable context" is what keeps track of metavariable declarations and their assignments. It already keeps track of a metavariable index, which is independent of the mvarid. The pretty printer could easily print that instead, and each command starts with an empty metavariable context.

[Kyle Miller]

lean4#9778 implements this for expression metavariables

It doesn't do anything for universe metavariables (e.g. in Sort ?u.123123) because they don't have indices. Maybe later.

[Kyle Miller]

It's kind of nice, no matter where you are in a file, the same small metavariable numbers!

#check _
-- ?m.2 : ?m.1

[Kyle Miller]

I wonder if it would be nice to pretty print these as ?m¹²³ instead of ?m.123. Superscripts to match how hygienic names pretty print (x✝¹). It saves one character, and also it's a bit less prominent.

[Dan Abramov]

Thanks!

I have a draft PR somewhere that tries to give these more informative names, drawing the names from what the metavariable stands for, for example an argument for parameter x to a function could be represented as ?x.22. That one needs some more work though.

I wonder if it would be nice to pretty print these as ?m¹²³ instead of ?m.123. Superscripts to match how hygienic names pretty print (x✝¹). It saves one character, and also it's a bit less prominent.

I'm in favor of both of these!