Basic environment linter types and attributes

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

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

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

def Lean.Linter.EnvLinter.isAutoDecl (decl : Name) : 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 Lean.Linter.EnvLinter.EnvLinter : Type

An environment linting test for the lake builtin-lint command.

• test : Name → MetaM (Option 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 : MessageData

  noErrorsFound is the message printed when all tests are negative

• errorsFound : MessageData

  errorsFound is printed when at least one test is positive

• isDefault : Bool

  If isDefault is false, this linter is only run when --extra is passed.

structure Lean.Linter.EnvLinter.NamedEnvLinterextends Lean.Linter.EnvLinter.EnvLinter : Type

A NamedEnvLinter is an environment linter associated to a particular declaration.

• test : Name → MetaM (Option MessageData)
• noErrorsFound : MessageData
• errorsFound : MessageData
• isDefault : Bool
• name : Name

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

• declName : Name

  The linter declaration name

def Lean.Linter.EnvLinter.getEnvLinter (name declName : Name) : CoreM NamedEnvLinter

Gets an environment linter by declaration name.

Equations

• Lean.Linter.EnvLinter.getEnvLinter name declName = Lean.Linter.EnvLinter.getEnvLinter.unsafe_impl_2✝ name declName

opaque Lean.Linter.EnvLinter.envLinterExt : SimplePersistentEnvExtension (Name × Bool) (NameMap (Name × Bool))

Defines the envLinterExt extension for adding an environment linter to the default set.

def Lean.Linter.EnvLinter.builtin_env_linter : ParserDescr

Defines the @[builtin_env_linter] attribute for adding a linter to the default set. The form @[builtin_env_linter extra] will not add the linter to the default set, but it can be selected by lake builtin-lint --extra.

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.