fix: make "use `set_option diagnostics true" message conditional on c…

…urrent setting (#4781)

It is confusing that the message suggesting to use the `diagnostics`
option is given even when the option is already set. This PR makes use
of lazy message data to make the message contingent on the option being
false.

It also tones down the promise that there is any diagonostic information
available, since sometimes there is nothing to report.

Suggested by Johan Commelin.

src/Lean/CoreM.lean

@@ -31,7 +31,16 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
-def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
+/--
+If the `diagnostics` option is not already set, gives a message explaining this option.
+Begins with a `\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
+-/
+def useDiagnosticMsg : MessageData :=
+  MessageData.lazy fun ctx =>
+    if diagnostics.get ctx.opts then
+      pure ""
+    else
+      pure s!"\nAdditional diagnostic information may be available by using the `set_option {diagnostics.name} true` command."
 
 namespace Core
 
@@ -300,8 +309,10 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
-  throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
+  throw <| Exception.error (← getRef) m!"\
+    (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
+    Use `set_option {optionName} <num>` to set the limit.\
+    {useDiagnosticMsg}"
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
   unless max == 0 do

src/Lean/Elab/Calc.lean

@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.

src/Lean/Elab/Term.lean

@@ -996,7 +996,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}\n{useDiagnosticMsg}"
+      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}{useDiagnosticMsg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do

src/Lean/Meta/SynthInstance.lean

@@ -636,7 +636,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
        (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
        fun ex =>
          if ex.isRuntime then
-           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}\n{useDiagnosticMsg}"
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}"
          else
            throw ex
 
@@ -810,7 +810,7 @@ def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM
     (fun _ => pure LOption.undef)
 
 def throwFailedToSynthesize (type : Expr) : MetaM Expr :=
-  throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+  throwError "failed to synthesize{indentExpr type}{useDiagnosticMsg}"
 
 def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId

tests/lean/1007.lean.expected.out

@@ -8,4 +8,4 @@
 1007.lean:39:4-39:7: warning: declaration uses 'sorry'
 1007.lean:56:64-56:78: error: failed to synthesize
   IsLin fun x => sum fun i => norm x
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/1102.lean.expected.out

@@ -1,3 +1,3 @@
 1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/2040.lean.expected.out

@@ -1,12 +1,12 @@
 2040.lean:8:8-8:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:14:8-14:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:20:8-20:13: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 2040.lean:18:2-20:22: error: type mismatch
   trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
 has type

tests/lean/2220.lean.expected.out

@@ -8,11 +8,11 @@
 @HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int
 2220.lean:25:19-25:24: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int
 2220.lean:26:12-26:17: error: failed to synthesize
   HPow Nat Nat Int
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 @HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1))
   (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int

tests/lean/2273.lean.expected.out

@@ -1,3 +1,3 @@
 2273.lean:9:8-9:14: error: failed to synthesize
   P 37
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/297.lean.expected.out

@@ -3,4 +3,4 @@
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Sort ?u
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/386.lean.expected.out

@@ -1,3 +1,3 @@
 386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/448.lean.expected.out

@@ -1,3 +1,3 @@
 448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/attrCmd.lean.expected.out

@@ -1,3 +1,3 @@
 attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/calcErrors.lean.expected.out

@@ -12,7 +12,7 @@ calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
   p a
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 calcErrors.lean:41:7-41:12: error: invalid 'calc' step, left-hand-side is
   γ : Sort u_1
 previous right-hand-side is

tests/lean/defInst.lean.expected.out

@@ -1,7 +1,7 @@
 [4, 5, 6]
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool

tests/lean/defaultInstance.lean.expected.out

@@ -1,5 +1,5 @@
 defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
   Foo Bool (?m x)

tests/lean/eagerUnfoldingIssue.lean.expected.out

@@ -1,6 +1,6 @@
 eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/eraseInsts.lean.expected.out

@@ -1,3 +1,3 @@
 eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/forErrors.lean.expected.out

@@ -1,3 +1,3 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/kernelMVarBug.lean.expected.out

@@ -1,3 +1,3 @@
 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.

tests/lean/macroStack.lean.expected.out

@@ -11,7 +11,7 @@ while expanding
 macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
 macroStack.lean:17:0-17:6: error: failed to synthesize
   HAdd Nat String ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding

tests/lean/macroSwizzle.lean.expected.out

@@ -1,6 +1,6 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
 argument

tests/lean/openScoped.lean.expected.out

@@ -1,7 +1,7 @@
 openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize
   Decidable (f = g)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
 openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'

tests/lean/prvCtor.lean.expected.out

@@ -7,7 +7,7 @@ prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize
     EmptyCollection (Name "hello")
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 
   invalid {...} notation, constructor for `Name` is marked as private
 prvCtor.lean:31:25-31:34: error: invalid ⟨...⟩ notation, constructor for `Name` is marked as private

tests/lean/run/1163.lean

@@ -16,7 +16,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def x : Bool := 0
@@ -29,7 +29,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error

tests/lean/run/3313.lean

@@ -41,7 +41,6 @@ info: [type_class] max synth pending failures (maxSynthPendingDepth: 1), use `se
 ---
 error: failed to synthesize
   HasQuotient (Synonym (Synonym R)) (Submodule R (Synonym (Synonym R)))
-use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/345.lean

@@ -6,7 +6,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 axiom bla : 1
@@ -17,7 +17,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 structure Foo where
@@ -29,7 +29,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Sort _
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 inductive Bla (x : 1) : Type

tests/lean/run/3554.lean

@@ -5,8 +5,12 @@ def foo : Nat → Nat
 set_option debug.moduleNameAtTimeout false
 /--
 error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
-use `set_option maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+---
+error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
+Use `set_option maxHeartbeats <num>` to set the limit.
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in

tests/lean/run/3996.lean

@@ -17,7 +17,7 @@ instance instB10000 : B 10000 where
 /--
 error: failed to synthesize
   A
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #synth A -- should fail quickly

tests/lean/run/4203.lean

@@ -14,7 +14,7 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
 /--
 error: failed to synthesize
   Fintype v
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder

tests/lean/run/4365.lean

@@ -37,7 +37,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : String)
@@ -48,7 +48,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool)
@@ -59,7 +59,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
   Bool → Nat
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool → Nat)
@@ -70,7 +70,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
   String
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def foo : String :=

tests/lean/run/by_cases.lean

@@ -13,7 +13,7 @@ example (p : Prop) : True := by
 /--
 error: failed to synthesize
   Decidable p
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 example (p : Prop) : True := by

tests/lean/run/diagnosticsMsgOptional.lean

@@ -0,0 +1,20 @@
+/-!
+# Mentioning `set_option diagnostics true` depends on it not already being set
+-/
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth Coe Nat Int
+
+set_option diagnostics true
+
+/--
+error: failed to synthesize
+  Coe Nat Int
+-/
+#guard_msgs in
+#synth Coe Nat Int

tests/lean/run/guard_msgs.lean

@@ -51,7 +51,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `22` cannot be used in a context where the expected type is
   α
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs(error) in
 example : α := 22
@@ -107,15 +107,15 @@ Lax whitespace
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
 
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available by using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)