fix(TacticAnalysis): include more CommandElabM state calling runTactic (#29505)

This PR fixes a few "unknown universe `v`" errors when running the tactic analysis framework on Mathlib. We need to move more state from the CommandElabM to the TermElabM that ends up running tactic code. Since we do essentially the same in a few places, bundle up all the state manipulation into a new function `runTacticCode`.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

Mathlib/Lean/ContextInfo.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 
+import Mathlib.Lean.Elab.Tactic.Meta
 -- Import this linter explicitly to ensure that
 -- this file has a valid copyright header and module docstring.
 import Mathlib.Tactic.Linter.Header
@@ -77,4 +78,12 @@ 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
+  let termCtx ← liftTermElabM read
+  let termState ← liftTermElabM get
+  ctx.runTactic i goal fun goal =>
+    Lean.Elab.runTactic' (ctx := termCtx) (s := termState) goal code
+
 end Lean.Elab.ContextInfo

Mathlib/Tactic/TacticAnalysis.lean

@@ -285,9 +285,9 @@ def testTacticSeq (config : ComplexConfig) (tacticSeq : Array (TSyntax `tactic))
   let stx ← `(tactic| $(tacticSeq);*)
   -- TODO: support more than 1 goal. Probably by requiring all tests to succeed in a row
   if let [goal] := i.goalsBefore then
-    let (oldGoals, oldHeartbeats) ← withHeartbeats <| ctxI.runTactic i goal fun goal => do
+    let (oldGoals, oldHeartbeats) ← withHeartbeats <|
       try
-        Lean.Elab.runTactic' goal stx
+        ctxI.runTacticCode i goal stx
       catch e =>
         logWarningAt stx m!"original tactic '{stx}' failed: {e.toMessageData}"
         return [goal]

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -117,14 +117,12 @@ def mergeWithGrind : TacticAnalysis.Config where
     if let #[(preCtx, preI), (_postCtx, postI)] := seq[0:2].array then
       if postI.stx.getKind == ``Lean.Parser.Tactic.grind then
         if let [goal] := preI.goalsBefore then
-          preCtx.runTactic preI goal <| fun goal => do
-            let tac := postI.stx
-            let (goals, _) ← try
-                Lean.Elab.runTactic goal tac
-              catch _e =>
-                pure ([goal], {})
-            if goals.isEmpty then
-              logWarningAt preI.stx m!"'{preI.stx}; grind' can be replaced with 'grind'"
+          let goals ← try
+            preCtx.runTacticCode preI goal postI.stx
+          catch _e =>
+            pure [goal]
+          if goals.isEmpty then
+            logWarningAt preI.stx m!"'{preI.stx}; grind' can be replaced with 'grind'"
 
 /-- Suggest replacing a sequence of tactics with `grind` if that also solves the goal. -/
 register_option linter.tacticAnalysis.terminalToGrind : Bool := {
@@ -153,27 +151,23 @@ def terminalToGrind : TacticAnalysis.Config where
           -- closes the goal like it does in userspace.
           let suffix := ⟨i.stx⟩ :: replaced
           let seq ← `(tactic| $suffix.toArray;*)
-          let (oldGoals, heartbeats) ← withHeartbeats <| ctx.runTactic i goal <| fun goal => do
-            let (goals, _) ←
-              try
-                Lean.Elab.runTactic goal seq
-              catch _e =>
-                pure ([goal], {})
-            return goals
+          let (oldGoals, heartbeats) ← withHeartbeats <|
+            try
+              ctx.runTacticCode i goal seq
+            catch _e =>
+              pure [goal]
           if !oldGoals.isEmpty then
             logWarningAt i.stx m!"Original tactics failed to solve the goal: {seq}"
           oldHeartbeats := heartbeats
 
           -- To check if `grind` can close the goal, run `grind` on the current goal
           -- and verify that no goals remain afterwards.
-          let (newGoals, heartbeats) ← withHeartbeats <| ctx.runTactic i goal <| fun goal => do
-            let tac ← `(tactic| grind)
-            let (goals, _) ←
-              try
-                Lean.Elab.runTactic goal tac
-              catch _e =>
-                pure ([goal], {})
-            return goals
+          let tac ← `(tactic| grind)
+          let (newGoals, heartbeats) ← withHeartbeats <|
+            try
+              ctx.runTacticCode i goal tac
+            catch _e =>
+              pure [goal]
           newHeartbeats := heartbeats
           if newGoals.isEmpty then
             success := true

MathlibTest/TacticAnalysis.lean

@@ -58,4 +58,19 @@ example : 1 + 1 = 2 := by
   have : 1 + 1 < 4 := by omega
   rfl
 
+universe u v
+
+-- This next example used to fail with `unknown universe level 'v'`.
+
+/--
+warning: replace the proof with 'grind': let T : Type max u v := Sigma f;
+  have : 1 + 1 = 2 := rfl;
+  rfl
+-/
+#guard_msgs in
+example {α : Type u} (f : α → Type max u v) : 1 = 1 := by
+  let T : Type max u v := Sigma f
+  have : 1 + 1 = 2 := rfl -- Extra line to ensure the linter picks it up.
+  rfl
+
 end replaceWithGrind