From 38086a83cb32656c75c7c8ed06e3d1a8c25c9d12 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 1 Feb 2025 13:12:00 -0800
Subject: [PATCH] feat: add `Grind.Config.verbose` and `reportIssue!` macro
 (#6904)

This PR adds the `grind` configuration option `verbose`. For example,
`grind -verbose` disables all diagnostics. We are going to use this flag
to implement `try?`.
---
 src/Init/Grind/Tactics.lean                 |  2 ++
 src/Lean/Meta/Tactic/Grind/Canon.lean       |  2 +-
 src/Lean/Meta/Tactic/Grind/Ctor.lean        |  2 +-
 src/Lean/Meta/Tactic/Grind/EMatch.lean      |  8 ++++----
 src/Lean/Meta/Tactic/Grind/Ext.lean         |  6 +++---
 src/Lean/Meta/Tactic/Grind/ForallProp.lean  |  2 +-
 src/Lean/Meta/Tactic/Grind/Internalize.lean |  8 ++++----
 src/Lean/Meta/Tactic/Grind/Main.lean        | 17 +++++++++--------
 src/Lean/Meta/Tactic/Grind/MatchCond.lean   |  4 ++--
 src/Lean/Meta/Tactic/Grind/PP.lean          | 11 +++++++----
 src/Lean/Meta/Tactic/Grind/Solve.lean       |  2 +-
 src/Lean/Meta/Tactic/Grind/Split.lean       |  2 +-
 src/Lean/Meta/Tactic/Grind/Types.lean       |  9 +++++++++
 tests/lean/run/grind_t1.lean                | 13 +++++++++++++
 14 files changed, 58 insertions(+), 30 deletions(-)

diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 59cfe83d16e6..3a51da8ebe32 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -65,6 +65,8 @@ structure Config where
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems available in the environment. -/
   ext : Bool := true
+  /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
+  verbose : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean
index 7addde37dde9..d0b89fa4e032 100644
--- a/src/Lean/Meta/Tactic/Grind/Canon.lean
+++ b/src/Lean/Meta/Tactic/Grind/Canon.lean
@@ -60,7 +60,7 @@ private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do
       withDefault <| isDefEq a b)
     fun ex => do
       if ex.isRuntime then
-        reportIssue m!"failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`"
+        reportIssue! "failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`"
         return false
       else
         throw ex
diff --git a/src/Lean/Meta/Tactic/Grind/Ctor.lean b/src/Lean/Meta/Tactic/Grind/Ctor.lean
index 53c6922de653..9bc9478f0d8e 100644
--- a/src/Lean/Meta/Tactic/Grind/Ctor.lean
+++ b/src/Lean/Meta/Tactic/Grind/Ctor.lean
@@ -20,7 +20,7 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit :=
   | HEq _ lhs _ rhs =>
     pushHEq (← shareCommon lhs) (← shareCommon rhs) proof
   | _ =>
-   reportIssue m!"unexpected injectivity theorem result type{indentExpr eqs}"
+   reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean
index b480d4b4cadf..cb92e325307b 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean
@@ -268,7 +268,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   assert! c.assignment.size == numParams
   let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
   if mvars.size != thm.numParams then
-    reportIssue m!"unexpected number of parameters at {← thm.origin.pp}"
+    reportIssue! "unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
@@ -278,7 +278,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       let mvarIdType ← mvarId.getType
       let vType ← inferType v
       let report : M Unit := do
-        reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+        reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
       unless (← withDefault <| isDefEq mvarIdType vType) do
         let some heq ← proveEq? vType mvarIdType
           | report
@@ -297,7 +297,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue m!"failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        reportIssue! "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
@@ -305,7 +305,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      reportIssue m!"failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      reportIssue! "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm proof c.gen
 
diff --git a/src/Lean/Meta/Tactic/Grind/Ext.lean b/src/Lean/Meta/Tactic/Grind/Ext.lean
index e4b42b0da7b2..7b1abb2c65c9 100644
--- a/src/Lean/Meta/Tactic/Grind/Ext.lean
+++ b/src/Lean/Meta/Tactic/Grind/Ext.lean
@@ -14,14 +14,14 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   let c ← mkConstWithFreshMVarLevels thm.declName
   let (mvars, bis, type) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
   unless (← isDefEq e type) do
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nis not definitionally equal to{indentExpr type}"
+    reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nis not definitionally equal to{indentExpr type}"
     return ()
   -- Instantiate type class instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue m!"failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
+        reportIssue! "failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
         return ()
   -- Remark: `proof c mvars` has type `e`
   let proof ← instantiateMVars (mkAppN c mvars)
@@ -33,7 +33,7 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   let proof' ← instantiateMVars (← mkLambdaFVars mvars proof)
   let prop' ← inferType proof'
   if proof'.hasMVar || prop'.hasMVar then
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
+    reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
     return ()
   addNewFact proof' prop' ((← getGeneration e) + 1)
 
diff --git a/src/Lean/Meta/Tactic/Grind/ForallProp.lean b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
index 77a14c162b75..963f5e49e4fb 100644
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/src/Lean/Meta/Tactic/Grind/ForallProp.lean
@@ -78,7 +78,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
     if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
       activateTheorem thm gen
   if (← get).newThms.size == size then
-    reportIssue m!"failed to create E-match local theorem for{indentExpr e}"
+    reportIssue! "failed to create E-match local theorem for{indentExpr e}"
 
 def propagateForallPropDown (e : Expr) : GoalM Unit := do
   let .forallE n a b bi := e | return ()
diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index cb207d0af32b..46a3d548343c 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -27,7 +27,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        reportIssue m!"found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        reportIssue! "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
     trace_goal[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
@@ -231,13 +231,13 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
   | .lit .. | .const .. =>
     mkENode e generation
   | .mvar .. =>
-    reportIssue m!"unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
+    reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
     mkENode' e generation
   | .mdata .. =>
-    reportIssue m!"unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
+    reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
     mkENode' e generation
   | .proj .. =>
-    reportIssue m!"unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
+    reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
     mkENode' e generation
   | .app .. =>
     if (← isLitValue e) then
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index cadee3bce1b1..cc75dcd7f29c 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -131,14 +131,15 @@ def Result.hasFailures (r : Result) : Bool :=
 
 def Result.toMessageData (result : Result) : MetaM MessageData := do
   let mut msgs ← result.failures.mapM (goalToMessageData · result.config)
-  let mut issues := result.issues
-  unless result.skipped.isEmpty do
-    let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
-    issues := .trace { cls := `issue } m #[] :: issues
-  unless issues.isEmpty do
-    msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
-  if let some msg ← result.counters.toMessageData? then
-    msgs := msgs ++ [msg]
+  if result.config.verbose then
+    let mut issues := result.issues
+    unless result.skipped.isEmpty do
+      let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
+      issues := .trace { cls := `issue } m #[] :: issues
+    unless issues.isEmpty do
+      msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
+    if let some msg ← result.counters.toMessageData? then
+      msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean
index 0d2edd0123c7..51587be1823c 100644
--- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean
+++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean
@@ -301,7 +301,7 @@ where
     -- created when we infer the type of the `noConfusion` term below
     let lhs ← shareCommon lhs
     let some root ← getRootENode? lhs
-      | reportIssue "found term that has not been internalized{indentExpr lhs}\nwhile trying to construct a proof for `MatchCond`{indentExpr e}"
+      | reportIssue! "found term that has not been internalized{indentExpr lhs}\nwhile trying to construct a proof for `MatchCond`{indentExpr e}"
         return none
     let isHEq := α?.isSome
     let h ← if isHEq then
@@ -430,7 +430,7 @@ builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do
   else
     if !(← isStatisfied e) then return ()
     let some h ← mkMatchCondProof? e
-       | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
+       | reportIssue! "failed to construct proof for{indentExpr e}"; return ()
     trace_goal[grind.debug.matchCond] "{← inferType h}"
     pushEqTrue e <| mkEqTrueCore e h
 
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index 4962933d8ba5..04511318962e 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -151,10 +151,13 @@ private def ppCasesTrace : M Unit := do
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do
-  let (_, m) ← go goal |>.run #[]
-  let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
-  let r := m!"{.ofGoal goal.mvarId}\n{gm}"
-  addMessageContextFull r
+  if config.verbose then
+    let (_, m) ← go goal |>.run #[]
+    let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
+    let r := m!"{.ofGoal goal.mvarId}\n{gm}"
+    addMessageContextFull r
+  else
+    return .ofGoal goal.mvarId
 where
   go : M Unit := do
     pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
diff --git a/src/Lean/Meta/Tactic/Grind/Solve.lean b/src/Lean/Meta/Tactic/Grind/Solve.lean
index cc243f25f27b..c9de66db8f85 100644
--- a/src/Lean/Meta/Tactic/Grind/Solve.lean
+++ b/src/Lean/Meta/Tactic/Grind/Solve.lean
@@ -40,7 +40,7 @@ def pushFailure (goal : Goal) : M Unit := do
     x goal
   catch ex =>
     if ex.isMaxHeartbeat || ex.isMaxRecDepth then
-      reportIssue ex.toMessageData
+      reportIssue! ex.toMessageData
       pushFailure goal
       return true
     else
diff --git a/src/Lean/Meta/Tactic/Grind/Split.lean b/src/Lean/Meta/Tactic/Grind/Split.lean
index 350dada02ec0..f7b5c1a01781 100644
--- a/src/Lean/Meta/Tactic/Grind/Split.lean
+++ b/src/Lean/Meta/Tactic/Grind/Split.lean
@@ -104,7 +104,7 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
     if e.isFVar then
       let type ← whnfD (← inferType e)
       let report : GoalM Unit := do
-        reportIssue "cannot perform case-split on {e}, unexpected type{indentExpr type}"
+        reportIssue! "cannot perform case-split on {e}, unexpected type{indentExpr type}"
       let .const declName _ := type.getAppFn | report; return .resolved
       let .inductInfo info ← getConstInfo declName | report; return .resolved
       return .ready info.ctors.length info.isRec
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 6cc50025e75e..d56084cc787e 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -244,6 +244,15 @@ def reportIssue (msg : MessageData) : GrindM Unit := do
   -/
   trace[grind.issues] msg
 
+private def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| do
+    if (← getConfig).verbose then
+      reportIssue $msg)
+
+macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportIssueMacro s.raw
+
 /--
 Stores information for a node in the egraph.
 Each internalized expression `e` has an `ENode` associated with it.
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index f1c57943b1f3..6c66acaae8e4 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -259,6 +259,19 @@ set_option trace.grind.split true in
 example (p q : Prop) : (p ↔ q) → p → False := by
   grind -- should not split on (p ↔ q)
 
+/--
+error: `grind` failed
+case grind
+p q : Prop
+a✝¹ : p = q
+a✝ : p
+⊢ False
+-/
+#guard_msgs (error) in
+example (p q : Prop) : (p ↔ q) → p → False := by
+  grind -verbose -- We should not get any diagnostics
+
+
 /--
 error: `grind` failed
 case grind