From cf4e106304179cb299e8a8e3d91eb79ecde1241a Mon Sep 17 00:00:00 2001
From: larsk21 <57503246+larsk21@users.noreply.github.com>
Date: Sat, 21 May 2022 22:38:23 +0200
Subject: [PATCH] fix: unused variables linter review comments

- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
---
 doc/examples/test_single.sh                   |  2 +-
 src/Lean/Linter/Basic.lean                    | 51 ++++++++++---------
 src/Lean/Linter/Util.lean                     | 34 ++++++++-----
 tests/compiler/test_single_interpret.sh       |  2 +-
 tests/lean/interactive/test_single.sh         |  2 +-
 tests/lean/linterUnusedVariables.lean         | 17 +++++--
 .../linterUnusedVariables.lean.expected.out   | 44 ++++++++--------
 tests/lean/run/test_single.sh                 |  2 +-
 tests/lean/server/diags.lean                  |  2 +-
 tests/lean/server/test_single.sh              |  2 +-
 tests/lean/test_single.sh                     |  2 +-
 tests/lean/trust0/test_single.sh              |  2 +-
 tests/plugin/test_single.sh                   |  2 +-
 13 files changed, 95 insertions(+), 69 deletions(-)

diff --git a/doc/examples/test_single.sh b/doc/examples/test_single.sh
index 4138ee78a8..e341426aca 100755
--- a/doc/examples/test_single.sh
+++ b/doc/examples/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -j 0 -Dlinter.nolint=true "$f"
+exec_check lean -j 0 -Dlinter.all=false "$f"
diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index 3fa35aa197..af5d9a19d6 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -8,11 +8,13 @@ import Std.Data.HashMap
 namespace Lean.Linter
 open Lean.Server Std
 
-register_builtin_option linter.unusedVariables.nolint : Bool := {
-  defValue := false,
-  descr := "disable the 'unused variables' linter"
+register_builtin_option linter.unusedVariables : Bool := {
+  defValue := true,
+  descr := "enable the 'unused variables' linter"
 }
 
+def getLinterUnusedVariables (o : Options) : Bool := o.get linter.unusedVariables.name (getLinterAll o)
+
 def unusedVariables : Linter := fun stx => do
   let some stxRange := stx.getRange?
     | pure ()
@@ -40,33 +42,35 @@ def unusedVariables : Linter := fun stx => do
   for (id, (decl?, uses)) in vars.toList do
     let some decl := decl?
       | continue
-    let some range := decl.stx.getRange?
+    let declStx := skipDeclIdIfPresent decl.stx
+    let some range := declStx.getRange?
       | continue
     let some localDecl := decl.info.lctx.find? id
       | continue
     if !stxRange.contains range.start then
       continue
 
-    let opts := decl.ci.options
-    if linter.nolint.get opts || linter.unusedVariables.nolint.get opts then
+    if !getLinterUnusedVariables decl.ci.options then
       continue
 
-    if anyWithStack (stx := stx) (fun stx stack =>
-      stx.getRange?.isEqSome range &&
-      stx.isOfKind decl.stx.getKind && (
-        matchesUnusedPattern stx stack ||
-        isTopLevelDecl constDecls stx stack ||
-        isVariable stx stack ||
-        isInCtor stx stack ||
-        isInStructBinder stx stack ||
-        isInConstantWithoutDef stx stack ||
-        isInAxiom stx stack ||
-        isInDefWithForeignDefinition stx stack
-    )) then continue
+    let some stack := findSyntaxStack? stx declStx
+      | continue
+    let ignoredPatternFns := [
+      isTopLevelDecl constDecls,
+      matchesUnusedPattern,
+      isVariable,
+      isInCtor,
+      isInStructBinder,
+      isInConstantWithoutDef,
+      isInAxiom,
+      isInDefWithForeignDefinition,
+      isInDepArrow
+    ]
+    if ignoredPatternFns.any (· declStx stack) then
+      continue
 
     if uses.isEmpty then
-      let pos := fileMap.toPosition range.start
-      publishMessage s!"unused variable `{localDecl.userName}` at {pos.line}:{pos.column + 1}" range
+      publishMessage s!"unused variable `{localDecl.userName}`" range
 
   return ()
 where
@@ -76,14 +80,13 @@ where
     else
       stx
 
-  matchesUnusedPattern (stx : Syntax) (_ : SyntaxStack) :=
-    stx.getId.toString.startsWith "_"
   isTopLevelDecl (constDecls : HashSet String.Range) (stx : Syntax) (stack : SyntaxStack) := Id.run <| do
-    let stx := skipDeclIdIfPresent stx
     let some declRange := stx.getRange?
       | false
     constDecls.contains declRange &&
     !stackMatches stack [`Lean.Parser.Term.letIdDecl]
+  matchesUnusedPattern (stx : Syntax) (_ : SyntaxStack) :=
+    stx.getId.toString.startsWith "_"
   isVariable (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, `Lean.Parser.Command.variable]
   isInCtor (_ : Syntax) (stack : SyntaxStack) :=
@@ -118,6 +121,8 @@ where
         return attr[0].getId == `implementedBy
       else
         return false)
+  isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
+    stackMatches stack [`null, `Lean.Parser.Term.explicitBinder, `Lean.Parser.Term.depArrow]
 
 builtin_initialize addLinter unusedVariables
 
diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean
index a896bdaee7..9203e86bf0 100644
--- a/src/Lean/Linter/Util.lean
+++ b/src/Lean/Linter/Util.lean
@@ -4,15 +4,17 @@ import Lean.Server.InfoUtils
 
 namespace Lean.Linter
 
-register_builtin_option linter.nolint : Bool := {
-  defValue := false,
-  descr := "disable all linters"
+register_builtin_option linter.all : Bool := {
+  defValue := true,
+  descr := "enable all linters"
 }
 
+def getLinterAll (o : Options) : Bool := o.get linter.all.name linter.all.defValue
+
 open Lean.Elab Lean.Elab.Command
 
 def publishMessage
-  (content : String) (range : String.Range) (severity : MessageSeverity := .information) : CommandElabM Unit :=
+  (content : String) (range : String.Range) (severity : MessageSeverity := .warning) : CommandElabM Unit :=
 do
   let ctx := (← read)
   let messages := (← get).messages |>.add (mkMessageCore ctx.fileName ctx.fileMap content severity range.start range.stop)
@@ -20,15 +22,23 @@ do
 
 abbrev SyntaxStack := List (Syntax × Nat)
 
-partial def anyWithStack (pred : Syntax → SyntaxStack → Bool) (stx : Syntax) : Bool :=
-  let rec go (stack : SyntaxStack) (stx : Syntax) : Bool := Id.run <| do
-    if pred stx stack then
-      return true
+partial def findSyntaxStack? (root child : Syntax) : Option SyntaxStack := Id.run <| do
+  let some childRange := child.getRange?
+    | none
+  let rec go (stack : SyntaxStack) (stx : Syntax) : Option SyntaxStack := Id.run <| do
+    let some range := stx.getRange?
+      | none
+    if !range.contains childRange.start then
+      return none
+
+    if range == childRange && stx.getKind == child.getKind then
+      return stack
+
     for i in List.range stx.getNumArgs do
-      if go ((stx, i) :: stack) stx[i] then
-        return true
-    return false
-  go [] stx
+      if let some resultStack := go ((stx, i) :: stack) stx[i] then
+        return resultStack
+    return none
+  go [] root
 
 def stackMatches (stack : SyntaxStack) (pattern : List $ Option SyntaxNodeKind) : Bool :=
   stack.length >= pattern.length &&
diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh
index 62ea05aa60..a4e60cda7c 100755
--- a/tests/compiler/test_single_interpret.sh
+++ b/tests/compiler/test_single_interpret.sh
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
 source ../common.sh
 
-exec_check lean -Dlinter.nolint=true --run "$f"
+exec_check lean -Dlinter.all=false --run "$f"
 diff_produced
diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index aa90be29df..b0dc01580d 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -6,5 +6,5 @@ source ../../common.sh
 export ASAN_OPTIONS=detect_leaks=0
 
 # these tests don't have to succeed
-exec_capture lean -Dlinter.nolint=true --run run.lean "$f" || true
+exec_capture lean -Dlinter.all=false --run run.lean "$f" || true
 diff_produced
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index 3dec766720..35a6ee90dc 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -1,6 +1,6 @@
 import Lean.Util.Trace
 
-set_option linter.nolint false
+set_option linter.all true
 
 def explicitelyUsedVariable (x : Nat) : Nat :=
   x
@@ -62,8 +62,19 @@ def unusedVariablesPattern (_x : Nat) : Nat :=
   let _y := 5
   3
 
-set_option linter.unusedVariables.nolint true in
-def nolint (x : Nat) : Nat :=
+set_option linter.unusedVariables false in
+def nolintUnusedVariables (x : Nat) : Nat :=
+  let y := 5
+  3
+
+set_option linter.all false in
+def nolintAll (x : Nat) : Nat :=
+  let y := 5
+  3
+
+set_option linter.all false in
+set_option linter.unusedVariables true in
+def lintUnusedVariables (x : Nat) : Nat :=
   let y := 5
   3
 
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index a2965914f0..59418d213a 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -1,22 +1,22 @@
-unused variable `HQ` at 10:8
-unused variable `y` at 16:7
-unused variable `x` at 15:22
-unused variable `x` at 21:9
-unused variable `x` at 28:3
-unused variable `z` at 32:10
-unused variable `z` at 34:12
-unused variable `inst` at 38:35
-unused variable `x` at 40:20
-unused variable `α` at 74:16
-unused variable `y` at 81:9
-unused variable `β` at 84:21
-unused variable `x` at 85:8
-unused variable `s` at 95:7
-unused variable `s` at 102:14
-unused variable `y` at 119:7
-unused variable `x` at 118:16
-unused variable `x` at 122:19
-unused variable `x` at 127:17
-unused variable `y` at 131:7
-unused variable `y` at 136:7
-unused variable `y` at 141:7
+linterUnusedVariables.lean:10:7-10:9: warning: unused variable `HQ`
+linterUnusedVariables.lean:16:6-16:7: warning: unused variable `y`
+linterUnusedVariables.lean:15:21-15:22: warning: unused variable `x`
+linterUnusedVariables.lean:21:8-21:9: warning: unused variable `x`
+linterUnusedVariables.lean:28:2-28:3: warning: unused variable `x`
+linterUnusedVariables.lean:32:9-32:10: warning: unused variable `z`
+linterUnusedVariables.lean:34:11-34:12: warning: unused variable `z`
+linterUnusedVariables.lean:38:34-38:38: warning: unused variable `inst`
+linterUnusedVariables.lean:77:25-77:26: warning: unused variable `x`
+linterUnusedVariables.lean:78:6-78:7: warning: unused variable `y`
+linterUnusedVariables.lean:85:15-85:16: warning: unused variable `α`
+linterUnusedVariables.lean:92:8-92:9: warning: unused variable `y`
+linterUnusedVariables.lean:95:20-95:21: warning: unused variable `β`
+linterUnusedVariables.lean:96:7-96:8: warning: unused variable `x`
+linterUnusedVariables.lean:106:6-106:7: warning: unused variable `s`
+linterUnusedVariables.lean:113:13-113:14: warning: unused variable `s`
+linterUnusedVariables.lean:130:6-130:7: warning: unused variable `y`
+linterUnusedVariables.lean:129:15-129:16: warning: unused variable `x`
+linterUnusedVariables.lean:138:16-138:17: warning: unused variable `x`
+linterUnusedVariables.lean:142:6-142:7: warning: unused variable `y`
+linterUnusedVariables.lean:147:6-147:7: warning: unused variable `y`
+linterUnusedVariables.lean:152:6-152:7: warning: unused variable `y`
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
index f8b89b49cc..59f661aefc 100755
--- a/tests/lean/run/test_single.sh
+++ b/tests/lean/run/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 -Dlinter.nolint=true "$f"
+exec_check lean -j 0 -Dlinter.all=false "$f"
diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index e5d9677062..0f052c148b 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -2,7 +2,7 @@ import Lean.Data.Lsp
 open IO Lean Lsp
 
 def main : IO Unit := do
-  Ipc.runWith (←IO.appPath) #["--server", "-Dlinter.nolint=true"] do
+  Ipc.runWith (←IO.appPath) #["--server", "-Dlinter.all=false"] do
     let hIn ← Ipc.stdin
     hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
     hIn.flush
diff --git a/tests/lean/server/test_single.sh b/tests/lean/server/test_single.sh
index f4d0030dfb..fc64ae8f13 100755
--- a/tests/lean/server/test_single.sh
+++ b/tests/lean/server/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -j 0 -Dlinter.nolint=true --run "$f"
+exec_check lean -j 0 -Dlinter.all=false --run "$f"
diff --git a/tests/lean/test_single.sh b/tests/lean/test_single.sh
index b3abc830c2..3cbc43c4b9 100755
--- a/tests/lean/test_single.sh
+++ b/tests/lean/test_single.sh
@@ -2,5 +2,5 @@
 source ../common.sh
 
 # these tests don't have to succeed
-exec_capture lean -DprintMessageEndPos=true -Dlinter.nolint=true "$f" || true
+exec_capture lean -DprintMessageEndPos=true -Dlinter.all=false "$f" || true
 diff_produced
diff --git a/tests/lean/trust0/test_single.sh b/tests/lean/trust0/test_single.sh
index 1ca0a9d5a0..eb9d0748fb 100755
--- a/tests/lean/trust0/test_single.sh
+++ b/tests/lean/trust0/test_single.sh
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -t0 -Dlinter.nolint=true "$f"
+exec_check lean -t0 -Dlinter.all=false "$f"
diff --git a/tests/plugin/test_single.sh b/tests/plugin/test_single.sh
index ba47d460cc..8622b0297e 100755
--- a/tests/plugin/test_single.sh
+++ b/tests/plugin/test_single.sh
@@ -3,5 +3,5 @@ source ../common.sh
 
 compile_lean -shared -o "${f%.lean}.so"
 expected_ret=1
-exec_check lean -Dlinter.nolint=true --plugin="${f%.lean}.so" "$f"
+exec_check lean -Dlinter.all=false --plugin="${f%.lean}.so" "$f"
 diff_produced