refactor(TacticAnalysis): use full CommandElabM context in test (#29771)

Running the `rwMerge` linter on the whole of Mathlib reveals that the tactic analysis framework did not always correctly pass the environment to the test step of a pass. By running the test in a full `CommandElabM` and adding a `ContextInfo` and `TacticInfo`, we can access the right environment (using the `ctxI.runTacticCode` function). There are still a few subtle issues to do with notation but I would like to get this fix in first, since it involves some larger refactors.

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

Author: Vierkantor

Mathlib/Tactic/TacticAnalysis.lean

@@ -288,7 +288,7 @@ structure ComplexConfig where
   -/
   trigger (context : Option ctx) (currentTactic : Syntax) : TriggerCondition ctx
   /-- Code to run in the context of the tactic, for example an alternative tactic. -/
-  test (context : ctx) (goal : MVarId) : MetaM out
+  test (ctxI : ContextInfo) (i : TacticInfo) (context : ctx) (goal : MVarId) : CommandElabM out
   /-- Decides what to report to the user. -/
   tell (stx : Syntax) (originalSubgoals : List MVarId) (originalHeartbeats : Nat)
     (new : out) (newHeartbeats : Nat) : CommandElabM (Option MessageData)
@@ -311,7 +311,7 @@ def testTacticSeq (config : ComplexConfig) (tacticSeq : Array (TSyntax `tactic))
           if !i.mayFail then
             logWarning m!"original tactic '{stx}' failed: {e.toMessageData}"
           return [goal]
-      let (new, newHeartbeats) ← withHeartbeats <| i.ctxI.runTactic i.tacI goal <| config.test ctx
+      let (new, newHeartbeats) ← withHeartbeats <| config.test i.ctxI i.tacI ctx goal
       if let some msg ← config.tell stx oldGoals oldHeartbeats new newHeartbeats  then
         logWarning msg
 

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -6,7 +6,6 @@ Authors: Anne Baanen, Edward van de Meent
 import Mathlib.Tactic.TacticAnalysis
 import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.MinImports
-import Lean.Elab.Tactic.Meta
 import Lean.Elab.Command
 
 /-!
@@ -25,7 +24,7 @@ private inductive TerminalReplacementOutcome where
 | remainingGoals (stx : TSyntax `tactic) (goals : List MessageData)
 | error (stx : TSyntax `tactic) (msg : MessageData)
 
-open Elab.Command
+open Elab Command
 
 /--
 Define a pass that tries replacing one terminal tactic with another.
@@ -41,28 +40,30 @@ for example `Mathlib.Tactic.linarith`.
 in `stx` and the current `goal`.
 -/
 def terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind : SyntaxNodeKind)
-    (newTactic : Syntax → MVarId → MetaM (TSyntax `tactic))
+    (newTactic : ContextInfo → TacticInfo → Syntax → CommandElabM (TSyntax `tactic))
     (reportFailure : Bool := true) (reportSuccess : Bool := false)
     (reportSlowdown : Bool := false) (maxSlowdown : Float := 1) :
     TacticAnalysis.Config := .ofComplex {
   out := TerminalReplacementOutcome
   ctx := Syntax
   trigger _ stx := if stx.getKind == oldTacticKind
     then .accept stx else .skip
-  test stx goal := do
-    let tac ← newTactic stx goal
+  test ctxI i stx goal := do
+    let tac ← newTactic ctxI i stx
     try
-      let (goals, _) ← Lean.Elab.runTactic goal tac
+      let goals ← ctxI.runTacticCode i goal tac
       match goals with
       | [] => return .success tac
       | _ => do
         let goalsMessages ← goals.mapM fun g => do
-          let e ← instantiateMVars (← g.getType)
+          let e ← ctxI.runTactic i g <| fun g => do instantiateMVars (← g.getType)
           pure m!"⊢ {MessageData.ofExpr e}\n"
         return .remainingGoals tac goalsMessages
     catch _e =>
       let name ← mkAuxDeclName `extracted
-      let ((sig, _, modules), _) ← (Mathlib.Tactic.ExtractGoal.goalSignature name goal).run
+      -- Rerun in the original tactic context, since `omega` changes the state.
+      let ((sig, _, modules), _) ← ctxI.runTactic i goal (fun goal =>
+        (Mathlib.Tactic.ExtractGoal.goalSignature name goal).run)
       let imports := modules.toList.map (s!"import {·}")
       return .error tac m!"{"\n".intercalate imports}\n\ntheorem {sig} := by\n  fail_if_success {tac}\n  {stx}"
   tell stx old oldHeartbeats new newHeartbeats :=
@@ -118,7 +119,7 @@ def grindReplacementWith (tacticName : String) (tacticKind : SyntaxNodeKind)
     (reportFailure : Bool := true) (reportSuccess : Bool := false)
     (reportSlowdown : Bool := false) (maxSlowdown : Float := 1) :
     TacticAnalysis.Config :=
-  terminalReplacement tacticName "grind" tacticKind (fun _ _ => `(tactic| grind))
+  terminalReplacement tacticName "grind" tacticKind (fun _ _ _ => `(tactic| grind))
     reportFailure reportSuccess reportSlowdown maxSlowdown
 
 end Mathlib.TacticAnalysis
@@ -148,7 +149,7 @@ register_option linter.tacticAnalysis.regressions.omegaToCutsat : Bool := {
 @[tacticAnalysis linter.tacticAnalysis.regressions.omegaToCutsat,
   inherit_doc linter.tacticAnalysis.regressions.omegaToCutsat]
 def omegaToCutsatRegressions :=
-  terminalReplacement "omega" "cutsat" ``Lean.Parser.Tactic.omega (fun _ _ => `(tactic| cutsat))
+  terminalReplacement "omega" "cutsat" ``Lean.Parser.Tactic.omega (fun _ _ _ => `(tactic| cutsat))
     (reportSuccess := false) (reportFailure := true)
 
 /-- Report places where `omega` can be replaced by `cutsat`. -/
@@ -158,7 +159,7 @@ register_option linter.tacticAnalysis.omegaToCutsat : Bool := {
 @[tacticAnalysis linter.tacticAnalysis.omegaToCutsat,
   inherit_doc linter.tacticAnalysis.omegaToCutsat]
 def omegaToCutsat :=
-  terminalReplacement "omega" "cutsat" ``Lean.Parser.Tactic.omega (fun _ _ => `(tactic| cutsat))
+  terminalReplacement "omega" "cutsat" ``Lean.Parser.Tactic.omega (fun _ _ _ => `(tactic| cutsat))
     (reportSuccess := true) (reportFailure := false)
 
 /-- Suggest merging two adjacent `rw` tactics if that also solves the goal. -/
@@ -174,14 +175,18 @@ def Mathlib.TacticAnalysis.rwMerge : TacticAnalysis.Config := .ofComplex {
     match stx with
     | `(tactic| rw [$args,*]) => .continue ((ctx.getD #[]).push args)
     | _ => if let some args := ctx then if args.size > 1 then .accept args else .skip else .skip
-  test ctx goal := withOptions (fun opts => opts.set `grind.warning false) do
+  test ctxI i ctx goal := do
     let ctxT : Array (TSyntax `Lean.Parser.Tactic.rwRule) := ctx.flatten.map (⟨·⟩)
     let tac ← `(tactic| rw [$ctxT,*])
+    let oldMessages := (← get).messages
     try
-      let (goals, _) ← Lean.Elab.runTactic goal tac
+      let goals ← ctxI.runTacticCode i goal tac
       return (goals, ctxT.map (↑·))
     catch _e => -- rw throws an error if it fails to pattern-match.
       return ([goal], ctxT.map (↑·))
+    finally
+      -- Drop any messages, since they will appear as if they are genuine errors.
+      modify fun s => { s with messages := oldMessages }
   tell _stx _old _oldHeartbeats new _newHeartbeats := pure <|
     if new.1.isEmpty then
       m!"Try this: rw {new.2}"
@@ -351,11 +356,11 @@ def Mathlib.TacticAnalysis.introMerge : TacticAnalysis.Config := .ofComplex {
       -- if `intro` is used without arguments, treat it as `intro _`
       <| if args.size = 0 then #[⟨mkHole x⟩] else args)
     | _ => if let some args := ctx then if args.size > 1 then .accept args else .skip else .skip
-  test ctx goal := do
+  test ctxI i ctx goal := do
     let ctxT := ctx.flatten
     let tac ← `(tactic| intro $ctxT*)
     try
-      let _ ← Lean.Elab.runTactic goal tac
+      let _ ← ctxI.runTacticCode i goal tac
       return some tac
     catch _e => -- if for whatever reason we can't run `intro` here.
       return none

Mathlib/Tactic/Tauto.lean

@@ -231,7 +231,7 @@ register_option linter.tacticAnalysis.tautoToGrind : Bool := {
 @[tacticAnalysis linter.tacticAnalysis.tautoToGrind,
   inherit_doc linter.tacticAnalysis.tautoToGrind]
 def tautoToGrind :=
-  terminalReplacement "tauto" "grind" ``Mathlib.Tactic.Tauto.tauto (fun _ _ => `(tactic| grind))
+  terminalReplacement "tauto" "grind" ``Mathlib.Tactic.Tauto.tauto (fun _ _ _ => `(tactic| grind))
     (reportSuccess := true) (reportFailure := false)
 
 /-- Debug `grind` by identifying places where it does not yet supersede `tauto`. -/

MathlibTest/TacticAnalysis.lean

@@ -51,6 +51,30 @@ example : Fact (x = z) where
     rw [xy]
     rw [yz]
 
+universe u
+
+def a : PUnit.{u} := ⟨⟩
+def b : PUnit.{u} := ⟨⟩
+def c : PUnit.{u} := ⟨⟩
+theorem ab : a = b := rfl
+theorem bc : b = c := rfl
+
+/--
+warning: Try this: rw [ab.{u}, bc.{u}]
+-/
+#guard_msgs in
+example : a.{u} = c := by
+  rw [ab.{u}]
+  rw [bc.{u}]
+
+theorem xyz (h : x = z → y = z) : x = y := by rw [h yz]; rfl
+
+-- The next example tripped up `rwMerge` because `rw [xyz fun h => ?_, ← h, xy]` gives
+-- an unknown identifier `h`.
+example : x = y := by
+  rw [xyz fun h => ?_]
+  rw [← h, xy]
+
 end rwMerge
 
 section mergeWithGrind