inductive Lean.Linter.EnvLinter.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.

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instInhabitedLintVerbosity : Inhabited LintVerbosity

Equations

• Lean.Linter.EnvLinter.instInhabitedLintVerbosity = { default := Lean.Linter.EnvLinter.instInhabitedLintVerbosity.default }

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instDecidableEqLintVerbosity : DecidableEq LintVerbosity

Equations

• Lean.Linter.EnvLinter.instDecidableEqLintVerbosity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Linter.EnvLinter.instReprLintVerbosity.repr : LintVerbosity → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instReprLintVerbosity : Repr LintVerbosity

Equations

• Lean.Linter.EnvLinter.instReprLintVerbosity = { reprPrec := Lean.Linter.EnvLinter.instReprLintVerbosity.repr }

inductive Lean.Linter.EnvLinter.LintScope : Type

Which set of linters to run.

• default : LintScope

  Run only default linters.

• extra : LintScope

  Run default linters together with the non-default (extra) linters.

• all : LintScope

  Run all linters (default + extra).

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instInhabitedLintScope : Inhabited LintScope

Equations

• Lean.Linter.EnvLinter.instInhabitedLintScope = { default := Lean.Linter.EnvLinter.instInhabitedLintScope.default }

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instDecidableEqLintScope : DecidableEq LintScope

Equations

• Lean.Linter.EnvLinter.instDecidableEqLintScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lean.Linter.EnvLinter.instReprLintScope : Repr LintScope

Equations

• Lean.Linter.EnvLinter.instReprLintScope = { reprPrec := Lean.Linter.EnvLinter.instReprLintScope.repr }

def Lean.Linter.EnvLinter.instReprLintScope.repr : LintScope → Nat → Format

Equations

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

def Lean.Linter.EnvLinter.getChecks (scope : LintScope := LintScope.default) (runOnly : Option (List Name) := none) : CoreM (Array NamedEnvLinter)

getChecks produces a list of linters to run.

If runOnly is populated, only those named linters are run (regardless of scope). Otherwise, linter selection depends on scope:

• default: only linters with isDefault = true
• extra: linters with isDefault = true together with linters with isDefault = false
• all: all linters

Equations

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

def Lean.Linter.EnvLinter.lintCore (decls : Array Name) (linters : Array NamedEnvLinter) : CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData))

Runs all the specified linters on all the specified declarations in parallel, producing a list of results.

Equations

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

def Lean.Linter.EnvLinter.sortResults {α : Type} (results : Std.HashMap Name α) : CoreM (Array (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 Lean.Linter.EnvLinter.printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false) (filePath : System.FilePath := default) : CoreM MessageData

Formats a linter warning as #check command with comment.

Equations

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

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

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

Equations

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

def Lean.Linter.EnvLinter.groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) : CoreM MessageData

Formats a map of linter warnings grouped by filename with -- filename comments.

Equations

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

def Lean.Linter.EnvLinter.formatLinterResults (results : Array (NamedEnvLinter × Std.HashMap Name MessageData)) (decls : Array Name) (groupByFilename : Bool) (whereDesc : String) (scope : LintScope := LintScope.default) (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) : CoreM 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 Lean.Linter.EnvLinter.getDeclsInCurrModule : CoreM (Array Name)

Get the list of declarations in the current module.

Equations

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

def Lean.Linter.EnvLinter.getAllDecls : CoreM (Array Name)

Get the list of all declarations in the environment.

Equations

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

def Lean.Linter.EnvLinter.getDeclsInPackage (pkg : Name) : CoreM (Array Name)

Get the list of all declarations in the specified package.

Equations

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