feat: have pp.proofs use ⋯ for omission (#3241)

By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.

Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.

This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.

RELEASES.md

@@ -11,6 +11,11 @@ of each version.
 v4.7.0 (development in progress)
 ---------
 
+* When the `pp.proofs` is false, now omitted proofs use `⋯` rather than `_`,
+  which gives a more helpful error message when copied from the Infoview.
+  The `pp.proofs.threshold` option lets small proofs always be pretty printed.
+  [#3241](https://github.com/leanprover/lean4/pull/3241).
+
 v4.6.0
 ---------
 

src/Init/NotationExtra.lean

@@ -173,16 +173,15 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
 /--
 Denotes a term that was omitted by the pretty printer.
 This is only used for pretty printing, and it cannot be elaborated.
-The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.deepTerms.threshold`
-options.
+The presence of `⋯` is controlled by the `pp.deepTerms` and `pp.proofs` options.
 -/
 syntax "⋯" : term
 
 macro_rules | `(⋯) => Macro.throwError "\
   Error: The '⋯' token is used by the pretty printer to indicate omitted terms, \
-  and it cannot be elaborated. \
-  Its presence in pretty printing output is controlled by the 'pp.deepTerms' and \
-  `pp.deepTerms.threshold` options."
+  and it cannot be elaborated.\
+  \n\nIts presence in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. \
+  These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`."
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -247,6 +247,19 @@ See also `Lean.PrettyPrinter.Delaborator.Context.depth`.
 def withIncDepth (act : DelabM α) : DelabM α := fun ctx =>
   act { ctx with depth := ctx.depth + 1 }
 
+/--
+Returns true if `e` is a "shallow" expression.
+Local variables, constants, and other atomic expressions are always shallow.
+In general, an expression is considered to be shallow if its depth is at most `threshold`.
+
+Since the implementation uses `Lean.Expr.approxDepth`, the `threshold` is clamped to `[0, 254]`.
+-/
+def isShallowExpression (threshold : Nat) (e : Expr) : Bool :=
+  -- Approximate depth is saturated at 255 for very deep expressions.
+  -- Need to clamp to `[0, 254]` so that not every expression is shallow.
+  let threshold := min 254 threshold
+  e.approxDepth.toNat ≤ threshold
+
 /--
 Returns `true` if, at the current depth, we should omit the term and use `⋯` rather than
 delaborating it. This function can only return `true` if `pp.deepTerms` is set to `false`.
@@ -255,19 +268,42 @@ an expression, which prevents terms such as atomic expressions or `OfNat.ofNat`
 delaborated as `⋯`.
 -/
 def shouldOmitExpr (e : Expr) : DelabM Bool := do
-  if ← getPPOption getPPDeepTerms then
+  -- Atomic expressions never get omitted, so we can do an early return here.
+  if e.isAtomic then
+    return false
+
+  if (← getPPOption getPPDeepTerms) then
     return false
 
   let depth := (← read).depth
   let depthThreshold ← getPPOption getPPDeepTermsThreshold
-  let approxDepth := e.approxDepth.toNat
   let depthExcess := depth - depthThreshold
+  -- This threshold for shallow expressions effectively allows full terms to be pretty printed 25% deeper,
+  -- so long as the subterm actually can be fully pretty printed within this extra 25% depth.
+  let threshold := depthThreshold/4 - depthExcess
 
-  let isMaxedOutApproxDepth := approxDepth >= 255
-  let isShallowExpression :=
-    !isMaxedOutApproxDepth && approxDepth <= depthThreshold/4 - depthExcess
+  return depthExcess > 0 && !isShallowExpression threshold e
 
-  return depthExcess > 0 && !isShallowExpression
+/--
+Returns `true` if the given expression is a proof and should be omitted.
+This function only returns `true` if `pp.proofs` is set to `false`.
+
+"Shallow" proofs are not omitted.
+The `pp.proofs.threshold` option controls the depth threshold for what constitutes a shallow proof.
+See `Lean.PrettyPrinter.Delaborator.isShallowExpression`.
+-/
+def shouldOmitProof (e : Expr) : DelabM Bool := do
+  -- Atomic expressions never get omitted, so we can do an early return here.
+  if e.isAtomic then
+    return false
+
+  if (← getPPOption getPPProofs) then
+    return false
+
+  unless (← try Meta.isProof e catch _ => pure false) do
+    return false
+
+  return !isShallowExpression (← getPPOption getPPProofsThreshold) e
 
 /--
 Annotates the term with the current expression position and registers `TermInfo`
@@ -310,13 +346,14 @@ partial def delab : Delab := do
   if ← shouldOmitExpr e then
     return ← omission
 
-  -- no need to hide atomic proofs
-  if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch _ => pure false) then
+  if ← shouldOmitProof e then
+    let pf ← omission
     if ← getPPOption getPPProofsWithType then
       let stx ← withType delab
-      return ← annotateTermInfo (← `((_ : $stx)))
+      return ← annotateCurPos (← `(($pf : $stx)))
     else
-      return ← annotateTermInfo (← ``(_))
+      return pf
+
   let k ← getExprKind
   let stx ← withIncDepth <| delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
   if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -118,12 +118,17 @@ register_builtin_option pp.tagAppFns : Bool := {
 register_builtin_option pp.proofs : Bool := {
   defValue := false
   group    := "pp"
-  descr    := "(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"
+  descr    := "(pretty printer) display proofs when true, and replace proofs appearing within expressions by `⋯` when false"
 }
 register_builtin_option pp.proofs.withType : Bool := {
   defValue := true
   group    := "pp"
-  descr    := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"
+  descr    := "(pretty printer) when `pp.proofs` is false, adds a type ascription to the omitted proof"
+}
+register_builtin_option pp.proofs.threshold : Nat := {
+  defValue := 0
+  group    := "pp"
+  descr    := "(pretty printer) when `pp.proofs` is false, controls the complexity of proofs at which they begin being replaced with `⋯`"
 }
 register_builtin_option pp.instances : Bool := {
   defValue := true
@@ -220,14 +225,15 @@ def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPA
 def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.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 (getPPAll o)
+def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (pp.proofs.defValue || getPPAll o)
 def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue
+def getPPProofsThreshold (o : Options) : Nat := o.get pp.proofs.threshold.name pp.proofs.threshold.defValue
 def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue
 def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue
 def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue
 def getPPInstances (o : Options) : Bool := o.get pp.instances.name pp.instances.defValue
 def getPPInstanceTypes (o : Options) : Bool := o.get pp.instanceTypes.name pp.instanceTypes.defValue
-def getPPDeepTerms (o : Options) : Bool := o.get pp.deepTerms.name pp.deepTerms.defValue
+def getPPDeepTerms (o : Options) : Bool := o.get pp.deepTerms.name (pp.deepTerms.defValue || getPPAll o)
 def getPPDeepTermsThreshold (o : Options) : Nat := o.get pp.deepTerms.threshold.name pp.deepTerms.threshold.defValue
 
 end Lean

src/Lean/Widget/InteractiveCode.lean

@@ -82,7 +82,8 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
       withOptionAtCurrPos pp.explicit.name true do
         delabApp
     else
-      delab
+      withOptionAtCurrPos pp.proofs.name true do
+        delab
   let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos e (delab := delab)
   let tt := TaggedText.prettyTagged fmt
   let ctx := {

tests/lean/1074a.lean.expected.out

@@ -1,4 +1,4 @@
 Brx.interp._eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
   Brx.interp H_2 =
-    match (_ : True ∧ Brx z) with
-    | (_ : True ∧ Brx z) => Brx.interp Hz
+    match (⋯ : True ∧ Brx z) with
+    | (⋯ : True ∧ Brx z) => Brx.interp Hz

tests/lean/1081.lean.expected.out

@@ -7,6 +7,6 @@ but is expected to have type
 1081.lean:23:4-23:7: error: type mismatch
   rfl
 has type
-  insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v = insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v : Prop
+  insert a { val := 0, isLt := (⋯ : 0 < Nat.succ n) } v = insert a { val := 0, isLt := (⋯ : 0 < Nat.succ n) } v : Prop
 but is expected to have type
-  insert a { val := 0, isLt := (_ : 0 < Nat.succ n) } v = cons a v : Prop
+  insert a { val := 0, isLt := (⋯ : 0 < Nat.succ n) } v = cons a v : Prop

tests/lean/1856.lean.expected.out

@@ -6,4 +6,4 @@ i : α
 β : α → Type ?u
 f : (j : α) → β j
 x : α
-⊢ (if h : x = i then (_ : i = x) ▸ f i else f x) = f x
+⊢ (if h : x = i then (⋯ : i = x) ▸ f i else f x) = f x

tests/lean/986.lean.expected.out

@@ -3,8 +3,8 @@ Array.insertionSort.swapLoop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Boo
 Array.insertionSort.swapLoop._eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
   (h : Nat.succ j' < Array.size a) :
   Array.insertionSort.swapLoop lt a (Nat.succ j') h =
-    let_fun h' := (_ : j' < Array.size a);
+    let_fun h' := (⋯ : j' < Array.size a);
     if lt a[Nat.succ j'] a[j'] = true then
       Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j'
-        (_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
+        (⋯ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
     else a

tests/lean/congrThm.lean.expected.out

@@ -1,8 +1,8 @@
 ∀ (p p_1 : Prop),
   p = p_1 →
     ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat) (e_a : a = a_1) (h : a > 0),
-      g p a h = g p_1 a_1 (_ : a_1 > 0)
+      g p a h = g p_1 a_1 (⋯ : a_1 > 0)
 ∀ (p p_1 : Prop),
   p = p_1 →
     ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat) (e_a : a = a_1) (h : a > 0),
-      g p a h = g p_1 a_1 (_ : a_1 > 0)
+      g p a h = g p_1 a_1 (⋯ : a_1 > 0)

tests/lean/congrThmIssue.lean.expected.out

@@ -4,10 +4,10 @@ cap : Nat
 backing : Fin cap → Option α
 size : Nat
 h_size : size ≤ cap
-h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing { val := i, isLt := (_ : i < cap) }) = true
+h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing { val := i, isLt := (⋯ : i < cap) }) = true
 i : Nat
 h : i < size
 ⊢ Option.isSome
-      (if h_1 : i < cap then backing { val := i, isLt := (_ : { val := i, isLt := (_ : i < cap + cap) }.val < cap) }
+      (if h_1 : i < cap then backing { val := i, isLt := (⋯ : { val := i, isLt := (⋯ : i < cap + cap) }.val < cap) }
       else none) =
     true

tests/lean/diamond9.lean.expected.out

@@ -1,2 +1,2 @@
 constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R
-Ring.mk (fun x n => Int.toNat x * n) (_ : ∀ (a : Nat), 0 * a = 0) : Ring Nat
+Ring.mk (fun x n => Int.toNat x * n) (⋯ : ∀ (a : Nat), 0 * a = 0) : Ring Nat

tests/lean/heapSort.lean.expected.out

@@ -13,5 +13,5 @@ Array.heapSort.loop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : B
     match e : BinaryHeap.max a with
     | none => out
     | some x =>
-      let_fun this := (_ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a);
+      let_fun this := (⋯ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a);
       Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)

tests/lean/letFun.lean.expected.out

@@ -15,7 +15,7 @@ a b : Nat
 h : a > b
 ⊢ a > b
 let_fun n := 5;
-{ val := [], property := (_ : 0 ≤ n) } : { as // List.length as ≤ 5 }
+{ val := [], property := (⋯ : 0 ≤ n) } : { as // List.length as ≤ 5 }
 rfl : (let_fun n := 5;
   n) =
   let_fun n := 5;

tests/lean/match1.lean.expected.out

@@ -11,9 +11,9 @@
 ---- inv
 10
 match1.lean:82:0-82:73: error: dependent elimination failed, type mismatch when solving alternative with type
-  motive 0 (Vec.cons head✝ Vec.nil) (_ : VecPred P (Vec.cons head✝ Vec.nil))
+  motive 0 (Vec.cons head✝ Vec.nil) (⋯ : VecPred P (Vec.cons head✝ Vec.nil))
 but expected
-  motive x✝ (Vec.cons head✝ tail✝) (_ : VecPred P (Vec.cons head✝ tail✝))
+  motive x✝ (Vec.cons head✝ tail✝) (⋯ : VecPred P (Vec.cons head✝ tail✝))
 [false, true, true]
 match1.lean:119:0-119:41: error: dependent match elimination failed, inaccessible pattern found
   .(j + j)

tests/lean/ppProofs.lean

@@ -1,3 +1,8 @@
+/-!
+# Tests for the `pp.proofs` option
+-/
+
+section
 set_option pp.analyze.trustSubst true
 set_option pp.proofs false
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
@@ -7,3 +12,13 @@ set_option pp.proofs.withType false
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 set_option pp.proofs true
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
+end
+
+/-!
+Testing threshold option
+-/
+section
+#check let _ := Nat.le_succ 1; 0
+set_option pp.proofs.threshold 10
+#check let _ := Nat.le_succ 1; 0
+end

tests/lean/ppProofs.lean.expected.out

@@ -1,34 +1,38 @@
-ppProofs.lean:3:47-3:48: error: don't know how to synthesize placeholder
+ppProofs.lean:8:47-8:48: error: don't know how to synthesize placeholder
 context:
 α β : Sort u_1
 b : β
 a : α
 h : α = β
 ⊢ h ▸ a = b
-ppProofs.lean:4:50-4:51: error: don't know how to synthesize placeholder
-context:
-α β : Sort u_1
-b : β
-a : α
-h : α = β
-⊢ (_ : α = β) ▸ a = b
-ppProofs.lean:5:50-5:98: error: unsolved goals
-α β : Sort ?u
-b : β
-a : α
-h : α = β
-⊢ (_ : α = β) ▸ a = b
-ppProofs.lean:7:50-7:51: error: don't know how to synthesize placeholder
-context:
-α β : Sort u_1
-b : β
-a : α
-h : α = β
-⊢ _ ▸ a = b
 ppProofs.lean:9:50-9:51: error: don't know how to synthesize placeholder
 context:
 α β : Sort u_1
 b : β
 a : α
 h : α = β
+⊢ (⋯ : α = β) ▸ a = b
+ppProofs.lean:10:50-10:98: error: unsolved goals
+α β : Sort ?u
+b : β
+a : α
+h : α = β
+⊢ (⋯ : α = β) ▸ a = b
+ppProofs.lean:12:50-12:51: error: don't know how to synthesize placeholder
+context:
+α β : Sort u_1
+b : β
+a : α
+h : α = β
+⊢ ⋯ ▸ a = b
+ppProofs.lean:14:50-14:51: error: don't know how to synthesize placeholder
+context:
+α β : Sort u_1
+b : β
+a : α
+h : α = β
 ⊢ id h ▸ a = b
+let x := (⋯ : 1 ≤ Nat.succ 1);
+0 : Nat
+let x := Nat.le_succ 1;
+0 : Nat

tests/lean/run/PPTopDownAnalyze.lean

@@ -257,14 +257,22 @@ structure S2 where x : Unit
 inductive NeedsAnalysis {α : Type} : Prop
   | mk : NeedsAnalysis
 
+section proofs
+/--
+The `#testDelab` expects it can elaborate the expression, so here is a macro rule to let that happen.
+-/
+local macro_rules | `(⋯) => `(_)
+
 set_option pp.proofs false in
 #testDelab @NeedsAnalysis.mk Unit
-  expecting (_ : NeedsAnalysis (α := Unit))
+  expecting (⋯ : NeedsAnalysis (α := Unit))
 
 set_option pp.proofs false in
 set_option pp.proofs.withType false in
 #testDelab @NeedsAnalysis.mk Unit
-  expecting _
+  expecting ⋯
+
+end proofs
 
 #testDelab ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 : Array α }
   expecting ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 }

tests/lean/wfrecUnusedLet.lean.expected.out

@@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
-    2 * a (n - 1) (_ : (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n - 1) n)
+    2 * a (n - 1) (⋯ : (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n - 1) n)