def Lean.Linter.LinterSets : Type

Linter sets are represented as a map from linter name to set name, to make it easy to look up which sets to check for enabling a linter.

Equations

• Lean.Linter.LinterSets = Lean.NameMap (Array Lean.Name)

@[implicit_reducible]

instance Lean.Linter.instEmptyCollectionLinterSets : EmptyCollection LinterSets

Equations

• Lean.Linter.instEmptyCollectionLinterSets = { emptyCollection := Lean.Linter.instEmptyCollectionLinterSets._aux_1 }

@[implicit_reducible]

instance Lean.Linter.instInhabitedLinterSets : Inhabited LinterSets

Equations

• Lean.Linter.instInhabitedLinterSets = { default := Lean.Linter.instInhabitedLinterSets._aux_1 }

def Lean.Linter.insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet) : LinterSets

Insert a set into a LinterSets map.

entry.1 is the name of the linter set, entry.2 contains the names of the set's linter options.

Equations

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

structure Lean.Linter.LinterSetsState : Type

State of linterSetsExt.

merged is the queryable union of all sources (builtins folded in at env creation, imported entries from oleans, and locally added entries). localEntries tracks entries added in the current module so they can be exported into the olean.

• merged : LinterSets
• localEntries : Array (Name × NameSet)

@[implicit_reducible]

instance Lean.Linter.instInhabitedLinterSetsState : Inhabited LinterSetsState

Equations

• Lean.Linter.instInhabitedLinterSetsState = { default := Lean.Linter.instInhabitedLinterSetsState.default }

opaque Lean.Linter.builtinLinterSetsRef : IO.Ref (Array (Name × NameSet))

Builtin linter sets registered from builtin_initialize blocks in core code.

Entries here are folded into every LinterSetsState produced by linterSetsExt, so they participate in getLinterValue like any user-declared set.

def Lean.Linter.addBuiltinLinterSet (setName : Name) (linterNames : NameSet) : IO Unit

Register a builtin linter set entry. Only valid during initialization; use register_builtin_linter_set rather than calling this directly.

Equations

• Lean.Linter.addBuiltinLinterSet setName linterNames = ST.Ref.modify Lean.Linter.builtinLinterSetsRef fun (x : Array (Lean.Name × Lean.NameSet)) => x.push (setName, linterNames)

opaque Lean.Linter.linterSetsExt : PersistentEnvExtension (Name × NameSet) (Name × NameSet) LinterSetsState

structure Lean.Linter.LinterOptions : Type

The LinterOptions structure is used to determine whether given linters are enabled.

This structure contains all the data required to do so, the Options set on the command line or by the set_option command, and the LinterSets that have been declared.

A single structure holding this data is useful since we want getLinterValue to be a pure function: determining the LinterSets would otherwise require a MonadEnv instance.

• toOptions : Options
• linterSets : LinterSets

def Lean.Linter.LinterOptions.get {α : Type} [KVMap.Value α] (o : LinterOptions) (k : Name) (defVal : α) : α

Equations

• o.get = o.toOptions.get

def Lean.Linter.LinterOptions.get? {α : Type} [KVMap.Value α] (o : LinterOptions) (k : Name) : Option α

Equations

• o.get? = o.toOptions.get?

def Lean.Options.toLinterOptions {m : Type → Type} [Monad m] [MonadEnv m] (o : Options) : m Linter.LinterOptions

Equations

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

def Lean.Linter.LinterOptions.getSet {α : Type} (o : LinterOptions) (opt : Lean.Option α) : Array Name

Return the set of linter sets that this option is contained in.

Equations

• o.getSet opt = Std.TreeMap.getD o.linterSets opt.name #[]

def Lean.Linter.getLinterOptions {m : Type → Type} [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions

Equations

• Lean.Linter.getLinterOptions = do let __do_lift ← Lean.getOptions __do_lift.toLinterOptions

opaque Lean.Linter.linter.all : Lean.Option Bool

opaque Lean.Linter.linter.extra : Lean.Option Bool

opaque Lean.Linter.envLinterOptionsRef : IO.Ref (Array (Lean.Option Bool))

Global registry of options associated with environment linters. These are precisely options, whose value will be snapshotted during addDecl.

def Lean.Linter.addEnvLinterOption (opt : Lean.Option Bool) : IO Unit

Equations

• Lean.Linter.addEnvLinterOption opt = ST.Ref.modify Lean.Linter.envLinterOptionsRef fun (x : Array (Lean.Option Bool)) => x.push opt

def Lean.Linter.getLinterAll (o : LinterOptions) (defValue : Bool := linter.all.defValue) : Bool

Equations

• Lean.Linter.getLinterAll o defValue = o.get Lean.Linter.linter.all.name defValue

def Lean.Linter.getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool

Equations

• Lean.Linter.getLinterValue opt o = o.get opt.name (Lean.Linter.getLinterAll o (((o.getSet opt).any fun (x : Lean.Name) => o.get? x == some true) || opt.defValue))

def Lean.Linter.isLinterEnabledByOptions (name : Name) (o : LinterOptions) : Bool

Equations

• Lean.Linter.isLinterEnabledByOptions name o = o.get name (Lean.Linter.getLinterAll o ((Std.TreeMap.getD o.linterSets name #[]).any fun (x : Lean.Name) => o.get? x == some true))

def Lean.Linter.linterMessageTag : Name

Tag attached by logLint to every linter warning so consumers (e.g. Lean.Linter.recordLints) can distinguish linter-produced messages from other tagged messages such as named errors or unknown-identifier messages.

Equations

• Lean.Linter.linterMessageTag = `Lean.Linter._linter

def Lean.Linter.logLint {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit

Equations

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

def Lean.MessageData.isLinterMessage (msg : MessageData) : Bool

Returns true if msg was produced by Lean.Linter.logLint (and therefore by a linter).

Equations

• msg.isLinterMessage = Lean.MessageData.hasTag (fun (x : Lean.Name) => x == Lean.Linter.linterMessageTag) msg

def Lean.Linter.logLintIf {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadEnv m] (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit

If linterOption is enabled, print a linter warning message at the position determined by stx.

Whether a linter option is enabled or not is determined by the following sequence:

1. If it is set, then the value determines whether or not it is enabled.
2. Otherwise, if linter.all is set, then its value determines whether or not the option is enabled.
3. Otherwise, if any of the linter sets containing the option is enabled, it is enabled. (Only enabled linter sets are considered: explicitly disabling a linter set will revert the linters it contains to their default behavior.)
4. Otherwise, the default value determines whether or not it is enabled.

Equations

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

@[reducible, inline]

abbrev Lean.Linter.EnvLinterSnapshot : Type

Equations

• Lean.Linter.EnvLinterSnapshot = Lean.NameMap Bool

opaque Lean.Linter.envLinterSnapshotExt : MapDeclarationExtension EnvLinterSnapshot

The envLinterSnapshotExt extension saves the state of all (Boolean-valued) Lean.Options associated with environment linters.

def Lean.Linter.getEnvLinterSnapshotEntry? (env : Environment) (declName optName : Name) : Option Bool

Equations

• Lean.Linter.getEnvLinterSnapshotEntry? env declName optName = do let x ← Lean.Linter.envLinterSnapshotExt.find? env declName Lean.NameMap.find? x optName