TacticAnalysis ignores tactics in have

Stream: mathlib4

[Gavin Zhao]

I have the following pass just to see what info I have in a pass:

import Mathlib.Tactic.TacticAnalysis

register_option linter.tacticAnalysis.myAnalysis : Bool := {
  defValue := false
}

@[tacticAnalysis linter.tacticAnalysis.myAnalysis]
def myAnalysisConfig : Mathlib.TacticAnalysis.Config :=
  {
    run nodes := do
      forM nodes.zipIdx $ λ⟨node, idx⟩ =>
        Lean.logInfoAt node.tacI.stx ("At node number" ++ idx.repr)
  }

but then I notice that the simp inside the have doesn't seem to be processed by the pass:

import Above.File
import Mathlib.Logic.Function.Basic

variable {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α]
  {f : (a : α) → β a} {a : α} {b : β a}

set_option linter.tacticAnalysis.myAnalysis true in
theorem eq_update_self_iff : f = Function.update f a b ↔ f a = b :=
  by
    have h : a = a := by
      simp
    simp

only shows At node number0 at the have h and At node number1 at the simp at the end, but the simp inside the have has no logs.
image.png

A slightly more complex example,

import Above.File
import Mathlib

section all_cot_671b_results

open Topology Filter Real Complex TopologicalSpace Finset
open scoped BigOperators

set_option linter.tacticAnalysis.myAnalysis true in
theorem DEMIMathAnalysis_25 (f : ℝ → ℝ)
  (hf : ContinuousOn f (Set.Ici 0))
  (h : ∀ x ≥ 0, Tendsto (λ n => f (n * x)) atTop (𝓝 0)) :
  Tendsto f atTop (𝓝 0) := by
  have h₁ : Tendsto (λ n : ℝ => f (n * 1)) atTop (𝓝 0) := by
    have h₂ : Tendsto (λ n : ℝ => f (n * 1)) atTop (𝓝 0) := h 1 (by norm_num)
    exact h₂

  have h₂ : Tendsto f atTop (𝓝 0) := by
    have h₃ : (λ n : ℝ => f (n * 1)) = (λ n : ℝ => f n) := by
      funext n
      ring_nf
    rw [h₃] at h₁
    simpa using h₁

  exact h₂

end all_cot_671b_results

image.png

I would expect both funext n and ring_nf to get underlined, or is the current behavior intended?

[Gavin Zhao]

btw I'm not sure whether this topic should belong to #metaprogramming / tactics or #mathlib4. All previous discussions of TacticAnalysis were here so posting it in #mathlib4 for visibility. Mods feel free to move topic.

[Damiano Testa]

I think that the tacticAnalysis framework only extracts the "main" tactic block and no subblock.

[Gavin Zhao]

But doesn't this mean that it's just missing tactics to analyze?

[Gavin Zhao]

In a different codebase for which I've failed to create a MWE, TacticAnalysis is still definitely going into the have as one can see the underline at contradiction in the cases, but not the intro and cases

image.png

[Kim Morrison]

@Gavin Zhao, @Damiano Testa, @Anne Baanen, fixed in #33584.

I'd be very interested in further reports about places that TacticAnalysis fails to see into.