fix(TacticAnalysis): remove syntax range check (#28950)

In #28802 we discovered the tactic analysis framework does not fire on declarations using `where` clauses. The reason is that `def foo where ...` gets turned into `def foo := { ... }`, and the `{ ... }` syntax is assigned a range outside of the `where ...` syntax; this causes the syntax range check to omit the whole declaration body. Moreover, [Verso involves pieces of syntax without any range at all](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20Verso.E2.80.93Mathlib.20conflict/with/543352839). So the range of a piece of syntax is essentially meaningless and we should not check it at all.

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

Author: Vierkantor

Mathlib/Tactic/TacticAnalysis.lean

@@ -145,19 +145,14 @@ would result in three sequences:
 Similarly, a declaration with multiple `by` blocks results in each of the blocks getting its
 own sequence.
 -/
-def findTacticSeqs (stx : Syntax) (tree : InfoTree) :
+def findTacticSeqs (tree : InfoTree) :
     CommandElabM (Array (Array (ContextInfo × TacticInfo))) := do
-  let some enclosingRange := stx.getRange? |
-    throw (Exception.error stx m!"operating on syntax without range")
   -- Turn the CommandElabM into a surrounding context for traversing the tree.
   let ctx ← read
   let state ← get
   let ctxInfo := { env := state.env, fileMap := ctx.fileMap, ngen := state.ngen }
   let out ← tree.visitM (m := CommandElabM) (ctx? := some ctxInfo)
-    (fun _ i _ => do
-      if let some range := i.stx.getRange? then
-        pure <| enclosingRange.start <= range.start && range.stop <= enclosingRange.stop
-      else pure false)
+    (fun _ _ _ => pure true) -- Assumption: a tactic can occur as a child of any piece of syntax.
     (fun ctx i _c cs => do
       let relevantChildren := (cs.filterMap id).toArray
       let childTactics := relevantChildren.filterMap Prod.fst
@@ -190,16 +185,15 @@ def findTacticSeqs (stx : Syntax) (tree : InfoTree) :
 
 /-- Run the tactic analysis passes from `configs` on the tactic sequences in `stx`,
 using `trees` to get the infotrees. -/
-def runPasses (configs : Array Pass) (stx : Syntax)
-    (trees : PersistentArray InfoTree) : CommandElabM Unit := do
+def runPasses (configs : Array Pass) (trees : PersistentArray InfoTree) : CommandElabM Unit := do
   let opts ← getLinterOptions
   let enabledConfigs := configs.filter fun config =>
     -- This can be `none` in the file where the option is declared.
     if let some opt := config.opt then getLinterValue opt opts else false
   if enabledConfigs.isEmpty then
     return
   for i in trees do
-    for seq in (← findTacticSeqs stx i) do
+    for seq in (← findTacticSeqs i) do
       for config in enabledConfigs do
         config.run seq
 
@@ -217,7 +211,7 @@ def tacticAnalysis : Linter where run := withSetOptionIn fun stx => do
   let env ← getEnv
   let configs := (tacticAnalysisExt.getState env).2
   let trees ← getInfoTrees
-  runPasses configs stx trees
+  runPasses configs trees
 
 initialize addLinter tacticAnalysis
 

MathlibTest/TacticAnalysis.lean

@@ -38,6 +38,19 @@ example : x = z := by
   rw [xy]
   rw [yz]
 
+-- Definitions using `where` clauses did not get picked up by the framework,
+-- since apparently their syntax bounds do not match the original.
+structure Fact (p : Prop) : Prop where
+  out : p
+/--
+warning: Try this: rw [xy, yz]
+-/
+#guard_msgs in
+example : Fact (x = z) where
+  out := by
+    rw [xy]
+    rw [yz]
+
 end rwMerge
 
 section mergeWithGrind