feat: improvegrind diagnostic information (#6656)

This PR improves the diagnostic information provided in `grind` failure
states. We now include the list of issues found during the search, and
all search thresholds that have been reached. This PR also improves its
formatting.

src/Lean/Elab/Tactic/Grind.lean

@@ -37,7 +37,7 @@ def elabGrindPattern : CommandElab := fun stx => do
 def grind (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) (fallback : Grind.Fallback) : MetaM Unit := do
   let goals ← Grind.main mvarId config mainDeclName fallback
   unless goals.isEmpty do
-    throwError "`grind` failed\n{← Grind.goalsToMessageData goals}"
+    throwError "`grind` failed\n{← Grind.goalsToMessageData goals config}"
 
 private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit) := do
   let some fallback := fallback? | return (pure ())

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
   | _ =>
-   trace_goal[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   reportIssue m!"unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -250,7 +250,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
-    trace_goal[grind.issues] "unexpected number of parameters at {← thm.origin.pp}"
+    reportIssue m!"unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
@@ -260,22 +260,22 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       let mvarIdType ← mvarId.getType
       let vType ← inferType v
       unless (← isDefEq mvarIdType vType <&&> mvarId.checkedAssign v) do
-        trace_goal[grind.issues] "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+        reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
         return ()
   -- Synthesize instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstance mvar type) do
-        trace_goal[grind.issues] "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        reportIssue m!"failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
     addNewInstance thm.origin proof c.gen
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      trace_goal[grind.issues] "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      reportIssue m!"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.origin proof c.gen
 where

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -77,7 +77,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
-    trace[grind.issues] "failed to create E-match local theorem for{indentExpr e}"
+    reportIssue m!"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 ()

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -24,7 +24,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        trace_goal[grind.issues] "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        reportIssue m!"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
@@ -168,7 +168,7 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
   | .mvar ..
   | .mdata ..
   | .proj .. =>
-    trace_goal[grind.issues] "unexpected term during internalization{indentExpr e}"
+    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"
     mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
   | .app .. =>
     if (← isLitValue e) then

src/Lean/Meta/Tactic/Grind/PP.lean

@@ -76,10 +76,16 @@ private def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsEle
   let es := es.map fun e => .trace { cls := clsElem} m!"{e}" #[]
   .trace { cls } header es
 
-private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
+private abbrev M := ReaderT Goal (StateT (Array MessageData) MetaM)
+
+private def pushMsg (m : MessageData) : M Unit :=
+  modify fun s => s.push m
+
+private def ppEqcs : M Unit := do
    let mut trueEqc?  : Option MessageData := none
    let mut falseEqc? : Option MessageData := none
    let mut otherEqcs : Array MessageData := #[]
+   let goal ← read
    for eqc in goal.getEqcs do
      if Option.isSome <| eqc.find? (·.isTrue) then
        let eqc := eqc.filter fun e => !e.isTrue
@@ -93,44 +99,68 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
        -- We may want to add a flag to pretty print equivalence classes of nested proofs
        unless (← isProof e) do
          otherEqcs := otherEqcs.push <| .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) #[]
-   let mut result := #[]
-   if let some trueEqc := trueEqc? then result := result.push trueEqc
-   if let some falseEqc := falseEqc? then result := result.push falseEqc
+   if let some trueEqc := trueEqc? then pushMsg trueEqc
+   if let some falseEqc := falseEqc? then pushMsg falseEqc
    unless otherEqcs.isEmpty do
-     result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
-   return result
+     pushMsg <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
 
 private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
   let m := m!"{← thm.origin.pp}:\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
   return .trace { cls := `thm } m #[]
 
-private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
-  let m ← goal.thms.toArray.mapM ppEMatchTheorem
-  let m := m ++ (← goal.newThms.toArray.mapM ppEMatchTheorem)
-  if m.isEmpty then
-    return ""
-  else
-    return .trace { cls := `ematch } "E-matching" m
+private def ppActiveTheorems : M Unit := do
+  let goal ← read
+  let m ← goal.thms.toArray.mapM fun thm => ppEMatchTheorem thm
+  let m := m ++ (← goal.newThms.toArray.mapM fun thm => ppEMatchTheorem thm)
+  unless m.isEmpty do
+    pushMsg <| .trace { cls := `ematch } "E-matching" m
 
-def ppOffset (goal : Goal) : MetaM MessageData := do
+private def ppOffset : M Unit := do
+  let goal ← read
   let s := goal.arith.offset
   let nodes := s.nodes
-  if nodes.isEmpty then return ""
+  if nodes.isEmpty then return ()
   let model ← Arith.Offset.mkModel goal
   let mut ms := #[]
   for (e, val) in model do
     ms := ms.push <| .trace { cls := `assign } m!"{e} := {val}" #[]
-  return .trace { cls := `offset } "Assignment satisfying offset contraints" ms
-
-def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
-  let mut m : Array MessageData := #[.ofGoal goal.mvarId]
-  m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
-  m := m ++ (← ppEqcs goal)
-  m := m.push (← ppActiveTheorems goal)
-  m := m.push (← ppOffset goal)
-  addMessageContextFull <| MessageData.joinSep m.toList ""
-
-def goalsToMessageData (goals : List Goal) : MetaM MessageData :=
-  return MessageData.joinSep (← goals.mapM goalToMessageData) m!"\n"
+  pushMsg <| .trace { cls := `offset } "Assignment satisfying offset contraints" ms
+
+private def ppIssues : M Unit := do
+  let issues := (← read).issues
+  unless issues.isEmpty do
+    pushMsg <| .trace { cls := `issues } "Issues" issues.reverse.toArray
+
+private def ppThresholds (c : Grind.Config) : M Unit := do
+  let goal ← read
+  let maxGen := goal.enodes.foldl (init := 0) fun g _ n => Nat.max g n.generation
+  let mut msgs := #[]
+  if goal.numInstances ≥ c.instances  then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of instances generated by E-matching has been reached, threshold: `(instances := {c.instances})`" #[]
+  if goal.numEmatch ≥ c.ematch  then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of E-matching rounds has been reached, threshold: `(ematch := {c.ematch})`" #[]
+  if goal.numSplits ≥ c.splits then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum number of case-splits has been reached, threshold: `(splits := {c.splits})`" #[]
+  if maxGen ≥ c.gen then
+    msgs := msgs.push <| .trace { cls := `limit } m!"maximum term generation has been reached, threshold: `(gen := {c.gen})`" #[]
+  unless msgs.isEmpty do
+    pushMsg <| .trace { cls := `limits } "Thresholds reached" 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
+where
+  go : M Unit := do
+    pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
+    ppEqcs
+    ppActiveTheorems
+    ppOffset
+    ppThresholds config
+    ppIssues
+
+def goalsToMessageData (goals : List Goal) (config : Grind.Config) : MetaM MessageData :=
+  return MessageData.joinSep (← goals.mapM (goalToMessageData · config)) m!"\n"
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -384,6 +384,11 @@ structure Goal where
   nextThmIdx : Nat := 0
   /-- Asserted facts -/
   facts      : PArray Expr := {}
+  /--
+  Issues found during the proof search in this goal. This issues are reported to
+  users when `grind` fails.
+  -/
+  issues     : List MessageData := []
   deriving Inhabited
 
 def Goal.admit (goal : Goal) : MetaM Unit :=
@@ -411,6 +416,15 @@ def updateLastTag : GoalM Unit := do
       trace[grind] "working on goal `{currTag}`"
       modifyThe Grind.State fun s => { s with lastTag := currTag }
 
+def reportIssue (msg : MessageData) : GoalM Unit := do
+  let msg ← addMessageContext msg
+  modify fun s => { s with issues := .trace { cls := `issue } msg #[] :: s.issues }
+  /-
+  We also add a trace message because we may want to know when
+  an issue happened relative to other trace messages.
+  -/
+  trace[grind.issues] msg
+
 /--
 Macro similar to `trace[...]`, but it includes the trace message `trace[grind] "working on <current goal>"`
 if the tag has changed since the last trace message.