Linter frontend and commands

This file defines the linter commands which spot common mistakes in the code.

• #lint: check all declarations in the current file
• #lint in Pkg: check all declarations in the package Pkg (so excluding core or other projects, and also excluding the current file)
• #lint in all: check all declarations in the environment (the current file and all imported files)

For a list of default / non-default linters, see the "Linting Commands" user command doc entry.

The command #list_linters prints a list of the names of all available linters.

You can append a * to any command (e.g. #lint* in Batteries) to omit the slow tests.

You can append a - to any command (e.g. #lint- in Batteries) to run a silent lint that suppresses the output if all checks pass. A silent lint will fail if any test fails.

You can append a + to any command (e.g. #lint+ in Batteries) to run a verbose lint that reports the result of each linter, including the successes.

You can append a sequence of linter names to any command to run extra tests, in addition to the default ones. e.g. #lint doc_blame_thm will run all default tests and doc_blame_thm.

You can append only name1 name2 ... to any command to run a subset of linters, e.g. #lint only unused_arguments in Batteries

You can add custom linters by defining a term of type Linter with the @[env_linter] attribute. A linter defined with the name Batteries.Tactic.Lint.myNewCheck can be run with #lint myNewCheck or #lint only myNewCheck. If you add the attribute @[env_linter disabled] to linter.myNewCheck it will be registered, but not run by default.

Adding the attribute @[nolint doc_blame unused_arguments] to a declaration omits it from only the specified linter checks.

Tags

sanity check, lint, cleanup, command, tactic

inductive Batteries.Tactic.Lint.LintVerbosity : Type

Verbosity for the linter output.

• low : LintVerbosity

  low: only print failing checks, print nothing on success.

• medium : LintVerbosity

  medium: only print failing checks, print confirmation on success.

• high : LintVerbosity

  high: print output of every check.

@[instance_reducible]

instance Batteries.Tactic.Lint.instInhabitedLintVerbosity : Inhabited LintVerbosity

Equations

• Batteries.Tactic.Lint.instInhabitedLintVerbosity = { default := Batteries.Tactic.Lint.instInhabitedLintVerbosity.default }

@[instance_reducible]

instance Batteries.Tactic.Lint.instDecidableEqLintVerbosity : DecidableEq LintVerbosity

Equations

• Batteries.Tactic.Lint.instDecidableEqLintVerbosity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Batteries.Tactic.Lint.instReprLintVerbosity.repr : LintVerbosity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Batteries.Tactic.Lint.instReprLintVerbosity : Repr LintVerbosity

Equations

• Batteries.Tactic.Lint.instReprLintVerbosity = { reprPrec := Batteries.Tactic.Lint.instReprLintVerbosity.repr }

def Batteries.Tactic.Lint.getChecks (slow : Bool) (runOnly runAlways : Option (List Lean.Name)) : Lean.CoreM (Array NamedLinter)

getChecks slow runOnly runAlways produces a list of linters. runOnly is an optional list of names that should resolve to declarations with type NamedLinter. If populated, only these linters are run (regardless of the default configuration). runAlways is an optional list of names that should resolve to declarations with type NamedLinter. If populated, these linters are always run (regardless of their configuration). Specifying a linter in runAlways but not runOnly is an error. Otherwise, it uses all enabled linters in the environment tagged with @[env_linter]. If slow is false, it only uses the fast default tests.

Equations

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

@[macro_inline]

def Batteries.Tactic.Lint.traceLintCore (msg : String) (inIO : Bool) : Lean.CoreM Unit

Traces via IO.println if inIO is true, and via trace[...] otherwise. It seems that trace messages in a running CoreM are not propagated through to IO in the current setup. We use IO.println directly instead of running printTraces at the end of our CoreM action so that trace messages are printed to stdout immediately, and are not lost if any part of the action hangs.

This declaration is macro_inline, so it should have the same thunky behavior as trace[...].

Equations

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

@[macro_inline]

def Batteries.Tactic.Lint.traceLint (msg : String) (inIO : Bool) (currentModule linterName : Option Lean.Name := none) : Lean.CoreM Unit

Traces via IO.println if inIO is true, and via trace[...] otherwise. Prepends currentModule and linter (if present).

This declaration is macro_inline, so it should have the same thunky behavior as trace[...].

Equations

• One or more equations did not get rendered due to their size.
• Batteries.Tactic.Lint.traceLint msg inIO (some m) linterName = Batteries.Tactic.Lint.traceLintCore (toString (toString "[" ++ toString m ++ toString "] ") ++ toString "" ++ toString msg) inIO
• Batteries.Tactic.Lint.traceLint msg inIO currentModule linterName = Batteries.Tactic.Lint.traceLintCore (toString "" ++ toString "" ++ toString msg) inIO

def Batteries.Tactic.Lint.lintBatchSize : Nat

The number of declarations that a lint worker takes at a time. A larger batch means fewer updates to the shared job counter. A smaller batch spreads the work more evenly across the workers at the end of the run. The value 64 is not tuned. One counter update costs little next to the checks on 64 declarations, and a large library still gives each worker many batches.

Equations

• Batteries.Tactic.Lint.lintBatchSize = 64

def Batteries.Tactic.Lint.mapOnWorkers {α : Type u_1} {β : Type} (jobs : Array α) (numWorkers : Nat) (f : α → Lean.CoreM β) : Lean.CoreM (Array β)

Maps f over jobs on at most numWorkers workers (at least one), and returns the results in no fixed order. Each worker takes the next job that no worker has taken, until no jobs remain. The workers use the cancellation token of the caller. An exception from f stops its worker and propagates. Changes that f makes to the Core state are discarded.

Equations

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

def Batteries.Tactic.Lint.lintDecl (linter : NamedLinter) (decl : Lean.Name) (inIO : Bool) : Lean.CoreM (Option Lean.MessageData)

Runs linter on decl with separate Core and Meta state, a distinct name generator, and its own heartbeat budget. An exception from the linter becomes a LINTER FAILED message, except for an interrupt, which propagates.

Equations

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

def Batteries.Tactic.Lint.lintCore (decls : Array Lean.Name) (linters : Array NamedLinter) (currentModule : Option Lean.Name := none) (inIO : Bool := false) (localDecls : Option (Array Lean.Name) := none) : Lean.CoreM (Array (NamedLinter × Std.HashMap Lean.Name Lean.MessageData))

Runs the linters on the declarations in parallel, and returns the failures of each linter as a map from declaration to message. A linter skips a declaration whose nolint attribute names it. LEAN_NUM_THREADS sets the number of workers (by default, the hardware concurrency). Each worker lints batches of lintBatchSize declarations.

If localDecls is given, linters with isLocal lint only those declarations (for example, the declarations of the modules a change touched), while the other linters still lint all of decls.

Equations

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

def Batteries.Tactic.Lint.sortResults {α : Type} (results : Std.HashMap Lean.Name α) : Lean.CoreM (Array (Lean.Name × α))

Sorts a map with declaration keys as names by line number.

Equations

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

def Batteries.Tactic.Lint.printWarning (declName : Lean.Name) (warning : Lean.MessageData) (useErrorFormat : Bool := false) (filePath : System.FilePath := default) : Lean.CoreM Lean.MessageData

Formats a linter warning as #check command with comment.

Equations

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

def Batteries.Tactic.Lint.printWarnings (results : Std.HashMap Lean.Name Lean.MessageData) (filePath : System.FilePath := default) (useErrorFormat : Bool := false) : Lean.CoreM Lean.MessageData

Formats a map of linter warnings using print_warning, sorted by line number.

Equations

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

def Batteries.Tactic.Lint.groupedByFilename (results : Std.HashMap Lean.Name Lean.MessageData) (useErrorFormat : Bool := false) : Lean.CoreM Lean.MessageData

Formats a map of linter warnings grouped by filename with -- filename comments. The first drop_fn_chars characters are stripped from the filename.

Equations

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

def Batteries.Tactic.Lint.formatLinterResults (results : Array (NamedLinter × Std.HashMap Lean.Name Lean.MessageData)) (decls : Array Lean.Name) (groupByFilename : Bool) (whereDesc : String) (runSlowLinters : Bool) (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) : Lean.CoreM Lean.MessageData

Formats the linter results as Lean code with comments and #check commands.

Equations

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

def Batteries.Tactic.Lint.getDeclsInCurrModule : Lean.CoreM (Array Lean.Name)

Get the list of declarations in the current module.

Equations

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

def Batteries.Tactic.Lint.getAllDecls : Lean.CoreM (Array Lean.Name)

Get the list of all declarations in the environment.

Equations

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

def Batteries.Tactic.Lint.getDeclsInPackage (pkg : Lean.Name) : Lean.CoreM (Array Lean.Name)

Get the list of all declarations in the specified package.

Equations

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

def Batteries.Tactic.Lint.inProject : Lean.ParserDescr

The in foo config argument allows running the linter on a specified project.

Equations

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

def Batteries.Tactic.Lint.«command#lint+-*Only___» : Lean.ParserDescr

The command #lint runs the linters on the current file (by default).

#lint only someLinter can be used to run only a single linter.

Equations

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

def Batteries.Tactic.Lint.«command#list_linters» : Lean.ParserDescr

The command #list_linters prints a list of all available linters.

Equations

• Batteries.Tactic.Lint.«command#list_linters» = Lean.ParserDescr.node `Batteries.Tactic.Lint.«command#list_linters» 1024 (Lean.ParserDescr.symbol "#list_linters")