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.

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
• optName : Name

  The option name associated to the linter.

• declName : Name

  The linter declaration name

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

Gets an environment linter by option name.

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

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 registering an environment linter. Each environment linter needs to have a registered Boolean-value Lean.Option that will be associated with it by providing the option name in the attribute, i.e. @[builtin_env_linter linter.envLinter.myLinter].