From d5e7dbad8071eccf40f2b49ba4145f3799510afe Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 30 Jul 2024 20:53:09 -0700 Subject: [PATCH] fix: make "use `set_option diagnostics true" message conditional on current 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 | 17 ++++++++-- src/Lean/Elab/Calc.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 4 +-- tests/lean/1007.lean.expected.out | 2 +- tests/lean/1102.lean.expected.out | 2 +- tests/lean/2040.lean.expected.out | 6 ++-- tests/lean/2220.lean.expected.out | 4 +-- tests/lean/2273.lean.expected.out | 2 +- tests/lean/297.lean.expected.out | 2 +- tests/lean/386.lean.expected.out | 2 +- tests/lean/448.lean.expected.out | 2 +- tests/lean/attrCmd.lean.expected.out | 2 +- tests/lean/calcErrors.lean.expected.out | 2 +- tests/lean/defInst.lean.expected.out | 2 +- tests/lean/defaultInstance.lean.expected.out | 2 +- .../eagerUnfoldingIssue.lean.expected.out | 4 +-- tests/lean/eraseInsts.lean.expected.out | 2 +- tests/lean/forErrors.lean.expected.out | 2 +- tests/lean/kernelMVarBug.lean.expected.out | 2 +- tests/lean/macroStack.lean.expected.out | 2 +- tests/lean/macroSwizzle.lean.expected.out | 2 +- tests/lean/openScoped.lean.expected.out | 2 +- tests/lean/prvCtor.lean.expected.out | 2 +- tests/lean/run/1163.lean | 4 +-- tests/lean/run/3313.lean | 1 - tests/lean/run/345.lean | 6 ++-- tests/lean/run/3554.lean | 8 +++-- tests/lean/run/3996.lean | 2 +- tests/lean/run/4203.lean | 2 +- tests/lean/run/4365.lean | 8 ++--- tests/lean/run/by_cases.lean | 2 +- tests/lean/run/diagnosticsMsgOptional.lean | 20 ++++++++++++ tests/lean/run/guard_msgs.lean | 6 ++-- tests/lean/run/isDefEqProjIssue.lean | 32 +++++++++++++++++-- tests/lean/sanitychecks.lean.expected.out | 2 +- tests/lean/scopedLocalInsts.lean.expected.out | 6 ++-- .../semicolonOrLinebreak.lean.expected.out | 2 +- tests/lean/setLit.lean.expected.out | 4 +-- tests/lean/tcloop.lean.expected.out | 9 ++---- tests/lean/typeOf.lean.expected.out | 4 +-- 41 files changed, 125 insertions(+), 66 deletions(-) create mode 100644 tests/lean/run/diagnosticsMsgOptional.lean diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 75eae9b8ad..0e79af6a73 100644 --- a/src/Lean/CoreM.lean +++ b/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} ` 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} ` to set the limit.\ + {useDiagnosticMsg}" def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do unless max == 0 do diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean index fa4d275895..d5586da4db 100644 --- a/src/Lean/Elab/Calc.lean +++ b/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. diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 3d4c4c7623..ea14af6e70 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index afd5129422..e412bfe451 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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 diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out index 535431abf0..f947d152d2 100644 --- a/tests/lean/1007.lean.expected.out +++ b/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. diff --git a/tests/lean/1102.lean.expected.out b/tests/lean/1102.lean.expected.out index d94f2b5cb6..127e652fdb 100644 --- a/tests/lean/1102.lean.expected.out +++ b/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. diff --git a/tests/lean/2040.lean.expected.out b/tests/lean/2040.lean.expected.out index 9cf0cfb86e..9788138631 100644 --- a/tests/lean/2040.lean.expected.out +++ b/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 diff --git a/tests/lean/2220.lean.expected.out b/tests/lean/2220.lean.expected.out index 8b03b90883..22390ad15f 100644 --- a/tests/lean/2220.lean.expected.out +++ b/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 diff --git a/tests/lean/2273.lean.expected.out b/tests/lean/2273.lean.expected.out index c15377bb35..dcc0ceb92c 100644 --- a/tests/lean/2273.lean.expected.out +++ b/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. diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out index 7c265e378c..d7ca31788d 100644 --- a/tests/lean/297.lean.expected.out +++ b/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. diff --git a/tests/lean/386.lean.expected.out b/tests/lean/386.lean.expected.out index 21c952dd87..530fa5ba18 100644 --- a/tests/lean/386.lean.expected.out +++ b/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. diff --git a/tests/lean/448.lean.expected.out b/tests/lean/448.lean.expected.out index 14d369862a..ec80bfed69 100644 --- a/tests/lean/448.lean.expected.out +++ b/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. diff --git a/tests/lean/attrCmd.lean.expected.out b/tests/lean/attrCmd.lean.expected.out index 814c35d447..5551509eae 100644 --- a/tests/lean/attrCmd.lean.expected.out +++ b/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. diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out index 2ac5779a74..85598c69c5 100644 --- a/tests/lean/calcErrors.lean.expected.out +++ b/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 diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out index 8bb2e82879..4014c89f3d 100644 --- a/tests/lean/defInst.lean.expected.out +++ b/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 diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out index 8612de8a01..ce40f49119 100644 --- a/tests/lean/defaultInstance.lean.expected.out +++ b/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) diff --git a/tests/lean/eagerUnfoldingIssue.lean.expected.out b/tests/lean/eagerUnfoldingIssue.lean.expected.out index ff3e277fa7..098500b40a 100644 --- a/tests/lean/eagerUnfoldingIssue.lean.expected.out +++ b/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. diff --git a/tests/lean/eraseInsts.lean.expected.out b/tests/lean/eraseInsts.lean.expected.out index 7fbc16acae..d4bbcf4593 100644 --- a/tests/lean/eraseInsts.lean.expected.out +++ b/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. diff --git a/tests/lean/forErrors.lean.expected.out b/tests/lean/forErrors.lean.expected.out index 860344f9ea..911b25b697 100644 --- a/tests/lean/forErrors.lean.expected.out +++ b/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. diff --git a/tests/lean/kernelMVarBug.lean.expected.out b/tests/lean/kernelMVarBug.lean.expected.out index 19feec3023..70cd682386 100644 --- a/tests/lean/kernelMVarBug.lean.expected.out +++ b/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. diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out index f044792348..9cfb577c7c 100644 --- a/tests/lean/macroStack.lean.expected.out +++ b/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 diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out index a5f6b79cda..b250009a78 100644 --- a/tests/lean/macroSwizzle.lean.expected.out +++ b/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 diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out index f2449eb935..0a23b21693 100644 --- a/tests/lean/openScoped.lean.expected.out +++ b/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' diff --git a/tests/lean/prvCtor.lean.expected.out b/tests/lean/prvCtor.lean.expected.out index a1de1f6b0f..e3c95f1e05 100644 --- a/tests/lean/prvCtor.lean.expected.out +++ b/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 diff --git a/tests/lean/run/1163.lean b/tests/lean/run/1163.lean index cdd3b44d61..26685b4548 100644 --- a/tests/lean/run/1163.lean +++ b/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 diff --git a/tests/lean/run/3313.lean b/tests/lean/run/3313.lean index 1b81992add..62a5180a9c 100644 --- a/tests/lean/run/3313.lean +++ b/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 diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean index fd99507518..a00bb02d27 100644 --- a/tests/lean/run/345.lean +++ b/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 diff --git a/tests/lean/run/3554.lean b/tests/lean/run/3554.lean index ac3afc8ef3..8458c60d40 100644 --- a/tests/lean/run/3554.lean +++ b/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 ` to set the limit -use `set_option diagnostics true` to get diagnostic information +Use `set_option maxHeartbeats ` 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 ` 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 diff --git a/tests/lean/run/3996.lean b/tests/lean/run/3996.lean index cd2592851c..dba0ec5f5a 100644 --- a/tests/lean/run/3996.lean +++ b/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 diff --git a/tests/lean/run/4203.lean b/tests/lean/run/4203.lean index 86caf423e4..bb3fc788d9 100644 --- a/tests/lean/run/4203.lean +++ b/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 diff --git a/tests/lean/run/4365.lean b/tests/lean/run/4365.lean index 5b7207adb6..29afb1caff 100644 --- a/tests/lean/run/4365.lean +++ b/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 := diff --git a/tests/lean/run/by_cases.lean b/tests/lean/run/by_cases.lean index 3289c1a7ff..b76280fff7 100644 --- a/tests/lean/run/by_cases.lean +++ b/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 diff --git a/tests/lean/run/diagnosticsMsgOptional.lean b/tests/lean/run/diagnosticsMsgOptional.lean new file mode 100644 index 0000000000..257cfa860e --- /dev/null +++ b/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 diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index 0135d4b599..c215bc5fa1 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/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,7 +107,7 @@ 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) @@ -115,7 +115,7 @@ use `set_option diagnostics true` to get diagnostic information /-- 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) diff --git a/tests/lean/run/isDefEqProjIssue.lean b/tests/lean/run/isDefEqProjIssue.lean index de429cecdf..e71137102d 100644 --- a/tests/lean/run/isDefEqProjIssue.lean +++ b/tests/lean/run/isDefEqProjIssue.lean @@ -52,8 +52,36 @@ where /-- error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached -use `set_option maxHeartbeats ` to set the limit -use `set_option diagnostics true` to get diagnostic information +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `elaborator`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. +--- +error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached +Use `set_option maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. -/ #guard_msgs in set_option backward.isDefEq.lazyWhnfCore false in diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out index 3958cd21a7..67a8f2eaf0 100644 --- a/tests/lean/sanitychecks.lean.expected.out +++ b/tests/lean/sanitychecks.lean.expected.out @@ -9,7 +9,7 @@ sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed sanitychecks.lean:10:0-10:23: error: failed to synthesize Inhabited False -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function False sanitychecks.lean:20:0-20:54: error: failed to compile partial definition 'Foo.unsound4', failed to show that type is inhabited and non empty diff --git a/tests/lean/scopedLocalInsts.lean.expected.out b/tests/lean/scopedLocalInsts.lean.expected.out index 9a3ab1cac8..d4bc1c5699 100644 --- a/tests/lean/scopedLocalInsts.lean.expected.out +++ b/tests/lean/scopedLocalInsts.lean.expected.out @@ -1,12 +1,12 @@ scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize ToString A -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. "A.mk 10 20" scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize ToString A -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. "{ x := 10, y := 20 }" scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize ToString A -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. "A.mk 10 20" diff --git a/tests/lean/semicolonOrLinebreak.lean.expected.out b/tests/lean/semicolonOrLinebreak.lean.expected.out index 2383a4e139..190bbfee00 100644 --- a/tests/lean/semicolonOrLinebreak.lean.expected.out +++ b/tests/lean/semicolonOrLinebreak.lean.expected.out @@ -7,4 +7,4 @@ term has type Nat semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize Singleton ?m Point -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. diff --git a/tests/lean/setLit.lean.expected.out b/tests/lean/setLit.lean.expected.out index 1f63e7cc4c..c2da77acbd 100644 --- a/tests/lean/setLit.lean.expected.out +++ b/tests/lean/setLit.lean.expected.out @@ -1,12 +1,12 @@ setLit.lean:22:19-22:21: error: overloaded, errors failed to synthesize EmptyCollection String - use `set_option diagnostics true` to get diagnostic information + Additional diagnostic information may be available by using the `set_option diagnostics true` command. fields missing: 'data' setLit.lean:24:31-24:38: error: overloaded, errors failed to synthesize Singleton Nat String - use `set_option diagnostics true` to get diagnostic information + Additional diagnostic information may be available by using the `set_option diagnostics true` command. 24:33 'val' is not a field of structure 'String' diff --git a/tests/lean/tcloop.lean.expected.out b/tests/lean/tcloop.lean.expected.out index 4b0a694e9a..dff58ab124 100644 --- a/tests/lean/tcloop.lean.expected.out +++ b/tests/lean/tcloop.lean.expected.out @@ -1,6 +1,3 @@ -tcloop.lean:14:2-14:15: error: failed to synthesize - B Nat -(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached -use `set_option synthInstance.maxHeartbeats ` to set the limit -use `set_option diagnostics true` to get diagnostic information -use `set_option diagnostics true` to get diagnostic information +tcloop.lean:14:2-14:15: error: (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached +Use `set_option synthInstance.maxHeartbeats ` to set the limit. +Additional diagnostic information may be available by using the `set_option diagnostics true` command. diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out index 65329e1845..53f3810095 100644 --- a/tests/lean/typeOf.lean.expected.out +++ b/tests/lean/typeOf.lean.expected.out @@ -1,9 +1,9 @@ typeOf.lean:11:22-11:25: error: failed to synthesize HAdd Nat Nat Bool -use `set_option diagnostics true` to get diagnostic information +Additional diagnostic information may be available by using the `set_option diagnostics true` command. typeOf.lean:12:0-12:5: error: failed to synthesize HAdd Bool 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. typeOf.lean:20:56-20:62: error: invalid reassignment, term has type Bool : Type but is expected to have type