Pantograph/Protocol.lean

@@ -18,6 +18,7 @@ structure Options where
   printExprPretty: Bool    := true
   -- When enabled, print the raw AST of expressions
   printExprAST: Bool       := false
+  printDependentMVars: Bool := false
   -- When enabled, the types and values of persistent variables in a goal
   -- are not shown unless they are new to the proof step. Reduces overhead.
   -- NOTE: that this assumes the type and assignment of variables can never change.
@@ -41,6 +42,7 @@ structure Expression where
   pp?: Option String             := .none
   -- AST structure
   sexp?: Option String           := .none
+  dependentMVars?: Option (Array String) := .none
   deriving Lean.ToJson
 
 structure Variable where
@@ -182,6 +184,7 @@ structure OptionsSet where
   printJsonPretty?: Option Bool
   printExprPretty?: Option Bool
   printExprAST?: Option Bool
+  printDependentMVars?: Option Bool
   noRepeat?: Option Bool
   printAuxDecls?: Option Bool
   printImplementationDetailHyps?: Option Bool

Pantograph/Serial.lean

@@ -15,7 +15,7 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL
 namespace Pantograph
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
 --- Input Functions ---
@@ -171,9 +171,13 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
   let sexp?: Option String ← match options.printExprAST with
     | true => pure $ .some $ ← serializeExpressionSexp e
     | false => pure $ .none
+  let dependentMVars? ← match options.printDependentMVars with
+    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
+    | false => pure $ .none
   return {
     pp?,
     sexp?
+    dependentMVars?,
   }
 
 /-- Adapted from ppGoal -/

Test/Metavar.lean

@@ -121,8 +121,12 @@ def test_m_couple_simp: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
+  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
+    #[#["_uniq.38"], #["_uniq.38"], #[]])
+
   let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
     | .success state => pure state
     | other => do