From 61232ed94eb1b83e84ea8bdec55a873fa4b885c4 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Wed, 29 Apr 2026 16:31:57 +0000
Subject: [PATCH 1/3] feat: upstream `unreachableTactic` linter

---
 src/Lean/Linter/Clippy.lean                   |   1 +
 src/Lean/Linter/Clippy/UnreachableTactic.lean | 129 ++++++++++++++++++
 .../tests/builtin-lint/ClippyViolations.lean  |   2 +
 tests/lake/tests/builtin-lint/test.sh         |   5 +
 4 files changed, 137 insertions(+)
 create mode 100644 src/Lean/Linter/Clippy/UnreachableTactic.lean

diff --git a/src/Lean/Linter/Clippy.lean b/src/Lean/Linter/Clippy.lean
index da6d4ff2978c..60ac59baa940 100644
--- a/src/Lean/Linter/Clippy.lean
+++ b/src/Lean/Linter/Clippy.lean
@@ -7,3 +7,4 @@ module
 
 prelude
 public import Lean.Linter.Clippy.UnnecessarySeqFocus
+public import Lean.Linter.Clippy.UnreachableTactic
diff --git a/src/Lean/Linter/Clippy/UnreachableTactic.lean b/src/Lean/Linter/Clippy/UnreachableTactic.lean
new file mode 100644
index 000000000000..6977902f3639
--- /dev/null
+++ b/src/Lean/Linter/Clippy/UnreachableTactic.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Linter.Basic
+public import Lean.Parser.Syntax
+public import Init.Try
+
+public section
+
+namespace Lean.Linter.Clippy
+open Elab Command
+
+/--
+Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.
+For example, in `example : True := by trivial <;> done`, the tactic `done` is never executed
+because `trivial` produces no subgoals; you could put `sorry` or `apply I_don't_exist`
+or anything else there and no error would result.
+
+A common source of such things is `simp <;> tac` in the case that `simp` improves and
+closes a subgoal that was previously being closed by `tac`.
+-/
+register_builtin_option linter.clippy.unreachableTactic : Bool := {
+  defValue := false
+  descr := "enable the 'unreachable tactic' linter"
+}
+namespace UnreachableTactic
+
+/-- The monad for collecting used tactic syntaxes. -/
+abbrev M := StateRefT (Std.HashMap Lean.Syntax.Range Syntax) IO
+
+/--
+A list of blacklisted syntax kinds, which are expected to have subterms that contain
+unevaluated tactics.
+-/
+initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
+  IO.mkRef <| (∅ : NameHashSet)
+    |>.insert ``Parser.Term.binderTactic
+    |>.insert ``Lean.Parser.Term.dynamicQuot
+    |>.insert ``Lean.Parser.Tactic.quotSeq
+    |>.insert ``Lean.Parser.Tactic.tacticStop_
+    |>.insert ``Lean.Parser.Command.notation
+    |>.insert ``Lean.Parser.Command.mixfix
+    |>.insert ``Lean.Parser.Command.registerTryTactic
+    |>.insert ``Lean.Parser.Tactic.discharger
+
+/-- Is this a syntax kind that contains intentionally unevaluated tactic subterms? -/
+def isIgnoreTacticKind (ignoreTacticKinds : NameHashSet) (k : SyntaxNodeKind) : Bool :=
+  match k with
+  | .str _ "quot" => true
+  | _ => ignoreTacticKinds.contains k
+
+/--
+Adds a new syntax kind whose children will be ignored by the `unreachableTactic` linter.
+This should be called from an `initialize` block.
+-/
+def addIgnoreTacticKind (kind : SyntaxNodeKind) : IO Unit :=
+  ignoreTacticKindsRef.modify (·.insert kind)
+
+variable (ignoreTacticKinds : NameHashSet) (isTacKind : SyntaxNodeKind → Bool) in
+/-- Accumulates the set of tactic syntaxes that should be evaluated at least once. -/
+@[specialize] partial def getTactics (stx : Syntax) : M Unit := do
+  if let .node _ k args := stx then
+    if !isIgnoreTacticKind ignoreTacticKinds k then
+      args.forM getTactics
+    if isTacKind k then
+      if let some r := stx.getRange? true then
+        modify fun m => m.insert r stx
+
+mutual
+
+/-- Search for tactic executions in the info tree and remove executed tactic syntaxes. -/
+partial def eraseUsedTacticsList (trees : PersistentArray InfoTree) : M Unit :=
+  trees.forM eraseUsedTactics
+
+/-- Search for tactic executions in the info tree and remove executed tactic syntaxes. -/
+partial def eraseUsedTactics : InfoTree → M Unit
+  | .node i c => do
+    if let .ofTacticInfo i := i then
+      if let some r := i.stx.getRange? true then
+        modify (·.erase r)
+    eraseUsedTacticsList c
+  | .context _ t => eraseUsedTactics t
+  | .hole _ => pure ()
+
+end
+
+@[inherit_doc linter.clippy.unreachableTactic]
+def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do
+  unless getLinterValueClippy linter.clippy.unreachableTactic (← getLinterOptions)
+    && (← getInfoState).enabled do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let cats := (Parser.parserExtension.getState (← getEnv)).categories
+  -- These lookups may fail when the linter is run in a fresh, empty environment
+  let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic
+    | return
+  let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv
+    | return
+  let trees ← getInfoTrees
+  let go : M Unit := do
+    getTactics (← ignoreTacticKindsRef.get) (fun k => tactics.contains k || convs.contains k) stx
+    eraseUsedTacticsList trees
+  let (_, map) ← go.run {}
+  let unreachable := map.toArray
+  let key (r : Lean.Syntax.Range) := (r.start.byteIdx, (-r.stop.byteIdx : Int))
+  let mut last : Lean.Syntax.Range := ⟨0, 0⟩
+  for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; unreachable.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
+    logLint linter.clippy.unreachableTactic stx "this tactic is never executed"
+    last := r
+
+builtin_initialize addLinter unreachableTacticLinter
+end UnreachableTactic
+
+
+end Lean.Linter.Clippy
diff --git a/tests/lake/tests/builtin-lint/ClippyViolations.lean b/tests/lake/tests/builtin-lint/ClippyViolations.lean
index 0181c85dd5c8..0958bcce2753 100644
--- a/tests/lake/tests/builtin-lint/ClippyViolations.lean
+++ b/tests/lake/tests/builtin-lint/ClippyViolations.lean
@@ -12,3 +12,5 @@ example : True := by
 -- The component `Dup` appears consecutively in this declaration's name —
 -- the builtin clippy `dupNamespace` env linter should flag it.
 def Dup.Dup.violation : Nat := 2
+
+def unreachableTacticViolation : True := by trivial <;> done
diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh
index 275f3c6c4eea..d2a0040203c8 100755
--- a/tests/lake/tests/builtin-lint/test.sh
+++ b/tests/lake/tests/builtin-lint/test.sh
@@ -88,6 +88,8 @@ no_match_pat 'clippy text linter saw a declaration' produced.out
 no_match_pat 'tac1 <;> tac2' produced.out
 # Builtin clippy env linter `dupNamespace` is non-default, so it stays silent.
 no_match_pat 'Dup.Dup.violation' produced.out
+# Builtin clippy text linter `unreachableTactic` is non-default, so silent.
+no_match_pat 'this tactic is never executed' produced.out
 
 # --clippy should run only non-default (clippy) linters, including the clippy
 # text linter which tags its warnings with `linter.clippy`.
@@ -102,6 +104,8 @@ match_pat 'tac1 <;> tac2' produced.out
 # Builtin `dupNamespace` env linter fires under --clippy.
 match_pat 'Dup.Dup.violation' produced.out
 match_pat "namespace .*Dup.* is duplicated" produced.out
+# Builtin `unreachableTactic` clippy text linter fires under --clippy.
+match_pat 'this tactic is never executed' produced.out
 # --clippy should not run default linters
 no_match_pat 'shouldBeTheorem' produced.out
 
@@ -119,6 +123,7 @@ lake_out lint --lint-all ClippyViolations || true
 match_pat 'badNameClippy' produced.out
 match_pat 'clippy text linter saw a declaration' produced.out
 match_pat 'tac1 <;> tac2' produced.out
+match_pat 'this tactic is never executed' produced.out
 
 # --lint-only unnecessarySeqFocus runs only the clippy text linter.
 lake_out lint --lint-only unnecessarySeqFocus ClippyViolations || true

From e19ba73f0003de242dac5acbe4775f837b27536a Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Wed, 29 Apr 2026 16:34:30 +0000
Subject: [PATCH 2/3] chore: use `logLintIfClippy` instead of `logLintIf`

---
 src/Lean/Linter/Clippy/UnnecessarySeqFocus.lean | 2 +-
 src/Lean/Linter/Clippy/UnreachableTactic.lean   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Linter/Clippy/UnnecessarySeqFocus.lean b/src/Lean/Linter/Clippy/UnnecessarySeqFocus.lean
index 482e58696552..5c75ac9de064 100644
--- a/src/Lean/Linter/Clippy/UnnecessarySeqFocus.lean
+++ b/src/Lean/Linter/Clippy/UnnecessarySeqFocus.lean
@@ -182,7 +182,7 @@ def unnecessarySeqFocusLinter : Linter where run := withSetOptionIn fun stx => d
   let mut last : Lean.Syntax.Range := ⟨0, 0⟩
   for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; unused.qsort (key ·.1 < key ·.1) do
     if last.start ≤ r.start && r.stop ≤ last.stop then continue
-    Linter.logLint linter.clippy.unnecessarySeqFocus stx
+    Linter.logLintIfClippy linter.clippy.unnecessarySeqFocus stx
       "Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice"
     last := r
 
diff --git a/src/Lean/Linter/Clippy/UnreachableTactic.lean b/src/Lean/Linter/Clippy/UnreachableTactic.lean
index 6977902f3639..7fe30daa344b 100644
--- a/src/Lean/Linter/Clippy/UnreachableTactic.lean
+++ b/src/Lean/Linter/Clippy/UnreachableTactic.lean
@@ -119,7 +119,7 @@ def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do
     -- if stx.getKind ∈ [``Batteries.Tactic.unreachable, ``Batteries.Tactic.unreachableConv] then
     --   continue
     if last.start ≤ r.start && r.stop ≤ last.stop then continue
-    logLint linter.clippy.unreachableTactic stx "this tactic is never executed"
+    logLintIfClippy linter.clippy.unreachableTactic stx "this tactic is never executed"
     last := r
 
 builtin_initialize addLinter unreachableTacticLinter

From 7af038b85a82d15fc5f266f5f8dceb20aff45f6c Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Tue, 5 May 2026 16:05:47 +0000
Subject: [PATCH 3/3] chore: remove batteries special casing

---
 src/Lean/Linter/Clippy/UnreachableTactic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Lean/Linter/Clippy/UnreachableTactic.lean b/src/Lean/Linter/Clippy/UnreachableTactic.lean
index 7fe30daa344b..b2178d2a286b 100644
--- a/src/Lean/Linter/Clippy/UnreachableTactic.lean
+++ b/src/Lean/Linter/Clippy/UnreachableTactic.lean
@@ -116,8 +116,6 @@ def unreachableTacticLinter : Linter where run := withSetOptionIn fun stx => do
   let key (r : Lean.Syntax.Range) := (r.start.byteIdx, (-r.stop.byteIdx : Int))
   let mut last : Lean.Syntax.Range := ⟨0, 0⟩
   for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; unreachable.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
     logLintIfClippy linter.clippy.unreachableTactic stx "this tactic is never executed"
     last := r