current mvar

Stream: lean4

[Kenny Lau]

This is just for fun basically, so,

import Lean
-- import Mathlib

open Lean Meta

def currentMVar : MetaM Nat := do
  let ⟨.num `_uniq n⟩ ← mkFreshMVarId | throwError "aaa"
  return n

#eval currentMVar
/-
977 with import Mathlib
887 with import Lean
-/

I wrote a code to get the "current number of metavariables", and found that it's 887 with just import Lean, an 977 with import Mathlib

[Kenny Lau]

does this mean there are 90 unassigned metavariables in Mathlib?

[Aaron Liu]

no???

[Aaron Liu]

it means some instance synthesis is happening probably

[Kenny Lau]

what determines the number i get?

[Aaron Liu]

the metavariable counter resets for every file

[Aaron Liu]

the number you get is just sequential based on how many numbers

[Aaron Liu]

based on how many times the name generator was incremented

[Aaron Liu]

how many times it was incremented since the file was initialized

[Robin Arnez]

That number gets incremented all the time but never decremented. Most notably it gets used for mkFreshMVarId and mkFreshFVarId which get indirectly called tons of times in pretty much every meta program. You can see this by just querying the name generator twice:

import Lean

open Lean Meta

/-- info: { namePrefix := `_uniq, idx := 1147 } -/
#guard_msgs in
#eval (getNGen : MetaM Lean.NameGenerator)

/-- info: { namePrefix := `_uniq, idx := 2293 } -/
#guard_msgs in
#eval (getNGen : MetaM Lean.NameGenerator)

As you can see, the single #eval command is already responsible for 1146 increments (it's 1 in its initial state)