feat: hide auxiliary declarations

src/Lean/Util/PPGoal.lean

@@ -7,12 +7,18 @@ import Lean.Util.PPExt
 
 namespace Lean
 
+def showAuxDeclsDefault := false
+@[init] def showAuxDeclsOption : IO Unit :=
+registerOption `pp.showAuxDecls { defValue := showAuxDeclsDefault, group := "pp", descr := "show auxiliary declarations used to compile recursive functions" }
+def getShowAuxDecls (o : Options) : Bool:= o.get `pp.showAuxDecls showAuxDeclsDefault
+
 def ppGoal (env : Environment) (mctx : MetavarContext) (opts : Options) (mvarId : MVarId) : Format :=
 match mctx.findDecl? mvarId with
 | none          => "unknown goal"
 | some mvarDecl =>
-  let indent := 2; -- Use option
-  let lctx   := mvarDecl.lctx;
+  let indent       := 2; -- Use option
+  let showAuxDecls := getShowAuxDecls opts;
+  let lctx         := mvarDecl.lctx;
   let pp (e : Expr) : Format := ppExpr env mctx lctx opts e;
   let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1;
   let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line;
@@ -27,6 +33,7 @@ match mctx.findDecl? mvarId with
       | _, some type => fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ pp type)).group;
   let (varNames, type?, fmt) := mvarDecl.lctx.foldl
     (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) =>
+       if !showAuxDecls && localDecl.isAuxDecl then acc else
        let (varNames, prevType?, fmt) := acc;
        match localDecl with
        | LocalDecl.cdecl _ _ varName type _   =>

tests/lean/auxDeclIssue.lean

@@ -11,3 +11,9 @@ by {
   subst x; -- should not use the auxiliary declaration `ex2 : x = y`
   exact rfl
 }
+
+set_option pp.showAuxDecls true in
+theorem ex1 : False :=
+by {
+   assumption -- should not use the auxiliary declaration `ex1 : False`
+}

tests/lean/auxDeclIssue.lean.expected.out

@@ -1,7 +1,9 @@
 auxDeclIssue.lean:5:3: error: tactic 'assumption' failed, 
-ex1 : False
 ⊢ False
 auxDeclIssue.lean:11:2: error: tactic 'subst' failed, did not find equation for eliminating 'x'
 x y : Nat
-ex2 : x=y
 ⊢ x=y
+auxDeclIssue.lean:18:3: error: tactic 'assumption' failed, 
+x y : Nat
+ex1 : False
+⊢ False

tests/lean/collectDepsIssue.lean.expected.out

@@ -1,6 +1,5 @@
 collectDepsIssue.lean:5:0: error: don't know how to synthesize placeholder
 context:
 α : Type
-f : α → List α
 a : α
 ⊢ List α

tests/lean/holes.lean.expected.out

@@ -2,26 +2,22 @@ holes.lean:4:4: error: placeholders '_' cannot be used where a function is expec
 holes.lean:11:8: error: don't know how to synthesize placeholder
 context:
 case hole
-f3 : Nat → Nat
 x : Nat
 y : Nat := g x+g x
 ⊢ Nat
 holes.lean:11:4: error: don't know how to synthesize placeholder
 context:
-f3 : Nat → Nat
 x : Nat
 y : Nat := g x+g x
 ⊢ Nat
 holes.lean:10:15: error: don't know how to synthesize placeholder
   @g … ?m …
 context:
-f3 : Nat → Nat
 x : Nat
 ⊢ Type
 holes.lean:10:9: error: don't know how to synthesize placeholder
   @g … ?m …
 context:
-f3 : Nat → Nat
 x : Nat
 ⊢ Type
 holes.lean:13:7: error: don't know how to synthesize placeholder
@@ -35,13 +31,11 @@ context:
 holes.lean:19:0: error: don't know how to synthesize placeholder
   @_uniq.125 … ?m …
 context:
-f6 : Nat → Nat
 a : Nat
 f : ∀ {α : Type} {β : ?m a}, α → α := fun {α : Type} {β : ?m a} (a : α) => a
 ⊢ ?m a
 holes.lean:18:6: error: don't know how to synthesize placeholder
 context:
-f6 : Nat → Nat
 a : Nat
 α : Type
 ⊢ Sort ?
@@ -51,6 +45,5 @@ x : Nat
 ⊢ Sort ?
 holes.lean:25:8: error: don't know how to synthesize placeholder
 context:
-f8 : Nat → Nat
 x y : Nat
 ⊢ Sort ?