From 114f7e42f1abd10885e91698cd2910b1e4d76083 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 15 Oct 2025 08:03:07 -0700
Subject: [PATCH] feat: lazy message with `grind` state (#10791)

This PR adds a silent info message with the `grind` state in its
interactive mode. The message is shown only when there is exactly one
goal in the grind interactive mode. The condition is a workaround for
current limitations of our `InfoTree`.
---
 src/Lean/Elab/Tactic/Grind/Basic.lean | 15 +++++++++++++
 src/Lean/Meta/Tactic/Grind/PP.lean    | 31 ++++++++++++++++-----------
 2 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Grind/Basic.lean b/src/Lean/Elab/Tactic/Grind/Basic.lean
index c9efe60ede..df82451d2d 100644
--- a/src/Lean/Elab/Tactic/Grind/Basic.lean
+++ b/src/Lean/Elab/Tactic/Grind/Basic.lean
@@ -10,7 +10,9 @@ public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Main
 public import Lean.Meta.Tactic.Grind.SearchM
+import Lean.CoreM
 import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.PP
 public section
 namespace Lean.Elab.Tactic.Grind
 open Meta
@@ -87,6 +89,19 @@ def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx
 def mkInitialTacticInfo (stx : Syntax) : GrindTacticM (GrindTacticM Info) := do
   let mctxBefore  ← getMCtx
   let goalsBefore ← getUnsolvedGoalMVarIds
+  /-
+  **Note**: We only display the grind state if there is exactly one goal.
+  This is a hack because we currently use a silent info to display the grind state, and we cannot attach it after each goal.
+  We claim this is not a big deal since the user will probably use `next =>` to focus on subgoals.
+  -/
+  if let [goal]  ← getGoals then goal.withContext do
+    let config := (← read).params.config
+    let msg := MessageData.lazy fun ctx => do
+      let .ok msg ← EIO.toBaseIO <| ctx.runMetaM
+          <| Grind.goalDiagToMessageData goal config (header := "Grind state") (collapsedMain := false)
+        | return "Grind state could not be generated"
+      return msg
+    logAt (severity := .information) (isSilent := true) stx msg
   return mkTacticInfo mctxBefore goalsBefore stx
 
 @[inline] def withTacticInfoContext (stx : Syntax) (x : GrindTacticM α) : GrindTacticM α := do
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index d9555286ae..5b6546a7c9 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -153,7 +153,7 @@ end EqcFilter
 def ppEqc (eqc : List Expr) (children : Array MessageData := #[]) : MessageData :=
   .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) children
 
-private def ppEqcs : M Unit := do
+private def ppEqcs (collapsedProps := true) : M Unit := do
    let mut trueEqc?  : Option MessageData := none
    let mut falseEqc? : Option MessageData := none
    let mut regularEqcs : Array MessageData := #[]
@@ -163,11 +163,11 @@ private def ppEqcs : M Unit := do
      if Option.isSome <| eqc.find? (·.isTrue) then
        let eqc := eqc.filter fun e => !e.isTrue
        unless eqc.isEmpty do
-         trueEqc? := ppExprArray `eqc  "True propositions" eqc.toArray `prop
+         trueEqc? := ppExprArray `eqc  "True propositions" eqc.toArray `prop (collapsed := collapsedProps)
      else if Option.isSome <| eqc.find? (·.isFalse) then
        let eqc := eqc.filter fun e => !e.isFalse
        unless eqc.isEmpty do
-         falseEqc? := ppExprArray `eqc "False propositions" eqc.toArray `prop
+         falseEqc? := ppExprArray `eqc "False propositions" eqc.toArray `prop (collapsed := collapsedProps)
      else if let e :: _ :: _ := eqc then
        -- We may want to add a flag to pretty print equivalence classes of nested proofs
        unless (← isProof e) do
@@ -270,18 +270,15 @@ 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
-  if config.verbose then
-    let (_, m) ← go goal |>.run #[]
-    let gm := MessageData.trace { cls := `grind, collapsed := false } "Goal diagnostics" m
-    let r := m!"{.ofGoal goal.mvarId}\n{gm}"
-    addMessageContextFull r
-  else
-    return .ofGoal goal.mvarId
+def goalDiagToMessageData (goal : Goal) (config : Grind.Config) (header := "Goal diagnostics") (collapsedMain := true)
+     : MetaM MessageData := do
+  let (_, m) ← go goal |>.run #[]
+  let gm := MessageData.trace { cls := `grind, collapsed := false } header m
+  return gm
 where
   go : M Unit := do
-    pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
-    ppEqcs
+    pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop (collapsed := collapsedMain)
+    ppEqcs (collapsedProps := collapsedMain)
     ppCasesTrace
     ppActiveTheoremPatterns
     ppOffset
@@ -291,4 +288,12 @@ where
     ppAC
     ppThresholds config
 
+def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.withContext do
+  if config.verbose then
+    let gm ← goalDiagToMessageData goal config
+    let r := m!"{.ofGoal goal.mvarId}\n{gm}"
+    addMessageContextFull r
+  else
+    return .ofGoal goal.mvarId
+
 end Lean.Meta.Grind