perf: do not lint unused variables defined in tactics by default

src/Lean/Linter/ConstructorAsVariable.lean

@@ -37,7 +37,7 @@ def constructorNameAsVariable : Linter where
     let warnings : IO.Ref (Std.HashMap String.Range (Syntax × Name × Name)) ← IO.mkRef {}
 
     for tree in infoTrees do
-      tree.visitM' (preNode := fun ci info _ => do
+      tree.visitM' (postNode := fun ci info _ => do
         match info with
         | .ofTermInfo ti =>
           match ti.expr with

src/Lean/Linter/UnusedVariables.lean

@@ -77,6 +77,11 @@ register_builtin_option linter.unusedVariables.patternVars : Bool := {
   defValue := true,
   descr := "enable the 'unused variables' linter to mark unused pattern variables"
 }
+/-- Enables linting variables defined in tactic blocks, may be expensive for complex proofs -/
+register_builtin_option linter.unusedVariables.inTactics : Bool := {
+  defValue := false,
+  descr := "enable linting variables defined in tactic blocks, may be expensive for complex proofs"
+}
 
 /-- Gets the status of `linter.unusedVariables` -/
 def getLinterUnusedVariables (o : Options) : Bool :=
@@ -360,55 +365,68 @@ structure References where
 
 /-- Collect information from the `infoTrees` into `References`.
 See `References` for more information about the return value. -/
-def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
-    StateRefT References IO Unit := do
-  for tree in infoTrees do
-    tree.visitM' (preNode := fun ci info _ => do
-      match info with
-      | .ofTermInfo ti =>
-        match ti.expr with
-        | .const .. =>
-          if ti.isBinder then
-            let some range := info.range? | return
-            let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-            modify fun s => { s with constDecls := s.constDecls.insert range }
-        | .fvar id .. =>
-          let some range := info.range? | return
-          let .original .. := info.stx.getHeadInfo | return -- we are not interested in canonical syntax here
-          if ti.isBinder then
-            -- This is a local variable declaration.
-            let some ldecl := ti.lctx.find? id | return
-            -- Skip declarations which are outside the command syntax range, like `variable`s
-            -- (it would be confusing to lint these), or those which are macro-generated
-            if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return
-            let opts := ci.options
-            -- we have to check for the option again here because it can be set locally
-            if !getLinterUnusedVariables opts then return
-            let stx := skipDeclIdIfPresent info.stx
-            if let .str _ s := stx.getId then
-              -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
-              -- This is the suggested way to silence the warning
-              if s.startsWith "_" then return
-            -- Record this either as a new `fvarDefs`, or an alias of an existing one
-            modify fun s =>
-              if let some ref := s.fvarDefs[range]? then
-                { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
-              else
-                { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+partial def collectReferences (infoTrees : Array Elab.InfoTree) (cmdStxRange : String.Range) :
+    StateRefT References IO Unit := ReaderT.run (r := false) <| go infoTrees none
+where
+  go infoTrees ctx? := do
+    for tree in infoTrees do
+      tree.visitM' (ctx? := ctx?) (preNode := fun ci info children => do
+        let ignoredInTactic ← read
+        match info with
+        | .ofTermInfo ti =>
+          match ti.expr with
+          | .const .. =>
+            if ti.isBinder then
+              let some range := info.range? | return true
+              let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+              modify fun s => { s with constDecls := s.constDecls.insert range }
+          | .fvar id .. =>
+            let some range := info.range? | return true
+            let .original .. := info.stx.getHeadInfo | return true -- we are not interested in canonical syntax here
+            if ti.isBinder then
+              -- This is a local variable declaration.
+              if ignoredInTactic then return true
+              let some ldecl := ti.lctx.find? id | return true
+              -- Skip declarations which are outside the command syntax range, like `variable`s
+              -- (it would be confusing to lint these), or those which are macro-generated
+              if !cmdStxRange.contains range.start || ldecl.userName.hasMacroScopes then return true
+              let opts := ci.options
+              -- we have to check for the option again here because it can be set locally
+              if !getLinterUnusedVariables opts then return true
+              let stx := skipDeclIdIfPresent info.stx
+              if let .str _ s := stx.getId then
+                -- If the variable name is `_foo` then it is intentionally (possibly) unused, so skip.
+                -- This is the suggested way to silence the warning
+                if s.startsWith "_" then return true
+              -- Record this either as a new `fvarDefs`, or an alias of an existing one
+              modify fun s =>
+                if let some ref := s.fvarDefs[range]? then
+                  { s with fvarDefs := s.fvarDefs.insert range { ref with aliases := ref.aliases.push id } }
+                else
+                  { s with fvarDefs := s.fvarDefs.insert range { userName := ldecl.userName, stx, opts, aliases := #[id] } }
+            else
+              -- Found a direct use, keep track of it
+              modify fun s => { s with fvarUses := s.fvarUses.insert id }
+          | _ => pure ()
+        | .ofTacticInfo ti =>
+          if ignoredInTactic then return true
+          -- Keep track of the `MetavarContext` after a tactic for later
+          modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
+          -- For `set_option linter.unusedVariables.inTactics true in` to work, it is important to
+          -- query the local options here
+          if linter.unusedVariables.inTactics.get ci.options then
+            return true
           else
-            -- Found a direct use, keep track of it
-            modify fun s => { s with fvarUses := s.fvarUses.insert id }
+            withReader (fun _ => true) do
+              go children.toArray ci
+            return false
+        | .ofFVarAliasInfo i =>
+          -- record any aliases we find
+          modify fun s =>
+            let id := followAliases s.fvarAliases i.baseId
+            { s with fvarAliases := s.fvarAliases.insert i.id id }
         | _ => pure ()
-      | .ofTacticInfo ti =>
-        -- Keep track of the `MetavarContext` after a tactic for later
-        modify fun s => { s with assignments := s.assignments.push ti.mctxAfter.eAssignment }
-      | .ofFVarAliasInfo i =>
-        -- record any aliases we find
-        modify fun s =>
-          let id := followAliases s.fvarAliases i.baseId
-          { s with fvarAliases := s.fvarAliases.insert i.id id }
-      | _ => pure ())
-where
+        return true)
   /-- Since declarations attach the declaration info to the `declId`,
   we skip that to get to the `.ident` if possible. -/
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
@@ -497,7 +515,7 @@ def unusedVariables : Linter where
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
         -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
-        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
+        fvarUsesRef.modify fun fvarUses => fvarUses.toArray.map getCanonVar |> .insertMany {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now

src/Lean/Server/InfoUtils.lean

@@ -40,27 +40,34 @@ structure InfoWithCtx where
   info : Elab.Info
   children : PersistentArray InfoTree
 
-/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones)
-and accumulating results on the way back up. -/
+/--
+Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
+accumulating results on the way back up. If `preNode` returns `false`, the children of the current
+node are skipped and `postNode` is invoked with an empty list of results.
+-/
 partial def InfoTree.visitM [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α)
-    : InfoTree → m (Option α) :=
-  go none
+    (ctx? : Option ContextInfo := none) : InfoTree → m (Option α) :=
+  go ctx?
 where go
   | ctx?, context ctx t => go (ctx.mergeIntoOuter? ctx?) t
   | some ctx, node i cs => do
-    preNode ctx i cs
-    let as ← cs.toList.mapM (go <| i.updateContext? ctx)
-    postNode ctx i cs as
+    let visitChildren ← preNode ctx i cs
+    if !visitChildren then
+      postNode ctx i cs []
+    else
+      let as ← cs.toList.mapM (go <| i.updateContext? ctx)
+      postNode ctx i cs as
   | none, node .. => panic! "unexpected context-free info tree node"
   | _, hole .. => pure none
 
 /-- `InfoTree.visitM` specialized to `Unit` return type -/
 def InfoTree.visitM' [Monad m]
-    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
+    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Bool := fun _ _ _ => pure true)
     (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
-    (t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard
+    (ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
+  t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
 
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/

tests/lean/linterUnusedVariables.lean

@@ -129,6 +129,7 @@ def nolintPatternVars (x : Option (Option Nat)) : Nat :=
   | some (some y) => (fun z => 1) 2
   | _ => 0
 
+set_option linter.unusedVariables.inTactics true in
 set_option linter.unusedVariables.patternVars false in
 theorem nolintPatternVarsInduction (n : Nat) : True := by
   induction n with
@@ -188,9 +189,12 @@ opaque foo (x : Nat) : Nat
 opaque foo' (x : Nat) : Nat :=
   let y := 5
   3
+
+section
 variable (bar)
 variable (bar' : (x : Nat) → Nat)
 variable {α β} [inst : ToString α]
+end
 
 @[specialize]
 def specializeDef (x : Nat) : Nat := 3
@@ -210,6 +214,8 @@ opaque externConst (x : Nat) : Nat :=
   let y := 3
   5
 
+section
+variable {α : Type}
 
 macro "useArg " name:declId arg:ident : command => `(def $name ($arg : α) : α := $arg)
 useArg usedMacroVariable a
@@ -222,6 +228,7 @@ doNotUseArg unusedMacroVariable b
 def ignoreDoNotUse : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``doNotUse]
 
 doNotUseArg unusedMacroVariable2 b
+end
 
 macro "ignoreArg " id:declId sig:declSig : command => `(opaque $id $sig)
 ignoreArg ignoredMacroVariable (x : UInt32) : UInt32
@@ -267,3 +274,6 @@ inaccessible annotation.
 -/
 example : (x = y) → y = x
   | .refl _ => .refl _
+
+theorem lexicalTacticUse (p : α → Prop) (ha : p a) (hb : p b) :  p b := by
+  simp [ha, hb]

tests/lean/linterUnusedVariables.lean.expected.out

@@ -30,51 +30,41 @@ linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h`
+linterUnusedVariables.lean:138:9-138:10: warning: unused variable `h`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y`
+linterUnusedVariables.lean:152:8-152:9: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β`
+linterUnusedVariables.lean:155:20-155:21: warning: unused variable `β`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x`
+linterUnusedVariables.lean:156:7-156:8: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s`
+linterUnusedVariables.lean:166:6-166:7: warning: unused variable `s`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y`
+linterUnusedVariables.lean:190:6-190:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x`
+linterUnusedVariables.lean:200:19-200:20: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
+linterUnusedVariables.lean:204:6-204:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
+linterUnusedVariables.lean:209:6-209:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
+linterUnusedVariables.lean:214:6-214:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b`
+linterUnusedVariables.lean:225:32-225:33: warning: unused variable `b`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:236:27-236:28: error: don't know how to synthesize placeholder
+linterUnusedVariables.lean:243:27-243:28: error: don't know how to synthesize placeholder
 context:
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:237:0-237:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:238:0-238:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:239:29-241:7: error: unexpected token 'theorem'; expected '{' or tactic
-linterUnusedVariables.lean:239:27-239:29: error: unsolved goals
-bar : ?m
-bar' : Nat → Nat
-α : Type ?u
-β : ?m
-inst : ToString α
+linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:246:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
+linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord`
+linterUnusedVariables.lean:256:9-256:12: warning: unused variable `ord`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord`
+linterUnusedVariables.lean:257:15-257:18: warning: unused variable `ord`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h`
+linterUnusedVariables.lean:258:9-258:10: warning: unused variable `h`
 note: this linter can be disabled with `set_option linter.unusedVariables false`