feat: finish? produces partial tactic scripts

This PR ensures that `finish?` produces partial tactic scripts containing `sorry`s.
We may add an option to disable this feature in the future.
It is enabled by default because it provides a useful way to debug `grind` failures.

Author: leodemoura

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

@@ -123,7 +123,15 @@ def loop (n : Nat) (x : Action) : Action := fun goal _ kp =>
 Runs action `a` on the given `goal`.
 -/
 def run (goal : Goal) (a : Action) : GrindM ActionResult := do
-  let k := fun goal => if goal.inconsistent then return .closed [] else return .stuck [goal]
+  let k := fun goal => do
+    if goal.inconsistent then
+      return .closed []
+    else if (← getConfig).trace then
+      goal.mvarId.admit
+      let sorryTac ← `(grind| sorry)
+      return .closed [sorryTac]
+    else
+      return .stuck [goal]
   a goal k k
 
 /--

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

@@ -294,7 +294,12 @@ hypotheses introduced during case analysis. If the proof is of the form `fun _ _
 -/
 private def getFalseProof? (mvarId : MVarId) : MetaM (Option Expr) := mvarId.withContext do
   let proof ← instantiateMVars (mkMVar mvarId)
-  go proof
+  if proof.hasSyntheticSorry then
+    /- **Note**: We do not perform non-chronological backtracking if the proof
+    contains synthetic `sorry`. -/
+    return none
+  else
+    go proof
 where
   go (proof : Expr) : MetaM (Option Expr) := do
     match_expr proof with
@@ -344,11 +349,25 @@ private def isCompressibleAlts (alts : Array (List (TSyntax `grind))) : Bool :=
   else
     true
 
+def isSorryAlt (alt : List (TSyntax `grind)) : Bool :=
+  match alt with
+  | [tac] => match tac with
+    | `(grind| sorry) => true
+    | _ => false
+  | _ => false
+
 private def mkCasesResultSeq (cases : TSyntax `grind) (alts : Array (List (TSyntax `grind)))
     (compress : Bool) : CoreM (List (TSyntax `grind)) := do
   if compress && isCompressibleAlts alts then
-    if h : alts.size > 0 then
-      return [(← mkCasesAndThen cases alts[0]!)]
+    if alts.size > 0 then
+      let firstAlt := alts[0]!
+      if isSorryAlt firstAlt then
+        /-
+        **Note**: It is a bit pointless to return a script of the form `cases #<anchor> <;> sorry`
+        -/
+        return firstAlt
+      else
+        return [(← mkCasesAndThen cases firstAlt)]
     else
       return [cases]
   else

tests/lean/run/grind_finish_trace.lean

@@ -60,3 +60,42 @@ example (as bs cs : Array α) (v₁ v₂ : α)
         (h₆ : j < as.size)
         : cs[j] = as[j] := by
   grind => finish?
+
+set_option warn.sorry false
+
+/--
+info: Try this:
+  [apply] ⏎
+    cases #c4b6
+    next =>
+      ring
+      cases #8c9f
+      next => ring
+      next => sorry
+    next =>
+      ring
+      cases #8c9f
+      next => ring
+      next => sorry
+-/
+#guard_msgs in
+example {α : Type} [CommRing α] (a b c d e : α) :
+    (a^2 = c * b ∨ e^2 = d * c) →
+    (b^2 = d*c ∨ b^2 = c*d) →
+    a*b*(b*a) = c^2*b*d := by
+ grind => finish?
+
+/--
+info: Try this:
+  [apply] ⏎
+    instantiate only [= Nat.min_def]
+    cases #7640
+    next => sorry
+    next =>
+      ring
+      lia
+-/
+#guard_msgs in
+example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
+    (_ : ¬as.size = 0) : min lo (as.size - 1) < i := by
+  grind => finish?