Basic linter types and attributes

This file defines the basic types and attributes used by the linting framework. A linter essentially consists of a function (declaration : Name) → MetaM (Option MessageData), this function together with some metadata is stored in the Linter structure. We define two attributes:

• @[env_linter] applies to a declaration of type Linter and adds it to the default linter set.

• @[nolint linterName] omits the tagged declaration from being checked by the linter with name linterName.

def Lean.Environment.isAutoDecl (env : Environment) (decl : Name) : Bool

Returns true if decl is an automatically generated declaration.

Also returns true if decl is an internal name or created during macro expansion.

@[inline]

def Batteries.Tactic.Lint.isAutoDecl {m : Type → Type} [Monad m] [Lean.MonadEnv m] (decl : Lean.Name) : m Bool

Returns true if decl is an automatically generated declaration.

Also returns true if decl is an internal name or created during macro expansion.

See Lean.Environment.isAutoDecl for an identical pure version of this function on the environment.

structure Batteries.Tactic.Lint.Linter : Type

A linting test for the #lint command.

• test : Lean.Name → Lean.MetaM (Option Lean.MessageData)

  test defines a test to perform on every declaration. It should never fail. Returning none signifies a passing test. Returning some msg reports a failing test with error msg.

• noErrorsFound : Lean.MessageData

  noErrorsFound is the message printed when all tests are negative

• errorsFound : Lean.MessageData

  errorsFound is printed when at least one test is positive

• isFast : Bool

  If isFast is false, this test will be omitted from #lint-.

structure Batteries.Tactic.Lint.NamedLinterextends Batteries.Tactic.Lint.Linter : Type

A NamedLinter is a linter associated to a particular declaration.

• test : Lean.Name → Lean.MetaM (Option Lean.MessageData)
• noErrorsFound : Lean.MessageData
• errorsFound : Lean.MessageData
• isFast : Bool
• name : Lean.Name

  The name of the named linter. This is just the declaration name without the namespace.

• declName : Lean.Name

  The linter declaration name

def Batteries.Tactic.Lint.getLinter (name declName : Lean.Name) : Lean.CoreM NamedLinter

Gets a linter by declaration name.

opaque Batteries.Tactic.Lint.batteriesLinterExt : Lean.SimplePersistentEnvExtension (Lean.Name × Bool) (Lean.NameMap (Lean.Name × Bool))

Defines the env_linter extension for adding a linter to the default set.

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

Defines the @[env_linter] attribute for adding a linter to the default set. The form @[env_linter disabled] will not add the linter to the default set, but it will be shown by #list_linters and can be selected by the #lint command.

Linters are named using their declaration names, without the namespace. These must be distinct.

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

@[nolint linterName] omits the tagged declaration from being checked by the linter with name linterName.

opaque Batteries.Tactic.Lint.nolintAttr : Lean.ParametricAttribute (Array Lean.Name)

Defines the user attribute nolint for skipping #lint

def Batteries.Tactic.Lint.shouldBeLinted {m : Type → Type} [Monad m] [Lean.MonadEnv m] (linter decl : Lean.Name) : m Bool

Returns true if decl should be checked using linter, i.e., if there is no nolint attribute.