feat: use omission dots for hidden let values in Infoview (#8041)

This PR changes the behavior of `pp.showLetValues` to use a hoverable
`⋯` to hide let values. This is now false by default, and there is a new
option `pp.showLetValues.threshold` for allowing small expressions to be
shown anyway. For tactic metavariables, there is an additional option
`pp.showLetValues.tactic.threshold`, which by default is set to the
maximal value, since in tactic states local values are usually
significant.

src/Lean/Meta/IndPredBelow.lean

@@ -568,7 +568,7 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
       let (_, belowTy) ← belowType motive xs idx
       let below ← mkFreshExprSyntheticOpaqueMVar belowTy
       try
-        trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
+        trace[Meta.IndPredBelow.match] "{below.mvarId!}"
         if (← below.mvarId!.applyRules { backtracking := false, maxDepth := 1 } []).isEmpty then
           trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
           if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx)

src/Lean/Meta/PPGoal.lean

@@ -27,11 +27,44 @@ register_builtin_option pp.inaccessibleNames : Bool := {
 }
 
 register_builtin_option pp.showLetValues : Bool := {
-  defValue := true
+  defValue := false
   group    := "pp"
-  descr    := "display let-declaration values in the info view"
+  descr    := "always display let-declaration values in the info view"
 }
 
+register_builtin_option pp.showLetValues.threshold : Nat := {
+  defValue := 0
+  group    := "pp"
+  descr    := "when `pp.showLetValues` is false, the maximum size of a term allowed before it is replaced by `⋯`"
+}
+
+register_builtin_option pp.showLetValues.tactic.threshold : Nat := {
+  defValue := 255
+  group    := "pp"
+  descr    := "when `pp.showLetValues` is false, the maximum size of a term allowed before it is replaced by `⋯`, for tactic goals"
+}
+
+/--
+Given the current values of the options `pp.showLetValues` and `pp.showLetValues.threshold`,
+determines whether the local let declaration's value should be omitted.
+
+- `tactic` is whether the goal is for a tactic metavariable.
+  In that case, uses the maximum of `pp.showLetValues.tactic.threshold` and `pp.showLetValues.threshold` for the threshold.
+  In tactics, we usually want to see let values.
+  In contrast, for the "expected type" view we usually do not.
+-/
+def ppGoal.shouldShowLetValue (tactic : Bool) (e : Expr) : MetaM Bool := do
+  -- Atomic expressions never get omitted by the following logic, so we can do an early return here.
+  if e.isAtomic then
+    return true
+  let options ← getOptions
+  if pp.showLetValues.get options then
+    return true
+  let threshold := pp.showLetValues.threshold.get options
+  let threshold := max threshold (if tactic then pp.showLetValues.tactic.threshold.get options else 0)
+  let threshold := min 254 threshold
+  return e.approxDepth.toNat ≤ threshold
+
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ "\n"
 
@@ -47,9 +80,11 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
   | none          => return "unknown goal"
   | some mvarDecl =>
     let indent         := 2 -- Use option
-    let showLetValues  := pp.showLetValues.get (← getOptions)
     let ppAuxDecls     := pp.auxDecls.get (← getOptions)
     let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
+    -- Heuristic: synthetic opaque metavariables are only used by tactics,
+    -- and tactics should always be creating synthetic opaque metavariables for new goals.
+    let tactic         := mvarDecl.kind.isSyntheticOpaque
     let lctx           := mvarDecl.lctx
     let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
     withLCtx lctx mvarDecl.localInstances do
@@ -82,10 +117,12 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
           let type ← instantiateMVars type
           let typeFmt ← ppExpr type
           let mut fmtElem  := format varName ++ " : " ++ typeFmt
-          if showLetValues then
-            let val ← instantiateMVars val
+          let val ← instantiateMVars val
+          if ← ppGoal.shouldShowLetValue tactic val then
             let valFmt ← ppExpr val
             fmtElem := fmtElem ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)
+          else
+            fmtElem := fmtElem ++ " := ⋯"
           let fmt := fmt ++ fmtElem.group
           return ([], none, fmt)
       let (varNames, type?, fmt) ← lctx.foldlM (init := ([], none, Format.nil)) fun (varNames, prevType?, fmt) (localDecl : LocalDecl) =>

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -323,11 +323,13 @@ inductive OmissionReason
   | deep
   | proof
   | maxSteps
+  | string (s : String)
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
   | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
+  | string s => s
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   addDelabTermInfo pos stx e (docString? := reason.toString) (explicit := false)

src/Lean/Widget/InteractiveGoal.lean

@@ -116,7 +116,7 @@ instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 open Meta in
 /-- Extend an array of hypothesis bundles with another bundle. -/
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
-    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) (tactic := false ) :
     MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
     throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
@@ -126,10 +126,22 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
     names
     fvarIds
     type        := (← ppExprTagged type)
-    val?        := (← value?.mapM ppExprTagged)
+    val?        := (← value?.mapM ppLetValueExprTagged)
     isInstance? := if (← isClass? type).isSome then true else none
     isType?     := if (← instantiateMVars type).isSort then true else none
   }
+where
+  ppLetValueExprTagged (value : Expr) : MetaM CodeWithInfos := do
+    if ← ppGoal.shouldShowLetValue tactic value then
+      ppExprTagged value
+    else
+      ppExprTagged value do PrettyPrinter.Delaborator.omission <| .string <|
+        if tactic then
+          "Value omitted since `pp.showLetValues` is false and \
+          the expression's depth exceeds both `pp.showLetValues.tactic.threshold` and `pp.showLetValues.threshold`."
+        else
+          "Value omitted since `pp.showLetValues` is false and \
+          the expression's depth exceeds `pp.showLetValues.threshold`."
 
 open Meta in
 variable [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] in
@@ -145,8 +157,9 @@ open Meta in
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
-  let showLetValues := pp.showLetValues.get (← getOptions)
   withGoalCtx mvarId fun lctx mvarDecl => do
+    -- See comment in `Lean.Meta.ppGoal` about this synthetic opaque heuristic.
+    let tactic := mvarDecl.kind.isSyntheticOpaque
     let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
       if ids.isEmpty then
@@ -179,8 +192,8 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
           let varName := toString varName
           hyps ← pushPending varNames prevType? hyps
           let type ← instantiateMVars type
-          let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
-          hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val?
+          let val ← instantiateMVars val
+          hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val tactic
           varNames := #[]
           prevType? := none
     hyps ← pushPending varNames prevType? hyps

tests/lean/holes.lean.expected.out

@@ -8,7 +8,7 @@ y : Nat := g x + g x
 holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
 context:
 x : Nat
-y : Nat := g x + g x
+y : Nat := ⋯
 ⊢ Nat
 holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument 'β'
   @g Nat (?m x) x
@@ -26,7 +26,7 @@ holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument 'β'
   @f Nat (?m a) a
 context:
 a : Nat
-f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
+f : {α : Type} → {β : ?m a} → α → α := ⋯
 ⊢ ?m a
 holes.lean:18:9-18:10: error: failed to infer binder type
 holes.lean:21:25-22:4: error: failed to infer type of `f7`

tests/lean/interactive/expectedTypeAsGoal.lean.expected.out

@@ -2,4 +2,4 @@
  "position": {"line": 3, "character": 5}}
 {"range":
  {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 23}},
- "goal": "x : Nat := 10\n⊢ IO Unit"}
+ "goal": "x : Nat := ⋯\n⊢ IO Unit"}

tests/lean/interactive/ppShowLetValues.lean

@@ -0,0 +1,81 @@
+/-!
+# Tests of `pp.showLetValues`
+-/
+
+-- Ensure default values
+set_option pp.showLetValues false
+set_option pp.showLetValues.threshold 0
+set_option pp.showLetValues.tactic.threshold 255
+
+/-!
+Non-tactic context. No let value (see ⋯)
+-/
+example (x : Nat) : Nat :=
+  let y := x + x
+  y
+--^ $/lean/plainTermGoal
+
+/-!
+Non-tactic context. Enable showing values (see x + x)
+-/
+set_option pp.showLetValues true in
+example (x : Nat) : Nat :=
+  let y := x + x
+  y
+--^ $/lean/plainTermGoal
+
+/-!
+Non-tactic context. Turn up threshold (see x + x)
+-/
+set_option pp.showLetValues.threshold 10 in
+example (x : Nat) : Nat :=
+  let y := x + x
+  y
+--^ $/lean/plainTermGoal
+
+/-!
+Tactic context. See x + x
+-/
+example (x : Nat) : Nat := by
+  let y := x + x
+  exact y
+--^ $/lean/plainGoal
+
+/-!
+Tactic context. Turn down threshold (see ⋯)
+-/
+set_option pp.showLetValues.tactic.threshold 0 in
+example (x : Nat) : Nat := by
+  let y := x + x
+  exact y
+--^ $/lean/plainGoal
+
+/-!
+Tactic context. Uses max of both thresholds (see x + x)
+-/
+set_option pp.showLetValues.threshold 10 in
+set_option pp.showLetValues.tactic.threshold 0 in
+example (x : Nat) : Nat := by
+  let y := x + x
+  exact y
+--^ $/lean/plainGoal
+
+/-!
+Non-tactic context. Atomic always shown (see x)
+-/
+set_option pp.showLetValues.threshold 0 in
+set_option pp.showLetValues.tactic.threshold 0 in
+example (x : Nat) : Nat :=
+  let y := x
+  y
+--^ $/lean/plainTermGoal
+
+/-!
+Tactic context. Atomic always shown (see x)
+-/
+set_option pp.showLetValues.threshold 0 in
+set_option pp.showLetValues.tactic.threshold 0 in
+example (x : Nat) : Nat := by
+  let y := x
+  exact y
+--^ $/lean/plainGoal

tests/lean/interactive/ppShowLetValues.lean.expected.out

@@ -0,0 +1,36 @@
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 14, "character": 2}}
+{"range":
+ {"start": {"line": 14, "character": 2}, "end": {"line": 14, "character": 3}},
+ "goal": "x : Nat\ny : Nat := ⋯\n⊢ Nat"}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 23, "character": 2}}
+{"range":
+ {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 3}},
+ "goal": "x : Nat\ny : Nat := x + x\n⊢ Nat"}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 32, "character": 2}}
+{"range":
+ {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 3}},
+ "goal": "x : Nat\ny : Nat := x + x\n⊢ Nat"}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 40, "character": 2}}
+{"rendered": "```lean\nx : Nat\ny : Nat := x + x\n⊢ Nat\n```",
+ "goals": ["x : Nat\ny : Nat := x + x\n⊢ Nat"]}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 49, "character": 2}}
+{"rendered": "```lean\nx : Nat\ny : Nat := ⋯\n⊢ Nat\n```",
+ "goals": ["x : Nat\ny : Nat := ⋯\n⊢ Nat"]}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 59, "character": 2}}
+{"rendered": "```lean\nx : Nat\ny : Nat := x + x\n⊢ Nat\n```",
+ "goals": ["x : Nat\ny : Nat := x + x\n⊢ Nat"]}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 69, "character": 2}}
+{"range":
+ {"start": {"line": 69, "character": 2}, "end": {"line": 69, "character": 3}},
+ "goal": "x : Nat\ny : Nat := x\n⊢ Nat"}
+{"textDocument": {"uri": "file:///ppShowLetValues.lean"},
+ "position": {"line": 79, "character": 2}}
+{"rendered": "```lean\nx : Nat\ny : Nat := x\n⊢ Nat\n```",
+ "goals": ["x : Nat\ny : Nat := x\n⊢ Nat"]}

tests/lean/mvarAtDefaultValue.lean.expected.out

@@ -2,5 +2,5 @@ mvarAtDefaultValue.lean:5:7-5:8: error: failed to infer default value for field
 mvarAtDefaultValue.lean:8:7-8:8: error: don't know how to synthesize placeholder
 context:
 x : Nat
-toA : A := { x := x }
+toA : A := ⋯
 ⊢ Nat