feat: add pp.mvars and pp.mvars.withType (leanprover#3798)

* Setting `pp.mvars` to false causes metavariables to pretty print as
`?_`.
* Setting `pp.mvars.withType` to true causes metavariables to pretty
print with type ascriptions.

Motivation: when making tests, it is inconvenient using `#guard_msgs`
when there are metavariables, since the unique numbering is subject to
change.

This feature does not use `⋯` omissions since a metavariable is already
in a sense an omitted term. If repeated metavariables do not appear in
an expression, there is a chance that a term pretty printed with
`pp.mvars` set to false can still elaborate to the correct term, unlike
for other omissions.

(In the future we could consider an option that pretty prints uniquely
numbered metavariables as `?m✝`, `?m✝¹`, `?m✝²`, etc. to be able to tell
them apart, at least in the same pretty printed expression. It would
take care to make sure that these names are stable across different
hovers.)

Closes leanprover#3781

RELEASES.md

@@ -69,6 +69,12 @@ v4.8.0 (development in progress)
   to enable pretty printing function applications using generalized field notation (defaults to true).
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
+* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
+  When `pp.mvars` is false, metavariables pretty print as `?_`,
+  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  [#3798](https://github.com/leanprover/lean4/pull/3798).
+
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
   Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -54,12 +54,16 @@ def delabBVar : Delab := do
 @[builtin_delab mvar]
 def delabMVar : Delab := do
   let Expr.mvar n ← getExpr | unreachable!
-  let mvarDecl ← n.getDecl
-  let n :=
-    match mvarDecl.userName with
-    | Name.anonymous => n.name.replacePrefix `_uniq `m
-    | n => n
-  `(?$(mkIdent n))
+  withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
+    if ← getPPOption getPPMVars then
+      let mvarDecl ← n.getDecl
+      let n :=
+        match mvarDecl.userName with
+        | .anonymous => n.name.replacePrefix `_uniq `m
+        | n => n
+      `(?$(mkIdent n))
+    else
+      `(?_)
 
 @[builtin_delab sort]
 def delabSort : Delab := do

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -79,6 +79,16 @@ register_builtin_option pp.instantiateMVars : Bool := {
   group    := "pp"
   descr    := "(pretty printer) instantiate mvars before delaborating"
 }
+register_builtin_option pp.mvars : Bool := {
+  defValue := true
+  group    := "pp"
+  descr    := "(pretty printer) display names of metavariables when true, and otherwise display them as '?_'"
+}
+register_builtin_option pp.mvars.withType : Bool := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) display metavariables with a type ascription"
+}
 register_builtin_option pp.beta : Bool := {
   defValue := false
   group    := "pp"
@@ -235,6 +245,8 @@ def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o)
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue
+def getPPMVars (o : Options) : Bool := o.get pp.mvars.name pp.mvars.defValue
+def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue
 def getPPBeta (o : Options) : Bool := o.get pp.beta.name pp.beta.defValue
 def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
 def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)

src/Lean/Widget/InteractiveCode.lean

@@ -81,6 +81,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
     if explicit then
       withOptionAtCurrPos pp.tagAppFns.name true do
       withOptionAtCurrPos pp.explicit.name true do
+      withOptionAtCurrPos pp.mvars.name true do
         delabApp
     else
       withOptionAtCurrPos pp.proofs.name true do

tests/lean/run/ppMVars.lean

@@ -0,0 +1,50 @@
+/-!
+# Testing `pp.mvars`
+-/
+
+/-!
+Default values
+-/
+
+/-- info: ?a : Nat -/
+#guard_msgs in #check (?a : Nat)
+
+/-!
+Turning off `pp.mvars`
+-/
+section
+set_option pp.mvars false
+
+/-- info: ?_ : Nat -/
+#guard_msgs in #check (?a : Nat)
+
+/-- info: ?_ : Nat -/
+#guard_msgs in #check (_ : Nat)
+
+end
+
+/-!
+Turning off `pp.mvars` and turning on `pp.mvars.withType`.
+-/
+section
+set_option pp.mvars false
+set_option pp.mvars.withType true
+
+/-- info: (?_ : Nat) : Nat -/
+#guard_msgs in #check (?a : Nat)
+
+/-- info: (?_ : Nat) : Nat -/
+#guard_msgs in #check (_ : Nat)
+
+end
+
+/-!
+Turning on `pp.mvars.withType`.
+-/
+section
+set_option pp.mvars.withType true
+
+/-- info: (?a : Nat) : Nat -/
+#guard_msgs in #check (?a : Nat)
+
+end