Documentation

Lean.Linter.UnusedVariables

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

Enables or disables all unused variable linter warnings

Enables or disables unused variable linter warnings in function arguments

Enables or disables unused variable linter warnings in patterns

@[reducible, inline]

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
Instances For

    Interpret an IgnoreFunction from the environment.

    Instances For
      @[implemented_by Lean.Linter.mkIgnoreFnImpl]

      Interpret an IgnoreFunction from the environment.

      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.

      Instances For
        @[implemented_by Lean.Linter.UnusedVariables.insertObjImpl]

        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.

        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.
        Instances For

          Visit an Expr, collecting all fvars in it into fvarUses

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

            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.

            Information regarding an FVarId definition.

            • userName : Lake.Name

              The user-provided name of the FVarId

            • A (usually .ident) syntax for the defined variable

            • 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.

            Instances For

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

              • 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.)

              • 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.

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

              • 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.

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

              Instances For

                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.
                Instances For

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

                  Equations
                  Instances For

                    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.
                    Instances For

                      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
                      Instances For