feat: improve done tactic in grind interactive mode

This PR improves the `done` tactic in `grind` interactive mode. It now
displays the `grind` state diagnostics for all unsolved subgoals.

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -167,12 +167,6 @@ where
 def throwNoGoalsToBeSolved : GrindTacticM α :=
   throwError "No goals to be solved"
 
-def done : GrindTacticM Unit := do
-  let gs ← getUnsolvedGoalMVarIds
-  unless gs.isEmpty do
-    Term.reportUnsolvedGoals gs
-    throwAbortTactic
-
 instance : MonadBacktrack SavedState GrindTacticM where
   saveState := Grind.saveState
   restoreState b := b.restore
@@ -190,31 +184,6 @@ def focus (k : GrindTacticM α) : GrindTacticM α := do
   setGoals (mvarIds' ++ mvarIds)
   pure a
 
-/--
-Runs `tactic` with only the first unsolved goal as the goal, and expects it leave no goals.
-Fails if there are no goal to be solved.
--/
-def focusAndDone (tactic : GrindTacticM α) : GrindTacticM α :=
-  focus do
-    let a ← tactic
-    done
-    pure a
-
-/-- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
-def closeUsingOrAdmit (tac : GrindTacticM Unit) : GrindTacticM Unit := do
-  /- Important: we must define `closeUsingOrAdmit` before we define
-     the instance `MonadExcept` for `GrindTacticM` since it backtracks the state including error messages. -/
-  let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
-  tryCatchRuntimeEx
-    (focusAndDone tac)
-    fun ex => do
-      if (← read).recover then
-        logException ex
-        admitGoal goal.mvarId
-        setGoals goals
-      else
-        throw ex
-
 /--
 Non-backtracking `try`/`catch`.
 -/
@@ -341,6 +310,43 @@ def liftSearchM (k : SearchM α) : GrindTacticM α := do
   replaceMainGoal [state.goal]
   return a
 
+def done : GrindTacticM Unit := do
+  pruneSolvedGoals
+  let goals ← getGoals
+  unless goals.isEmpty do
+    let params := (← read).params
+    let results ← liftGrindM do goals.mapM fun goal => Grind.mkResult params (some goal)
+    let msgs ← results.mapM fun result => result.toMessageData
+    let msg := MessageData.joinSep msgs m!"\n\n"
+    logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{msg}"
+    goals.forM fun goal => admitGoal goal.mvarId
+    throwAbortTactic
+
+/--
+Runs `tactic` with only the first unsolved goal as the goal, and expects it leave no goals.
+Fails if there are no goal to be solved.
+-/
+def focusAndDone (tactic : GrindTacticM α) : GrindTacticM α :=
+  focus do
+    let a ← tactic
+    done
+    pure a
+
+/-- Close the main goal using the given tactic. If it fails, log the error and `admit` -/
+def closeUsingOrAdmit (tac : GrindTacticM Unit) : GrindTacticM Unit := do
+  /- Important: we must define `closeUsingOrAdmit` before we define
+     the instance `MonadExcept` for `GrindTacticM` since it backtracks the state including error messages. -/
+  let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
+  tryCatchRuntimeEx
+    (focusAndDone tac)
+    fun ex => do
+      if (← read).recover then
+        logException ex
+        admitGoal goal.mvarId
+        setGoals goals
+      else
+        throw ex
+
 def GrindTacticM.run (x : GrindTacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
   x ctx |>.run s
 

tests/lean/run/grind_interactive.lean

@@ -311,7 +311,7 @@ h✝ : as = []
 -/
 #guard_msgs in
 example : h bs = 1 → h as ≠ 0 := by
-  grind [h.eq_def] =>
+  grind -verbose [h.eq_def] =>
     instantiate
     cases #dce6
     next => skip
@@ -501,7 +501,7 @@ r p q : Prop
 -/
 #guard_msgs in
 example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
-  grind =>
+  grind -verbose =>
     rename_i h1 _ h2 _
     done