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 Batteries.Tactic.Lint.isAutoDecl (decl : Lean.Name) : Lean.CoreM Bool

Returns true if decl is an automatically generated declaration.

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

Equations

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

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 Batteries.Tactic.Lint.NamedLinter

Gets a linter by declaration name.

Equations

• Batteries.Tactic.Lint.getLinter name declName = Batteries.Tactic.Lint.getLinter.unsafe_impl_1 name declName

opaque Batteries.Tactic.Lint.batteriesLinterExt : Lean.PersistentEnvExtension (Lean.Name × Bool) (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.

Equations

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

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

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

Equations

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

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.

Equations

• Batteries.Tactic.Lint.shouldBeLinted linter decl = do let __do_lift ← Lean.getEnv pure !((Batteries.Tactic.Lint.nolintAttr.getParam? __do_lift decl).getD #[]).contains linter