Unused variable Linter

This file implements the unused variable linter, which runs automatically on all commands and reports any local variables that are never referred to, using information from the info tree.

It is not immediately obvious but this is a surprisingly expensive check without some optimizations. The main complication is that it can be difficult to determine what constitutes a "use". For example, we would like this to be considered a use of x:

def foo (x : Nat) : Nat := by assumption

The final proof term is fun x => x so clearly x was used, but we can't make use of this because the final proof term is after we have abstracted over the original fvar for x. If we look further into the tactic state we can see the fvar show up in the instantiation to the original goal metavariable ?m : Nat := x, but it is not always the case that we can follow metavariable instantiations to determine what happened after the fact, because tactics might skip the goal metavariable and instantiate some other metavariable created prior to it instead.

Instead, we use a (much more expensive) overapproximation, which is just to look through the entire metavariable context looking for occurrences of x. We use caching to ensure that this is still linear in the size of the info tree, even though there are many metavariable contexts in all the intermediate stages of elaboration; these are highly similar and make use of PersistentHashMap so there is a lot of subterm sharing we can take advantage of.

The @[unused_variables_ignore_fn] attribute

Some occurrences of variables are deliberately unused, or at least we don't want to lint on unused variables in these positions. For example:

def foo (x : Nat) : (y : Nat) → Nat := fun _ => x
                  -- ^ don't lint this unused variable because it is public API

They are generally a syntactic criterion, so we allow adding custom IgnoreFunctions so that external syntax can also opt in to lint suppression, like so:

macro (name := foobarKind) "foobar " name:ident : command => `(def foo ($name : Nat) := 0)

foobar n -- linted because n is unused in the macro expansion

@[unused_variables_ignore_fn]
def ignoreFoobar : Lean.Linter.IgnoreFunction := fun _ stack _ => stack.matches [``foobarKind]

foobar n -- not linted

opaque Lean.Linter.linter.unusedVariables : Lean.Option Bool

Enables or disables all unused variable linter warnings

opaque Lean.Linter.linter.unusedVariables.funArgs : Lean.Option Bool

Enables or disables unused variable linter warnings in function arguments

opaque Lean.Linter.linter.unusedVariables.patternVars : Lean.Option Bool

Enables or disables unused variable linter warnings in patterns

def Lean.Linter.getLinterUnusedVariables (o : Lean.Options) : Bool

Gets the status of linter.unusedVariables

Equations

• Lean.Linter.getLinterUnusedVariables o = Lean.Linter.getLinterValue Lean.Linter.linter.unusedVariables o

def Lean.Linter.getLinterUnusedVariablesFunArgs (o : Lean.Options) : Bool

Gets the status of linter.unusedVariables.funArgs

Equations

• Lean.Linter.getLinterUnusedVariablesFunArgs o = Lean.KVMap.get o Lean.Linter.linter.unusedVariables.funArgs.name (Lean.Linter.getLinterUnusedVariables o)

def Lean.Linter.getLinterUnusedVariablesPatternVars (o : Lean.Options) : Bool

Gets the status of linter.unusedVariables.patternVars

Equations

• Lean.Linter.getLinterUnusedVariablesPatternVars o = Lean.KVMap.get o Lean.Linter.linter.unusedVariables.patternVars.name (Lean.Linter.getLinterUnusedVariables o)

@[reducible, inline]

abbrev Lean.Linter.IgnoreFunction : Type

An IgnoreFunction receives:

• a Syntax.ident for the unused variable
• a Syntax.Stack with the location of this piece of syntax in the command
• The Options set locally to this syntax

and should return true to indicate that the lint should be suppressed, or false to proceed with linting as usual (other IgnoreFunctions may still say it is ignored). A variable is only linted if it is unused and no IgnoreFunction returns true on this syntax.

Equations

• Lean.Linter.IgnoreFunction = (Lean.Syntax → Lean.Syntax.Stack → Lean.Options → Bool)

unsafe def Lean.Linter.mkIgnoreFnImpl (constName : Lake.Name) : Lean.ImportM Lean.Linter.IgnoreFunction

Interpret an IgnoreFunction from the environment.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by Lean.Linter.mkIgnoreFnImpl]

opaque Lean.Linter.mkIgnoreFn (constName : Lake.Name) : Lean.ImportM Lean.Linter.IgnoreFunction

Interpret an IgnoreFunction from the environment.

opaque Lean.Linter.builtinUnusedVariablesIgnoreFnsRef : IO.Ref (Array Lean.Linter.IgnoreFunction)

The list of builtin IgnoreFunctions.

def Lean.Linter.addBuiltinUnusedVariablesIgnoreFn (h : Lean.Linter.IgnoreFunction) : IO Unit

Adds a new builtin IgnoreFunction. This function should only be used from within the Lean package.

Equations

• Lean.Linter.addBuiltinUnusedVariablesIgnoreFn h = ST.Ref.modify Lean.Linter.builtinUnusedVariablesIgnoreFnsRef fun (x : Array Lean.Linter.IgnoreFunction) => x.push h

opaque Lean.Linter.unusedVariablesIgnoreFnsExt : Lean.PersistentEnvExtension Lake.Name (Lake.Name × Lean.Linter.IgnoreFunction) (List Lake.Name × Array Lean.Linter.IgnoreFunction)

An extension which keeps track of registered IgnoreFunctions.

def Lean.Linter.getUnusedVariablesIgnoreFns : Lean.Elab.Command.CommandElabM (Array Lean.Linter.IgnoreFunction)

Get the current list of IgnoreFunctions.

Equations

• Lean.Linter.getUnusedVariablesIgnoreFns = do let __do_lift ← Lean.getEnv pure (Lean.Linter.unusedVariablesIgnoreFnsExt.getState __do_lift).snd

unsafe def Lean.Linter.UnusedVariables.insertObjImpl {α : Type} (set : IO.Ref (Lean.HashSet USize)) (a : α) : IO Bool

Collect into a heterogeneous collection of objects with external storage. This uses pointer identity and does not store the objects, so it is important not to store the last pointer to an object in the map, or it can be freed and reused, resulting in incorrect behavior.

Returns true if the object was not already in the set.

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by Lean.Linter.UnusedVariables.insertObjImpl]

opaque Lean.Linter.UnusedVariables.insertObj {α : Type} (set : IO.Ref (Lean.HashSet USize)) (a : α) : IO Bool

Collect into a heterogeneous collection of objects with external storage. This uses pointer identity and does not store the objects, so it is important not to store the last pointer to an object in the map, or it can be freed and reused, resulting in incorrect behavior.

Returns true if the object was not already in the set.

def Lean.Linter.UnusedVariables.visitAssignments (set : IO.Ref (Lean.HashSet USize)) (fvarUses : IO.Ref (Lean.HashSet Lean.FVarId)) (assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)) : IO Unit

Collects into fvarUses all fvars occurring in the Exprs in assignments. This implementation respects subterm sharing in both the PersistentHashMap and the Expr to ensure that pointer-equal subobjects are not visited multiple times, which is important in practice because these expressions are very frequently highly shared.

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Linter.UnusedVariables.visitAssignments.visitNode (set : IO.Ref (Lean.HashSet USize)) (fvarUses : IO.Ref (Lean.HashSet Lean.FVarId)) (node : Lean.PersistentHashMap.Node Lean.MVarId Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit IO Unit

Visit a PersistentHashMap.Node, collecting all fvars in it into fvarUses

partial def Lean.Linter.UnusedVariables.visitAssignments.visitEntry (set : IO.Ref (Lean.HashSet USize)) (fvarUses : IO.Ref (Lean.HashSet Lean.FVarId)) (e : Lean.PersistentHashMap.Entry Lean.MVarId Lean.Expr (Lean.PersistentHashMap.Node Lean.MVarId Lean.Expr)) : Lean.MonadCacheT Lean.Expr Unit IO Unit

Visit a PersistentHashMap.Entry, collecting all fvars in it into fvarUses

def Lean.Linter.UnusedVariables.visitAssignments.visitExpr (set : IO.Ref (Lean.HashSet USize)) (fvarUses : IO.Ref (Lean.HashSet Lean.FVarId)) (e : Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit IO Unit

Visit an Expr, collecting all fvars in it into fvarUses

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Linter.UnusedVariables.followAliases (aliases : Lean.HashMap Lean.FVarId Lean.FVarId) (x : Lean.FVarId) : Lean.FVarId

Given aliases as a map from an alias to what it aliases, we get the original term by recursion. This has no cycle detection, so if aliases contains a loop then this function will recurse infinitely.

structure Lean.Linter.UnusedVariables.FVarDefinition : Type

Information regarding an FVarId definition.

• userName : Lake.Name

  The user-provided name of the FVarId

• stx : Lean.Syntax

  A (usually .ident) syntax for the defined variable

• opts : Lean.Options

  The options set locally to this part of the syntax (used by IgnoreFn)

• aliases : Array Lean.FVarId

  The list of all FVarIds that are considered as being defined at this position. This can have more than one element if multiple variables are declared by the same syntax, such as the h in if h : c then ... else .... We only report an unused variable at this span if all variables in aliases are unused.

structure Lean.Linter.UnusedVariables.References : Type

The main data structure used to collect information from the info tree regarding unused variables.

• constDecls : Lean.HashSet String.Range

  The set of all (ranges corresponding to) global definitions that are made in the syntax. For example in mutual def foo := ... def bar := ... where baz := ... end this would be the spans for foo, bar, and baz. Global definitions are always treated as used. (It would be nice to be able to detect unused global definitions but this requires more information than the linter framework can provide.)

• fvarDefs : Lean.HashMap String.Range Lean.Linter.UnusedVariables.FVarDefinition

  The collection of all local declarations, organized by the span of the declaration. We collapse all declarations declared at the same position into a single record using FVarDefinition.aliases.

• fvarUses : Lean.HashSet Lean.FVarId

  The set of FVarIds that are used directly. These may or may not be aliases.

• fvarAliases : Lean.HashMap Lean.FVarId Lean.FVarId

  A mapping from alias to original FVarId. We don't guarantee that the value is not itself an alias, but we use followAliases when adding new elements to try to avoid long chains.

• assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)

  Collection of all MetavarContexts following the execution of a tactic. We trawl these if needed to find additional fvarUses.

def Lean.Linter.UnusedVariables.collectReferences (infoTrees : Array Lean.Elab.InfoTree) (cmdStxRange : String.Range) : StateRefT' IO.RealWorld Lean.Linter.UnusedVariables.References IO Unit

Collect information from the infoTrees into References. See References for more information about the return value.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Linter.UnusedVariables.collectReferences.skipDeclIdIfPresent (stx : Lean.Syntax) : Lean.Syntax

Since declarations attach the declaration info to the declId, we skip that to get to the .ident if possible.

Equations

• Lean.Linter.UnusedVariables.collectReferences.skipDeclIdIfPresent stx = if stx.isOfKind `Lean.Parser.Command.declId = true then stx[0] else stx

def Lean.Linter.UnusedVariables.unusedVariables : Lean.Linter

Reports unused variable warnings on each command. Use linter.unusedVariables to disable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.MessageData.isUnusedVariableWarning (msg : Lean.MessageData) : Bool

Returns true if this is a message produced by the unused variable linter. This is used to give these messages an additional "faded" style in the editor.

Equations

• msg.isUnusedVariableWarning = Lean.MessageData.hasTag (fun (x : Lake.Name) => x == Lean.Linter.linter.unusedVariables.name) msg