feat(TacticAnalysis): check if we are in a try/anyGoals context (#29964)

This PR adds a check if the tactic is being run in a `try` or `anyGoals` call, so that we do not add a warning for the original tactic failing in this context. This was the source of a few "original tactic failed" in the `grind` regression reports.

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

Author: Vierkantor

Mathlib/Tactic/TacticAnalysis.lean

@@ -46,6 +46,23 @@ register_option linter.tacticAnalysis : Bool := {
 
 namespace Mathlib.TacticAnalysis
 
+/-- Information about a tactic in a sequence, parsed from infotrees and passed to a tactic
+analysis pass. -/
+structure TacticNode where
+  /-- `ContextInfo` at the infotree node. -/
+  ctxI : ContextInfo
+  /-- `TacticInfo` at the infotree node. -/
+  tacI : TacticInfo
+  /-- This tactic is allowed to fail because it is in a `try`/`anyGoals`/etc block. -/
+  mayFail : Bool
+
+/-- Run tactic code, given by a piece of syntax, in the context of a tactic info node.
+
+Convenience abbreviation for `ContextInfo.runTacticCode`. -/
+abbrev TacticNode.runTacticCode (i : TacticNode) :
+    MVarId → Syntax → CommandElabM (List MVarId) :=
+  i.ctxI.runTacticCode i.tacI
+
 /-- Stores the configuration for a tactic analysis pass.
 
 This provides the low-level interface into the tactic analysis framework.
@@ -55,7 +72,7 @@ structure Config where
   to a sequence of tactics from the source file. Should do all reporting itself,
   for example by `Lean.Linter.logLint`.
   -/
-  run : Array (ContextInfo × TacticInfo) → CommandElabM Unit
+  run : Array TacticNode → CommandElabM Unit
 
 /-- The internal representation of a tactic analysis pass,
 extending `Config` with some declaration meta-information.
@@ -145,8 +162,7 @@ would result in three sequences:
 Similarly, a declaration with multiple `by` blocks results in each of the blocks getting its
 own sequence.
 -/
-def findTacticSeqs (tree : InfoTree) :
-    CommandElabM (Array (Array (ContextInfo × TacticInfo))) := do
+def findTacticSeqs (tree : InfoTree) : CommandElabM (Array (Array TacticNode)) := do
   -- Turn the CommandElabM into a surrounding context for traversing the tree.
   let ctx ← read
   let state ← get
@@ -177,7 +193,13 @@ def findTacticSeqs (tree : InfoTree) :
         -- We discard `childTactics` here, because those are either already picked up by a
         -- sequencing operator, or come from macros.
         if let .ofTacticInfo i := i then
-          return ((ctx, i), childSequences)
+          let childSequences :=
+            -- This tactic accepts the failure of its children.
+            if stx.getKind ∈ [``Lean.Parser.Tactic.tacticTry_, ``Lean.Parser.Tactic.anyGoals] then
+              childSequences.map (· |>.map fun i => { i with mayFail := true })
+            else
+              childSequences
+          return (some ⟨ctx, i, false⟩, childSequences)
         return (none, childSequences)
       else
         return (none, childSequences))
@@ -274,35 +296,36 @@ structure ComplexConfig where
 /-- Test the `config` against a sequence of tactics, using the context info and tactic info
 from the start of the sequence. -/
 def testTacticSeq (config : ComplexConfig) (tacticSeq : Array (TSyntax `tactic))
-    (ctxI : ContextInfo) (i : TacticInfo) (ctx : config.ctx) :
+    (i : TacticNode) (ctx : config.ctx) :
     CommandElabM Unit := do
   /- Syntax quotations use the current ref's position info even for nodes which do not usually
   carry position info. We set the ref here to ensure we log messages on the correct range. -/
   withRef (mkNullNode tacticSeq) do
     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
+    if let [goal] := i.tacI.goalsBefore then
       let (oldGoals, oldHeartbeats) ← withHeartbeats <|
         try
-          ctxI.runTacticCode i goal stx
+          i.runTacticCode goal stx
         catch e =>
-          logWarning m!"original tactic '{stx}' failed: {e.toMessageData}"
+          if !i.mayFail then
+            logWarning m!"original tactic '{stx}' failed: {e.toMessageData}"
           return [goal]
-      let (new, newHeartbeats) ← withHeartbeats <| ctxI.runTactic i goal <| config.test ctx
+      let (new, newHeartbeats) ← withHeartbeats <| i.ctxI.runTactic i.tacI goal <| config.test ctx
       if let some msg ← config.tell stx oldGoals oldHeartbeats new newHeartbeats  then
         logWarning msg
 
 /-- Run the `config` against a sequence of tactics, using the `trigger` to determine which
 subsequences should be `test`ed. -/
-def runPass (config : ComplexConfig) (seq : Array (ContextInfo × TacticInfo)) :
+def runPass (config : ComplexConfig) (seq : Array TacticNode) :
     CommandElabM Unit := do
   let mut acc := none
   let mut firstInfo := none
   let mut tacticSeq := #[]
-  for (ctxI, i) in seq do
+  for i in seq do
     if firstInfo.isNone then
-      firstInfo := some (ctxI, i)
-    let stx : TSyntax `tactic := ⟨i.stx⟩
+      firstInfo := some i
+    let stx : TSyntax `tactic := ⟨i.tacI.stx⟩
     tacticSeq := tacticSeq.push stx
     match config.trigger acc stx with
     | .continue ctx =>
@@ -312,16 +335,16 @@ def runPass (config : ComplexConfig) (seq : Array (ContextInfo × TacticInfo)) :
       tacticSeq := #[]
       firstInfo := none
     | .accept ctx =>
-      if let some (ctxI, i) := firstInfo then
-        testTacticSeq config tacticSeq ctxI i ctx
+      if let some i := firstInfo then
+        testTacticSeq config tacticSeq i ctx
       else
         logWarningAt stx m!"internal error in tactic analysis: accepted an empty sequence."
       acc := none
   -- Insert a `done` at the end so we can handle a final `.continue` at the end.
   match config.trigger acc (← `(tactic| done)) with
   | .accept ctx =>
-    if let some (ctxI, i) := firstInfo then
-      testTacticSeq config tacticSeq ctxI i ctx
+    if let some i := firstInfo then
+      testTacticSeq config tacticSeq i ctx
   | _ => pure ()
 
 /-- Constructor for a `Config` which breaks the pass up into multiple pieces. -/

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -65,8 +65,11 @@ def terminalReplacement (oldTacticName newTacticName : String) (oldTacticKind :
       let ((sig, _, modules), _) ← (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 _ oldHeartbeats new newHeartbeats :=
-    match new with
+  tell stx old oldHeartbeats new newHeartbeats :=
+    -- If the original tactic failed, then we do not need to check the replacement.
+    if !old.isEmpty then
+      return none
+    else match new with
     | .error _ msg =>
       if reportFailure then
         let msg :=
@@ -195,15 +198,16 @@ private abbrev mergeWithGrindAllowed : Std.HashSet Name := { `«tactic#adaptatio
   inherit_doc linter.tacticAnalysis.mergeWithGrind]
 def Mathlib.TacticAnalysis.mergeWithGrind : TacticAnalysis.Config where
   run seq := do
-    if let #[(preCtx, preI), (_postCtx, postI)] := seq[seq.size - 2:].toArray then
-      if postI.stx.getKind == ``Lean.Parser.Tactic.grind && preI.stx.getKind ∉ mergeWithGrindAllowed then
-        if let [goal] := preI.goalsBefore then
+    if let #[preI, postI] := seq[seq.size - 2:].toArray then
+      if postI.tacI.stx.getKind == ``Lean.Parser.Tactic.grind &&
+          preI.tacI.stx.getKind ∉ mergeWithGrindAllowed then
+        if let [goal] := preI.tacI.goalsBefore then
           let goals ← try
-            preCtx.runTacticCode preI goal postI.stx
+            preI.runTacticCode goal postI.tacI.stx
           catch _e =>
             pure [goal]
           if goals.isEmpty then
-            logWarningAt preI.stx m!"'{preI.stx}; grind' can be replaced with 'grind'"
+            logWarningAt preI.tacI.stx m!"'{preI.tacI.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 := {
@@ -225,28 +229,28 @@ def Mathlib.TacticAnalysis.terminalToGrind : TacticAnalysis.Config where
     -- already solved by `grind` and if so pushing that tactic onto `replaced`.
     -- By repeating this until `grind` fails for the first time, we get a terminal sequence
     -- of replaceable tactics.
-    for (ctx, i) in seq.reverse do
-      if replaced.length >= threshold - 1 && i.stx.getKind != ``Lean.Parser.Tactic.grind then
-        if let [goal] := i.goalsBefore then
+    for i in seq.reverse do
+      if replaced.length >= threshold - 1 && i.tacI.stx.getKind != ``Lean.Parser.Tactic.grind then
+        if let [goal] := i.tacI.goalsBefore then
           -- Count the heartbeats of the original tactic sequence, verifying that this indeed
           -- closes the goal like it does in userspace.
-          let suffix := ⟨i.stx⟩ :: replaced
+          let suffix := ⟨i.tacI.stx⟩ :: replaced
           let seq ← `(tactic| $suffix.toArray;*)
           let (oldGoals, heartbeats) ← withHeartbeats <|
             try
-              ctx.runTacticCode i goal seq
+              i.runTacticCode goal seq
             catch _e =>
               pure [goal]
           if !oldGoals.isEmpty then
-            logWarningAt i.stx m!"Original tactics failed to solve the goal: {seq}"
+            logWarningAt i.tacI.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 tac ← `(tactic| grind)
           let (newGoals, heartbeats) ← withHeartbeats <|
             try
-              ctx.runTacticCode i goal tac
+              i.runTacticCode goal tac
             catch _e =>
               pure [goal]
           newHeartbeats := heartbeats
@@ -256,7 +260,7 @@ def Mathlib.TacticAnalysis.terminalToGrind : TacticAnalysis.Config where
             break
         else
           break
-      replaced := ⟨i.stx⟩ :: replaced
+      replaced := ⟨i.tacI.stx⟩ :: replaced
 
     if h : replaced.length >= threshold ∧ success then
       let stx := replaced[0]
@@ -281,16 +285,16 @@ register_option linter.tacticAnalysis.tryAtEachStep.fraction : Nat := {
 def Mathlib.TacticAnalysis.tryAtEachStep (tac : Syntax → MVarId → CommandElabM (TSyntax `tactic)) : TacticAnalysis.Config where
   run seq := do
     let fraction := linter.tacticAnalysis.tryAtEachStep.fraction.get (← getOptions)
-    for (ctx, i) in seq do
-      if let [goal] := i.goalsBefore then
+    for i in seq do
+      if let [goal] := i.tacI.goalsBefore then
         if (hash goal) % fraction = 0 then
-          let tac ← tac i.stx goal
+          let tac ← tac i.tacI.stx goal
           let goalsAfter ← try
-            ctx.runTacticCode i goal tac
+            i.runTacticCode goal tac
           catch _e =>
             pure [goal]
           if goalsAfter.isEmpty then
-            logInfoAt i.stx m!"`{i.stx}` can be replaced with `{tac}`"
+            logInfoAt i.tacI.stx m!"`{i.tacI.stx}` can be replaced with `{tac}`"
 
 /-- Run `grind` at every step in proofs, reporting where it succeeds. -/
 register_option linter.tacticAnalysis.tryAtEachStepGrind : Bool := {

MathlibTest/TacticAnalysis.lean

@@ -216,3 +216,40 @@ example : P 37 := by
 end
 
 end tryAtEachStep
+
+section grindReplacement
+
+set_option linter.tacticAnalysis.regressions.omegaToCutsat true
+
+-- We should not complain about `omega` (and others) failing in a `try` context.
+example : x = y := by
+  try omega
+  rfl
+
+-- Example with more than one tactic step:
+example : x = y := by
+  try
+    symm
+    symm
+    omega
+  rfl
+
+set_option linter.unusedVariables false in
+theorem create_a_few_goals (h1 : 1 + 1 = 2) (h2 : y = z) : x = y := rfl
+
+-- We should not complain about `omega` (and others) failing in an `any_goals` context.
+example : x = y := by
+  apply create_a_few_goals
+  any_goals omega
+  rfl
+
+-- Example with more than one tactic step:
+example : x = y := by
+  apply create_a_few_goals
+  any_goals
+    symm
+    symm
+    omega
+  rfl
+
+end grindReplacement