fix: panic in tactic analysis framework (#31472)

The test added in this PR causes a panic on current mathlib, the panic being this one:
https://github.com/leanprover-community/mathlib4/blob/32fb6832e1009174e2787a2cbbc7669399175c61/Mathlib/Lean/ContextInfo.lean#L72 

This PR fixes the panic. The issue is in the tactic analysis framework's `terminalReplacement` linter builder. The idea with `terminalReplacement` is to try all `old_tactic` occurrences to see if swapping in `new_tactic` finishes at that point. If `new_tactic` works but doesn't finish it is supposed to print the new goal(s) produced by `new_tactic`; this is the case that was causing the panic.

The issue was that the `MetaM` call(s) to infer the type(s) of the new goal(s) were being routed through the `Lean.Elab.ContextInfo.runTactic` function, which panics if (as will typically be the case) one of these goals represents nontrivial progress from the previous goal state.  I have fixed this by storing the types of the new goals at the time they are generated, so we don't need `Lean.Elab.ContextInfo.runTactic` to cook up a new `MetaM` instance.

Author: hrmacbeth

Mathlib/Lean/ContextInfo.lean

@@ -78,12 +78,15 @@ def runTactic (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (x : MVarId 
     let goal ← Meta.mkFreshExprSyntheticOpaqueMVar type
     x goal.mvarId!
 
-/-- Run tactic code, given by a piece of syntax, in the context of an infotree node. -/
-def runTacticCode (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (code : Syntax) :
-    CommandElabM (List MVarId) := do
+/-- Run tactic code, given by a piece of syntax, in the context of an infotree node.
+The optional `MetaM` argument `m` performs postprocessing on the goals produced. -/
+def runTacticCode (ctx : ContextInfo) (i : TacticInfo) (goal : MVarId) (code : Syntax)
+    (m : Σ α : Type, MVarId → MetaM α := ⟨MVarId, pure⟩) :
+    CommandElabM (List m.1) := do
   let termCtx ← liftTermElabM read
   let termState ← liftTermElabM get
-  ctx.runTactic i goal fun goal =>
-    Lean.Elab.runTactic' (ctx := termCtx) (s := termState) goal code
+  ctx.runTactic i goal fun goal => do
+    let newGoals ← Lean.Elab.runTactic' (ctx := termCtx) (s := termState) goal code
+    newGoals.mapM m.2
 
 end Lean.Elab.ContextInfo

Mathlib/Tactic/TacticAnalysis.lean

@@ -354,3 +354,8 @@ def Config.ofComplex (config : ComplexConfig) : Config where
 end ComplexConfig
 
 end Mathlib.TacticAnalysis
+
+/-- A dummy option for testing the tactic analysis framework -/
+register_option linter.tacticAnalysis.dummy : Bool := {
+  defValue := false
+}

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -51,13 +51,11 @@ def terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind :
   test ctxI i stx goal := do
     let tac ← newTactic ctxI i stx
     try
-      let goals ← ctxI.runTacticCode i goal tac
-      match goals with
+      let goalTypes ← ctxI.runTacticCode i goal tac ⟨Expr, MVarId.getType'⟩
+      match goalTypes with
       | [] => return .success tac
       | _ => do
-        let goalsMessages ← goals.mapM fun g => do
-          let e ← ctxI.runTactic i g <| fun g => do instantiateMVars (← g.getType)
-          pure m!"⊢ {MessageData.ofExpr e}\n"
+        let goalsMessages := goalTypes.map fun e => m!"⊢ {MessageData.ofExpr e}\n"
         return .remainingGoals tac goalsMessages
     catch _e =>
       let name ← mkAuxDeclName `extracted

MathlibTest/TacticAnalysis.lean

@@ -15,6 +15,26 @@ example : 1 + 1 = 2 := by
 
 end omega
 
+@[tacticAnalysis linter.tacticAnalysis.dummy]
+def foo : Mathlib.TacticAnalysis.Config :=
+  Mathlib.TacticAnalysis.terminalReplacement "simp" "simp only" ``Lean.Parser.Tactic.simp
+    (fun _ _ _ => `(tactic| simp only))
+    (reportSuccess := true) (reportFailure := true)
+
+/--
+warning: `simp only` left unsolved goals where `simp` succeeded.
+Original tactic:
+  simp
+Replacement tactic:
+  simp only
+Unsolved goals:
+  [⊢ (List.map (fun x => x + 1) [1, 2, 3]).sum = 9 ]
+-/
+#guard_msgs in
+set_option linter.tacticAnalysis.dummy true in
+example : List.sum ([1,2,3].map fun x ↦ x + 1) = 9 := by
+  simp
+
 end terminalReplacement
 
 section rwMerge