26.1. Linters and Warnings🔗

When using Lean interactively, linters are run after each command is elaborated. Linters run on a separate thread, so their warnings may arrive after the command has been processed and elaboration has proceeded to the next command.

Linter warnings have a standarized format. Each ends with instructions for disabling the linter. For example, the unused variable linter issues a warning on this code:

example :=
  let Variable name `y` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _y

Note: This linter can be disabled with `set_option linter.unusedVariables false`y := 2
  "hello"

The warning explains that linter.unusedVariables can be used to disable it:

Variable name `y` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _y

Note: This linter can be disabled with `set_option linter.unusedVariables false`

Setting the option as instructed disables the linter:

set_option linter.unusedVariables false in
example :=
  let y := 2
  "hello"

Linter options can be set in three scopes:

Command scope: Use Lean.Parser.Command.set_option : command`set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option, the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of Lean as well as user-defined extensions. The setting is active until the end of the current `section` or `namespace` or the end of the file. Auto-completion is available for `<id>` to list available options. `set_option <id> <value> in <command>` sets the option for just a single command: ``` set_option pp.all true in #check 1 + 1 ``` Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option only in a single term or tactic.set_optionlinter.x ...Lean.Parser.Command.in : commandin ... to enable or disable a linter in single command.
Section scope: The Lean.Parser.Command.set_option : command`set_option <id> <value>` sets the option `<id>` to `<value>`. Depending on the type of the option, the value can be `true`, `false`, a string, or a numeral. Options are used to configure behavior of Lean as well as user-defined extensions. The setting is active until the end of the current `section` or `namespace` or the end of the file. Auto-completion is available for `<id>` to list available options. `set_option <id> <value> in <command>` sets the option for just a single command: ``` set_option pp.all true in #check 1 + 1 ``` Similarly, `set_option <id> <value> in` can also be used inside terms and tactics to set an option only in a single term or tactic.set_option command can be used to enable or disable a linter for the remainder of the current section scope.
Package scope: Lean options, including linter options, can be set in the leanOptions field in a Lake configuration file.

Linters are organized into linter sets. All the linters in a set may be enabled together with a single option. Linters may be a part of arbitrarily many linter sets, and they are enabled if any of their sets are enabled.

Whether a given linter is enabled is determined by multiple options. Even though every option has a default value, Lean still tracks whether they've been explicitly set. If the linter's own option has been set, then that value is used. If the linter's option has not been set, but linter.all has been, then its value is used. If neither the linter's own option nor linter.all has been set, then the linter is enabled if its default value is true or if any linter set that contains it has been explicitly enabled.

There are a few consequences of this prioritization. First, linter sets can only ever enable linters, not disable them. Setting a linter set's option to false has no effect. Second, setting linter.all to either true or false takes precedence over all linter sets. linter.all also takes precedence over a linter option's default value, but not over an explicit value.

option

linter.all

Default value: false

enable all linters

option

linter.extra

Default value: false

enables the set of extra linters — linters that are turned off by default and only available via lake lint. An extra linter early-returns unless this option is true.

option

linter.coreInternal

Default value: false

enables the set of core-internal linters — linters that enforce conventions of the Lean repository itself and are not intended for use by non-core projects.