Predictable meta numbering?

Stream: lean4

[David Thrane Christiansen]

While attempting to describe Lean output in a predictable and testable way, I'm running into a challenge with implicit polymorphic arguments.

My technique so far has been to use a macro to capture the output as a string, and then compare it to an expected string, which can then be included in documentation. This helps me keep the text up to date with compiler and library changes.

However, using #check with (say) List.length yields output like: List.length : List ?m.10389 → Nat. The specific number chosen for the meta is not easily predictable, and inserting new definitions earlier in the file changes the number.

Is there a way to temporarily locally override the gensym counter? That seems likely to introduce subtle elaborator bugs, so I suspect not :-)

I suppose I could also make a new macro that takes a "message spec" regexp and then requires that the example string and the compiler output match the regexp. Do we have a regexp library for Lean 4 yet?

[David Thrane Christiansen]

Perhaps it might also make sense to modify the Lean output code so that numbered metas are renamed to Greek letters that do not occur in the term being rendered? Perhaps decorated with some suitable "I'm a meta!" annotation?

[Mario Carneiro]

In lean 3 it would use ?m_1 instead, renumbering all metavariables in that particular printout based on the order they appear. This seems better on balance, although you can't easily correlate metavariables between printouts if they are in different "renumbering scopes"

[Mario Carneiro]

I think this just hasn't been implemented yet in lean 4

[Mario Carneiro]

I think in lean 4 tests, the number is predictable because the file is compiled in one shot (and I guess the numbering scheme is single-threaded?). Not sure if that is applicable for your use case

[David Thrane Christiansen]

My use case is documentation, and the numbering is predictable even interactively as Lean runs in the file, but inserting new examples prior to the message test changes the numbering. So it's not a blocker, but it does seem a bit inelegant.

This works for now, but it does make the tests a bit more fragile.

Thanks!

[Sebastian Ullrich]

At a minimum, I wonder if we can/should make the mvar id generator local to each command. I would hope at least that there is no chance of confusion between mvars from different commands for either Lean itself or for users. /cc @Leonardo de Moura