unusedTacticLinter — Mathlib

Lean4
/-- The main entry point to the unused tactic linter. -/
def unusedTacticLinter : Linter where
  run :=
    withSetOptionIn fun stx => do
      unless getLinterValue linter.unusedTactic (← getLinterOptions) && (← getInfoState).enabled do
        return
      if (← get).messages.hasErrors then
        return
      if stx.isOfKind ``Mathlib.Linter.UnusedTactic.«command#show_kind_» then
        return
      let env ← getEnv
      let cats := (Parser.parserExtension.getState env).categories
      let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic |
        return
      let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv |
        return
      let trees ← getInfoTrees
      let exceptions := (← allowedRef.get).union <| allowedUnusedTacticExt.getState env
      let go : M Unit := do
        getTactics (← ignoreTacticKindsRef.get) (fun k => tactics.contains k || convs.contains k) stx
        eraseUsedTacticsList exceptions trees
      let (_, map) ← go.run { }
      let unused := map.toArray
      let key (r : String.Range) := (r.start.byteIdx, (-r.stop.byteIdx : Int))
      let mut last : String.Range := ⟨0, 0⟩
      for (r, stx) in
        let _ := @lexOrd;
        let _ := @ltOfOrd.{0};
        unused.qsort (key ·.1 < key ·.1)do
        if stx.getKind ∈ [``Batteries.Tactic.unreachable, ``Batteries.Tactic.unreachableConv] then
          continue
        if last.start ≤ r.start && r.stop ≤ last.stop then
          continue
        Linter.logLint linter.unusedTactic stx m! "'{stx}' tactic does nothing"
        last := r
Похожие утверждения