From 5dd8d570fd12419c6dd7df114c0a9c4b92777973 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Sun, 1 Mar 2026 17:43:14 +1100 Subject: [PATCH] feat: add pp.fvars.anonymous option (#12688) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a `pp.fvars.anonymous` option (default `true`) that controls the display of loose free variables (fvars not in the local context). - When `true` (default), loose fvars display their internal name like `_fvar.42` - When `false`, they display as `_fvar._` This is analogous to `pp.mvars.anonymous` for metavariables. It's useful for stabilizing output in `#guard_msgs` when messages contain fvar IDs that vary between runs — for example, in diagnostic tools that report `isDefEq` failures from trace output where the local context is not available. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 --- src/Init/Notation.lean | 2 ++ .../PrettyPrinter/Delaborator/Builtins.lean | 8 ++++-- .../PrettyPrinter/Delaborator/Options.lean | 6 +++++ tests/lean/run/ppFVarsAnonymous.lean | 27 +++++++++++++++++++ 4 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/ppFVarsAnonymous.lean diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 0996748f2f..6d588d3d0b 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -910,6 +910,8 @@ When messages contain autogenerated names (e.g., metavariables like `?m.47`), th differ between runs or Lean versions. Use `set_option pp.mvars.anonymous false` to replace anonymous metavariables with `?_` while preserving user-named metavariables like `?a`. Alternatively, `set_option pp.mvars false` replaces all metavariables with `?_`. +Similarly, `set_option pp.fvars.anonymous false` replaces loose free variable names like +`_fvar.22` with `_`. For example, `#guard_msgs (error, drop all) in cmd` means to check errors and drop everything else. diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index ec3bba493e..b2940f5c96 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -46,8 +46,12 @@ def delabFVar : Delab := do let l ← fvarId.getDecl maybeAddBlockImplicit (mkIdent l.userName) catch _ => - -- loose free variable, use internal name - maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar) + -- loose free variable + if ← getPPOption getPPFVarsAnonymous then + -- use internal name like `_fvar.22` + maybeAddBlockImplicit <| mkIdent (fvarId.name.replacePrefix `_uniq `_fvar) + else + maybeAddBlockImplicit <| mkIdent `_ -- loose bound variable, use pseudo syntax @[builtin_delab bvar] diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 0c54b1ed04..1ee6a9b6bb 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -130,6 +130,11 @@ register_builtin_option pp.mvars.delayed : Bool := { defValue := false descr := "(pretty printer) display delayed assigned metavariables when true, otherwise display what they are assigned to" } +register_builtin_option pp.fvars.anonymous : Bool := { + defValue := true + descr := "(pretty printer) display names for loose free variables (not in the local context) such as `_fvar.22` when true, \ + and otherwise display them as '_'. Useful for stabilizing output in `#guard_msgs`." +} register_builtin_option pp.beta : Bool := { defValue := false descr := "(pretty printer) apply beta-reduction when pretty printing" @@ -271,6 +276,7 @@ def getPPMVarsAnonymous (o : Options) : Bool := o.get pp.mvars.anonymous.name (p def getPPMVarsLevels (o : Options) : Bool := o.get pp.mvars.levels.name (pp.mvars.levels.defValue && getPPMVarsAnonymous o) def getPPMVarsWithType (o : Options) : Bool := o.get pp.mvars.withType.name pp.mvars.withType.defValue def getPPMVarsDelayed (o : Options) : Bool := o.get pp.mvars.delayed.name (pp.mvars.delayed.defValue || getPPAll o) +def getPPFVarsAnonymous (o : Options) : Bool := o.get pp.fvars.anonymous.name pp.fvars.anonymous.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) diff --git a/tests/lean/run/ppFVarsAnonymous.lean b/tests/lean/run/ppFVarsAnonymous.lean new file mode 100644 index 0000000000..9a1d4f77a1 --- /dev/null +++ b/tests/lean/run/ppFVarsAnonymous.lean @@ -0,0 +1,27 @@ +import Lean + +/-! +# Tests for `pp.fvars.anonymous` + +When a free variable is not in the local context (a "loose" fvar), +the pretty printer renders it with an internal name like `_fvar.42`. +The `pp.fvars.anonymous` option (default `true`) controls this behavior: +when set to `false`, loose fvars are displayed as `_`. +-/ + +open Lean Elab Command in +#guard_msgs in +run_cmd liftTermElabM do + let fvarId : FVarId := { name := .num `_uniq 42 } + let e := Expr.fvar fvarId + let fmt ← Meta.ppExpr e + guard <| s!"{fmt}" == "_fvar.42" + +set_option pp.fvars.anonymous false in +open Lean Elab Command in +#guard_msgs in +run_cmd liftTermElabM do + let fvarId : FVarId := { name := .num `_uniq 42 } + let e := Expr.fvar fvarId + let fmt ← Meta.ppExpr e + guard <| s!"{fmt}" == "_"