diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 8ce3a949d2..4faa98979d 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -47,7 +47,9 @@ structure Context where abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε abbrev CommandElabM := CommandElabCoreM Exception abbrev CommandElab := Syntax → CommandElabM Unit -abbrev Linter := Syntax → CommandElabM Unit +structure Linter where + run : Syntax → CommandElabM Unit + name : Name := by exact decl_name% /- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the @@ -68,6 +70,7 @@ def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := /- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the environment (which only contains `import`ed objects). -/ builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[] +builtin_initialize registerTraceClass `Elab.lint def addLinter (l : Linter) : IO Unit := do let ls ← lintersRef.get @@ -195,17 +198,20 @@ instance : MonadLog CommandElabM where let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data } modify fun s => { s with messages := s.messages.add msg } -def runLinters (stx : Syntax) : CommandElabM Unit := do profileitM Exception "linting" (← getOptions) do - let linters ← lintersRef.get - unless linters.isEmpty do - for linter in linters do - let savedState ← get - try - linter stx - catch ex => - logException ex - finally - modify fun s => { savedState with messages := s.messages } +def runLinters (stx : Syntax) : CommandElabM Unit := do + profileitM Exception "linting" (← getOptions) do + withTraceNode `Elab.lint (fun _ => return m!"running linters") do + let linters ← lintersRef.get + unless linters.isEmpty do + for linter in linters do + withTraceNode `Elab.lint (fun _ => return m!"running linter: {linter.name}") do + let savedState ← get + try + linter.run stx + catch ex => + logException ex + finally + modify fun s => { savedState with messages := s.messages } protected def getCurrMacroScope : CommandElabM Nat := do pure (← read).currMacroScope protected def getMainModule : CommandElabM Name := do pure (← getEnv).mainModule diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean index cb5a4b7bc0..2548e9b23a 100644 --- a/src/Lean/Linter/Builtin.lean +++ b/src/Lean/Linter/Builtin.lean @@ -10,24 +10,25 @@ register_builtin_option linter.suspiciousUnexpanderPatterns : Bool := { def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o -def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do - unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do - return +def suspiciousUnexpanderPatterns : Linter where + run cmdStx := do + unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do + return - -- check `[app_unexpander _]` defs defined by pattern matching - let `($[$_:docComment]? @[$[$attrs:attr],*] $(_vis)? def $_ : $_ $[| $pats => $_]*) := cmdStx | return + -- check `[app_unexpander _]` defs defined by pattern matching + let `($[$_:docComment]? @[$[$attrs:attr],*] $(_vis)? def $_ : $_ $[| $pats => $_]*) := cmdStx | return - unless attrs.any (· matches `(attr| app_unexpander $_)) do - return + unless attrs.any (· matches `(attr| app_unexpander $_)) do + return - for pat in pats do - let patHead ← match pat with - | `(`($patHead:ident $_args*)) => pure patHead - | `(`($patHead:ident)) => pure patHead - | _ => continue + for pat in pats do + let patHead ← match pat with + | `(`($patHead:ident $_args*)) => pure patHead + | `(`($patHead:ident)) => pure patHead + | _ => continue - logLint linter.suspiciousUnexpanderPatterns patHead - "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name." + logLint linter.suspiciousUnexpanderPatterns patHead + "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name." builtin_initialize addLinter suspiciousUnexpanderPatterns diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index 3d8200fc47..672f896cdf 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -64,9 +64,10 @@ def addHandler (env : Environment) (declName key : Name) (h : Handler) : Environ def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getState env).2 -partial def missingDocs : Linter := fun stx => do - if let some h := (getHandlers (← getEnv)).find? stx.getKind then - h (getLinterMissingDocs (← getOptions)) stx +partial def missingDocs : Linter where + run stx := do + if let some h := (getHandlers (← getEnv)).find? stx.getKind then + h (getLinterMissingDocs (← getOptions)) stx builtin_initialize addLinter missingDocs @@ -237,10 +238,10 @@ def handleIn : Handler := fun _ stx => do if stx[0].getKind == ``«set_option» then let opts ← Elab.elabSetOption stx[0][1] stx[0][2] withScope (fun scope => { scope with opts }) do - missingDocs stx[2] + missingDocs.run stx[2] else - missingDocs stx[2] + missingDocs.run stx[2] @[builtin_missing_docs_handler «mutual»] def handleMutual : Handler := fun _ stx => do - stx[1].getArgs.forM missingDocs + stx[1].getArgs.forM missingDocs.run diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 1aaf666c60..e49c2f1bca 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -133,111 +133,112 @@ unsafe def getUnusedVariablesIgnoreFnsImpl : CommandElabM (Array IgnoreFunction) opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction) -def unusedVariables : Linter := fun cmdStx => do - unless getLinterUnusedVariables (← getOptions) do - return +def unusedVariables : Linter where + run cmdStx := do + unless getLinterUnusedVariables (← getOptions) do + return - -- NOTE: `messages` is local to the current command - if (← get).messages.hasErrors then - return + -- NOTE: `messages` is local to the current command + if (← get).messages.hasErrors then + return - let some cmdStxRange := cmdStx.getRange? - | pure () + let some cmdStxRange := cmdStx.getRange? + | pure () - let infoTrees := (← get).infoState.trees.toArray - let fileMap := (← read).fileMap + let infoTrees := (← get).infoState.trees.toArray + let fileMap := (← read).fileMap - if (← infoTrees.anyM (·.hasSorry)) then - return + if (← infoTrees.anyM (·.hasSorry)) then + return - -- collect references - let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true) + -- collect references + let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true) - let mut vars : HashMap FVarId RefInfo := .empty - let mut constDecls : HashSet String.Range := .empty + let mut vars : HashMap FVarId RefInfo := .empty + let mut constDecls : HashSet String.Range := .empty - for (ident, info) in refs.toList do - match ident with - | .fvar id => - vars := vars.insert id info - | .const _ => - if let some definition := info.definition then - if let some range := definition.stx.getRange? then - constDecls := constDecls.insert range + for (ident, info) in refs.toList do + match ident with + | .fvar id => + vars := vars.insert id info + | .const _ => + if let some definition := info.definition then + if let some range := definition.stx.getRange? then + constDecls := constDecls.insert range - -- collect uses from tactic infos - let tacticMVarAssignments : HashMap MVarId Expr := - infoTrees.foldr (init := .empty) fun tree assignments => - tree.foldInfo (init := assignments) (fun _ i assignments => match i with - | .ofTacticInfo ti => - ti.mctxAfter.eAssignment.foldl (init := assignments) fun assignments mvar expr => - if assignments.contains mvar then - assignments - else - assignments.insert mvar expr - | _ => - assignments) + -- collect uses from tactic infos + let tacticMVarAssignments : HashMap MVarId Expr := + infoTrees.foldr (init := .empty) fun tree assignments => + tree.foldInfo (init := assignments) (fun _ i assignments => match i with + | .ofTacticInfo ti => + ti.mctxAfter.eAssignment.foldl (init := assignments) fun assignments mvar expr => + if assignments.contains mvar then + assignments + else + assignments.insert mvar expr + | _ => + assignments) - let tacticFVarUses : HashSet FVarId ← - tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do - let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!) - return s + let tacticFVarUses : HashSet FVarId ← + tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do + let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!) + return s - -- collect ignore functions - let ignoreFns := (← getUnusedVariablesIgnoreFns) - |>.insertAt! 0 (isTopLevelDecl constDecls) + -- collect ignore functions + let ignoreFns := (← getUnusedVariablesIgnoreFns) + |>.insertAt! 0 (isTopLevelDecl constDecls) - -- determine unused variables - let mut unused := #[] - for (id, ⟨decl?, uses⟩) in vars.toList do - -- process declaration - let some decl := decl? - | continue - let declStx := skipDeclIdIfPresent decl.stx - let some range := declStx.getRange? - | continue - let some localDecl := decl.info.lctx.find? id - | continue - if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then - continue - - -- check if variable is used - if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then + -- determine unused variables + let mut unused := #[] + for (id, ⟨decl?, uses⟩) in vars.toList do + -- process declaration + let some decl := decl? + | continue + let declStx := skipDeclIdIfPresent decl.stx + let some range := declStx.getRange? + | continue + let some localDecl := decl.info.lctx.find? id + | continue + if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then continue - -- check linter options - let opts := decl.ci.options - if !getLinterUnusedVariables opts then - continue + -- check if variable is used + if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then + continue - -- evaluate ignore functions on original syntax - if let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range)) then - if id'.isIdent && ignoreFns.any (· declStx stack opts) then + -- check linter options + let opts := decl.ci.options + if !getLinterUnusedVariables opts then continue - else - continue - -- evaluate ignore functions on macro expansion outputs - if ← infoTrees.anyM fun tree => do - if let some macroExpansions ← collectMacroExpansions? range tree then - return macroExpansions.any fun expansion => - -- in a macro expansion, there may be multiple leafs whose (synthetic) range includes `range`, so accept strict matches only - if let some (_ :: stack) := expansion.output.findStack? (·.getRange?.any (·.includes range)) (fun stx => stx.isIdent && stx.getRange?.any (· == range)) then - ignoreFns.any (· declStx stack opts) - else - false + -- evaluate ignore functions on original syntax + if let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range)) then + if id'.isIdent && ignoreFns.any (· declStx stack opts) then + continue else - return false - then - continue + continue - -- publish warning if variable is unused and not ignored - unused := unused.push (declStx, localDecl) + -- evaluate ignore functions on macro expansion outputs + if ← infoTrees.anyM fun tree => do + if let some macroExpansions ← collectMacroExpansions? range tree then + return macroExpansions.any fun expansion => + -- in a macro expansion, there may be multiple leafs whose (synthetic) range includes `range`, so accept strict matches only + if let some (_ :: stack) := expansion.output.findStack? (·.getRange?.any (·.includes range)) (fun stx => stx.isIdent && stx.getRange?.any (· == range)) then + ignoreFns.any (· declStx stack opts) + else + false + else + return false + then + continue - for (declStx, localDecl) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do - logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`" + -- publish warning if variable is unused and not ignored + unused := unused.push (declStx, localDecl) - return () + for (declStx, localDecl) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do + logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`" + + return () where skipDeclIdIfPresent (stx : Syntax) : Syntax := if stx.isOfKind ``Lean.Parser.Command.declId then diff --git a/tests/plugin/SnakeLinter.lean b/tests/plugin/SnakeLinter.lean index b9414d95aa..93a0a77d69 100644 --- a/tests/plugin/SnakeLinter.lean +++ b/tests/plugin/SnakeLinter.lean @@ -3,15 +3,16 @@ import Lean open Lean def oh_no : Nat := 0 -def snakeLinter : Linter := fun stx => do - if stx.getKind == `Lean.Parser.Command.declaration then - let decl := stx[1] - if decl.getKind == `Lean.Parser.Command.def then - let declId := decl[1] - withRef declId do - let declName := declId[0].getId - if declName.eraseMacroScopes.toString.contains '_' then - -- TODO(Sebastian): return actual message with position from syntax tree - throwError "SNAKES!!" +def snakeLinter : Linter where + run stx := do + if stx.getKind == `Lean.Parser.Command.declaration then + let decl := stx[1] + if decl.getKind == `Lean.Parser.Command.def then + let declId := decl[1] + withRef declId do + let declName := declId[0].getId + if declName.eraseMacroScopes.toString.contains '_' then + -- TODO(Sebastian): return actual message with position from syntax tree + throwError "SNAKES!!" initialize addLinter snakeLinter