The Lean Language Reference

26.2. Linting Workflows🔗

In addition to providing feedback on individual commands while a module is under development, linters can be applied at the package level. When modules are elaborated, their linter warnings are stored in their .olean files for replay. In addition to collecting these interactive results, linting a package provides the opportunity to run environment linters, which are linters that report potential problems in a the environment that results from importing a collection of modules, rather than in source files themselves.

26.2.1. Kinds of Linters🔗

Linters run in two contexts:

Interactive linters

These linters are run in the context of the Lean elaborator and language server while checking a single Lean file. Lean invokes these linters when the corresponding options are enabled.

Environment linters

These linters are run after a collection of modules have been built, in an environment that results from importing their modules. Environment linters are only invoked by lake lint.

There are three kinds of interactive linters:

Command linters

Command linters are run once for each top-level command.

Module linters

Module linters are run at the end of the module.

Stateful linters

Stateful linters are a special kind of command linter that can modify a shared state from one command to the next. They can be used to enforce non-local invariants, such as those governing file structure, while still providing feedback before the entire file has elaborated.

26.2.2. Running lake lint🔗

Linting via lake lint can invoke either the current project's lint driver, Lake's built-in support for linting, or both. The linters described in this chapter are built-in; a lint driver is a way to run additional linting tools that do not fit this paradigm. Built-in linting occurs when builtinLint is true in the Lake configuration or when the --builtin-lint or --builtin-only command-line options are passed to lake lint.

The --linters and --lint-only options take a comma-separated list of linter option names. --linters sets the indicated linter options, while --lint-only also disables all other linters. Within this list, a - prefix disables the linter and a leading period abbreviates linter., so .XYZ is equivalent to linter.XYZ. Later entries take precedence over earlier entries. Positional module arguments restrict built-in linting to the indicated modules; otherwise, linting begins at the module roots of all default targets. The --record-exceptions flag causes 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 commands to be added to files to suppress warnings.

26.2.3. Environment Linters and the Import Hierarchy🔗

Environment linters typically consist of two modules. One module defines the linter's option, and it must be imported by every module that will be checked with the linter. Modules that don't transitively import the linter's option are not checked. This allows the modules to override the linter option's value as needed. The other module defines the linter itself; this module only needs to be imported publicly by the root module from which linting is initiated. The environment linter runs only when it is transitively imported by the root module, but it can be applied to code in modules that the linter itself imports. Only modules that share a prefix with the root module are linted.

26.2.4. Code Quality Metrics🔗

In addition to emitting warnings, linters can save code quality metrics, which are named values that are associated either with a module or with a particular declaration. The values may be either Float or mappings from String to Float, and arbitrarily many values with a given name may be associated with a module or declaration. These associations are referred to as entries.

Every linter is already implicitly a metric. The metric's name is the linter option's name, and the metric's value is the number of times that the linter's warning was issued in a given module.

Code quality metrics are emitted in JSON format and can be processed by arbitrary scripts. For example, they can be used to track the number of linter warnings in a codebase over time, or to ensure that no new lints are introduced in a change. Custom metrics can be used to track features such as the number of times each simp lemma is used, making it easier to gain insights into a codebase that are not immediately available by inspecting the code itself.

When lake lint is run with the --code-quality flag, it emits a JSON representation of the metrics entries to standard output as a sequence of JSON objects. The lint driver is skipped. Each entry is an object with three fields:

  • name contains the metric name,

  • value contains the metric value, as a single-field object whose key name determines the field's interpretation,

  • source contains the location for which the metric was saved, also as a single-field object.

Metric values contain either the key scalar with a numeric value or the key dict with an object that maps arbitrary strings to numbers. Sources are either the key module with an object that maps name to a string or the key declaration together with an object that maps module and name to strings. The JSON output may include newlines, and should be parsed with an actual JSON parser.

Metrics Entries as JSON

A scalar value attributed to a module, as produced for replayed linter warnings:

{"name": "linter.unusedVariables",
 "source": {"module": {"name": "Proj.Basic"}},
 "value": {"scalar": {"value": 2}}}

A dictionary value attributed to a declaration, as logged by a linter:

{"name": "linter.simpUsage.lemmas",
 "source": {"declaration": {"module": "Proj.Lemmas", "name": "t3"}},
 "value": {"dict": {"dictionary": {"Nat.add_zero": 1, "Nat.zero_add": 1}}}}

When lake lint is run with the --code-quality flag, it additionally runs the code quality checks specified in the Lake configuration's checks field and on the command line via the --checks option. Both the configuration field and the command-line option point at modules; all registered checks in all specified modules are run. These checks are Lean functions that can add additional metrics that require more than a single command or module's state. Checks can replace ad hoc data collection mechanisms for CI and reporting with a single consistent mechanism.

Existing Warnings as Metrics

Without any further configuration, running lake lint with the --code-quality flag on a project returns a metric for each linter that tracks the number of warnings it issues in each module. This module contains two unused variable warnings:

module public def first (x 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 : Nat) : Nat := x public def second (Variable name `x` 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] _x Note: This linter can be disabled with `set_option linter.unusedVariables false`x y : Nat) : Nat := y module public import Code.Basic

Linting the package shows these messages:

$ lake lint --builtin-only
-- Text linter diagnostics in Code.Basic:
⟨project⟩/Code/Basic.lean:3:20: warning: 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`
⟨project⟩/Code/Basic.lean:5:19: warning: Variable name `x` 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] _x

Note: This linter can be disabled with `set_option linter.unusedVariables false`
-- No environment linters were run for Code.

The module Code.Basic itself is annotated with two instances of linter.unusedVariables:

$ lake lint --code-quality
{"value": {"scalar": {"value": 2}},
 "source": {"module": {"name": "Code.Basic"}},
 "name": "linter.unusedVariables"}