max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: unused variables linter review comments

Browse source 
- 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`
This commit is contained in:
larsk21 2022-05-21 22:38:23 +02:00 • committed by Sebastian Ullrich
parent b708eaec2c
commit cf4e106304
13 changed files with 95 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/examples/test_single.sh
View file

@ -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"

51
src/Lean/Linter/Basic.lean
View file

@ -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

34
src/Lean/Linter/Util.lean
View file

@ -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 &&

2
tests/compiler/test_single_interpret.sh
View file

@ -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

2
tests/lean/interactive/test_single.sh
View file

@ -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

17
tests/lean/linterUnusedVariables.lean
View file

@ -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

44
tests/lean/linterUnusedVariables.lean.expected.out
View file

@ -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`

2
tests/lean/run/test_single.sh
View file

@ -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"

2
tests/lean/server/diags.lean
View file

@ -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

2
tests/lean/server/test_single.sh
View file

@ -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"

2
tests/lean/test_single.sh
View file

@ -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

2
tests/lean/trust0/test_single.sh
View file

@ -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"

2
tests/plugin/test_single.sh
View file

@ -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