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 (after stripping private mangling; i.e., private names are not necessarily considered autogenerated).

Equations

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

@[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.

Equations

• Batteries.Tactic.Lint.isAutoDecl decl = do let __do_lift ← Lean.getEnv pure (__do_lift.isAutoDecl decl)

@[inline]

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

Returns true if decl is a private or automatically generated declaration.

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

Equations

• env.isPrivateOrAutoDecl decl = (Lean.isPrivateName decl || env.isAutoDecl decl)

@[inline]

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

Returns true if decl is a private or automatically generated declaration.

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

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

Equations

• Batteries.Tactic.Lint.isPrivateOrAutoDecl decl = do let __do_lift ← Lean.getEnv pure (__do_lift.isPrivateOrAutoDecl decl)

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-.

• isLocal : Bool

  Whether this linter's verdict on a declaration depends only on the declaration's own module, so that linting just the declarations of changed modules (runLinter --only-modules) cannot miss a report. A linter is not local if anything another module can add or remove changes its verdict: simpNF and simpComm consult the simp set, the instance linters and docBlame consult instance attributes (deleting a downstream attribute [instance] can create a docBlame report).

  Locality says nothing about changes to the linter itself or to external suppression lists such as nolints.json: a caller restricting local linters must lint everything when those change. Default false, so that a new linter lints everywhere until someone checks it is local.

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
• isLocal : 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.

Equations

• Batteries.Tactic.Lint.getLinter name declName = Batteries.Tactic.Lint.getLinter.unsafe_impl_2✝ name declName

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.

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