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.
2025-01-15 12:57:28 -08:00 · 2025-01-15 12:57:28 -08:00 · 65175dc7d4
commit 65175dc7d4
parent 54f06ccd64
9 changed files with 226 additions and 123 deletions
--- a/src/Lean/Elab/Tactic/Grind.lean
+++ b/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 ())
--- 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
  | _ =>
-   trace_goal[grind.issues] "unexpected injectivity theorem result type{indentExpr eqs}"
+   reportIssue m!"unexpected injectivity theorem result type{indentExpr eqs}"
   return ()

 /--
--- a/src/Lean/Meta/Tactic/Grind/EMatch.lean
+++ b/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,14 +260,14 @@ 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
@ -275,7 +275,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
-      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
--- a/src/Lean/Meta/Tactic/Grind/ForallProp.lean
+++ b/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 ()
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/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
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/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
+  pushMsg <| .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 ""
+private def ppIssues : M Unit := do
+  let issues := (← read).issues
+  unless issues.isEmpty do
+    pushMsg <| .trace { cls := `issues } "Issues" issues.reverse.toArray

-def goalsToMessageData (goals : List Goal) : MetaM MessageData :=
-  return MessageData.joinSep (← goals.mapM goalToMessageData) m!"\n"
+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
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/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.
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@ -13,23 +13,27 @@ left : p
 right : q
 h✝ : b = false
 h : c = true
-⊢ False[facts] Asserted facts
-  [prop] a = true
-  [prop] b = true ∨ c = true
-  [prop] p
-  [prop] q
-  [prop] b = false ∨ a = false
-  [prop] b = false
-  [prop] c = true[eqc] True propositions
-  [prop] b = true ∨ c = true
-  [prop] p
-  [prop] q
-  [prop] b = false ∨ a = false
-  [prop] b = false
-  [prop] c = true[eqc] Equivalence classes
-  [eqc] {b = true, a = false}
-  [eqc] {b, false}
-  [eqc] {a, c, true}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a = true
+    [prop] b = true ∨ c = true
+    [prop] p
+    [prop] q
+    [prop] b = false ∨ a = false
+    [prop] b = false
+    [prop] c = true
+  [eqc] True propositions
+    [prop] b = true ∨ c = true
+    [prop] p
+    [prop] q
+    [prop] b = false ∨ a = false
+    [prop] b = false
+    [prop] c = true
+  [eqc] Equivalence classes
+    [eqc] {b = true, a = false}
+    [eqc] {b, false}
+    [eqc] {a, c, true}
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@ -46,16 +50,20 @@ h✝ : c = true
 left : p
 right : q
 h : b = false
-⊢ False[facts] Asserted facts
-  [prop] a = true
-  [prop] c = true
-  [prop] p
-  [prop] q
-  [prop] b = false[eqc] True propositions
-  [prop] p
-  [prop] q[eqc] Equivalence classes
-  [eqc] {b, false}
-  [eqc] {a, c, true}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a = true
+    [prop] c = true
+    [prop] p
+    [prop] q
+    [prop] b = false
+  [eqc] True propositions
+    [prop] p
+    [prop] q
+  [eqc] Equivalence classes
+    [eqc] {b, false}
+    [eqc] {a, c, true}
 -/
 #guard_msgs (error) in
 theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@ -70,14 +78,19 @@ i j : Nat
 h : j + 1 < i + 1
 h✝ : j + 1 ≤ i
 x✝ : ¬g (i + 1) j ⋯ = i + j + 1
-⊢ False[facts] Asserted facts
-  [prop] j + 1 ≤ i
-  [prop] ¬g (i + 1) j ⋯ = i + j + 1[eqc] True propositions
-  [prop] j + 1 ≤ i[eqc] False propositions
-  [prop] g (i + 1) j ⋯ = i + j + 1[offset] Assignment satisfying offset contraints
-  [assign] j := 0
-  [assign] i := 1
-  [assign] i + j := 1
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] j + 1 ≤ i
+    [prop] ¬g (i + 1) j ⋯ = i + j + 1
+  [eqc] True propositions
+    [prop] j + 1 ≤ i
+  [eqc] False propositions
+    [prop] g (i + 1) j ⋯ = i + j + 1
+  [offset] Assignment satisfying offset contraints
+    [assign] j := 0
+    [assign] i := 1
+    [assign] i + j := 1
 -/
 #guard_msgs (error) in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
@ -102,15 +115,18 @@ head_eq : a₁ = b₁
 x_eq : a₂ = b₂
 y_eq : a₃ = b₃
 tail_eq : as = bs
-⊢ False[facts] Asserted facts
-  [prop] a₁ = b₁
-  [prop] a₂ = b₂
-  [prop] a₃ = b₃
-  [prop] as = bs[eqc] Equivalence classes
-  [eqc] {as, bs}
-  [eqc] {a₃, b₃}
-  [eqc] {a₂, b₂}
-  [eqc] {a₁, b₁}
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] a₁ = b₁
+    [prop] a₂ = b₂
+    [prop] a₃ = b₃
+    [prop] as = bs
+  [eqc] Equivalence classes
+    [eqc] {as, bs}
+    [eqc] {a₃, b₃}
+    [eqc] {a₂, b₂}
+    [eqc] {a₁, b₁}
 -/
 #guard_msgs (error) in
 theorem ex3 (h : a₁ :: { x := a₂, y := a₃ : Point } :: as = b₁ :: { x := b₂, y := b₃} :: bs) : False := by
@ -133,22 +149,26 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : ¬r
-⊢ False[facts] Asserted facts
-  [prop] HEq p a
-  [prop] HEq q a
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] ¬r[eqc] True propositions
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] ¬p
-  [prop] ¬r[eqc] False propositions
-  [prop] a
-  [prop] p
-  [prop] q
-  [prop] r
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq p a
+    [prop] HEq q a
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] ¬r
+  [eqc] True propositions
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] ¬p
+    [prop] ¬r
+  [eqc] False propositions
+    [prop] a
+    [prop] p
+    [prop] q
+    [prop] r
 case grind.2
 α : Type
 a : α
@ -158,22 +178,26 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : p
-⊢ False[facts] Asserted facts
-  [prop] HEq p a
-  [prop] HEq q a
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] p[eqc] True propositions
-  [prop] p = r
-  [prop] ¬p ∨ r
-  [prop] ¬r ∨ p
-  [prop] a
-  [prop] p
-  [prop] q
-  [prop] r[eqc] False propositions
-  [prop] ¬p
-  [prop] ¬r
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq p a
+    [prop] HEq q a
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] p
+  [eqc] True propositions
+    [prop] p = r
+    [prop] ¬p ∨ r
+    [prop] ¬r ∨ p
+    [prop] a
+    [prop] p
+    [prop] q
+    [prop] r
+  [eqc] False propositions
+    [prop] ¬p
+    [prop] ¬r
 -/
 #guard_msgs (error) in
 example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h₃ : p = r) → False := by
@ -200,3 +224,31 @@ set_option trace.grind.debug.proof false in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
  fail_if_success grind
  sorry
+
+/--
+error: `grind` failed
+case grind
+f : Nat → Bool
+g : Int → Bool
+a : Nat
+b : Int
+a✝¹ : HEq f g
+a✝ : HEq a b
+x✝ : ¬f a = g b
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] HEq f g
+    [prop] HEq a b
+    [prop] ¬f a = g b
+  [eqc] False propositions
+    [prop] f a = g b
+  [eqc] Equivalence classes
+    [eqc] {a, b}
+    [eqc] {f, g}
+  [issues] Issues
+    [issue] found congruence between g b and f a but functions have different types
+-/
+#guard_msgs (error) in
+example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
+  grind
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@ -244,12 +244,15 @@ case grind
 p q : Prop
 a✝¹ : p = q
 a✝ : p
-⊢ False[facts] Asserted facts
-  [prop] p = q
-  [prop] p[eqc] True propositions
-  [prop] p = q
-  [prop] q
-  [prop] p
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] p = q
+    [prop] p
+  [eqc] True propositions
+    [prop] p = q
+    [prop] q
+    [prop] p
 -/
 #guard_msgs (error) in
 set_option trace.grind.split true in
@ -262,13 +265,17 @@ case grind
 p q : Prop
 a✝¹ : p = ¬q
 a✝ : p
-⊢ False[facts] Asserted facts
-  [prop] p = ¬q
-  [prop] p[eqc] True propositions
-  [prop] p = ¬q
-  [prop] ¬q
-  [prop] p[eqc] False propositions
-  [prop] q
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] p = ¬q
+    [prop] p
+  [eqc] True propositions
+    [prop] p = ¬q
+    [prop] ¬q
+    [prop] p
+  [eqc] False propositions
+    [prop] q
 -/
 #guard_msgs (error) in
 set_option trace.grind.split true in