List of linters

Stream: lean4

[Patrick Massot]

How do I get the list of all linters? I want my teaching lib to disable all linters but I don’t know what to put in my lakefile.

[Sebastian Ullrich]

You should be able to set linter.all to false. If that doesn't work, it is a bug in that specific linter

[Damiano Testa]

If you actually want to know their names without hoping that they would trigger, this should be the list of all the linters in mathlib:

import Mathlib
open Lean Elab Command

elab "#find_linters" : command => do
  let stxLints ← Command.lintersRef.get
  let stxLints := stxLints.qsort (·.name.toString < ·.name.toString)
  logInfo <| "\n".intercalate <|
    s!"{stxLints.size} syntax linters found:" ::"":: stxLints.toList.map (·.name.toString)
  let envL := Batteries.Tactic.Lint.batteriesLinterExt.getState (← getEnv)
  let envLints := envL.fold (init := #[]) (fun a _shortName (name, _option) => a.push name)
  let envLints := envLints.qsort (·.toString < ·.toString)
  logInfo <| "\n".intercalate <|
    s!"{envLints.size} environment linters found:" ::"":: envLints.toList.map toString

#find_linters
/-
30 syntax linters found:

Batteries.Linter.UnnecessarySeqFocus.unnecessarySeqFocusLinter
Batteries.Linter.UnreachableTactic.unreachableTacticLinter
Lean.Linter.MissingDocs.missingDocs
Lean.Linter.UnusedVariables.unusedVariables
Lean.Linter.constructorNameAsVariable
Lean.Linter.omit
Lean.Linter.suspiciousUnexpanderPatterns
Mathlib.Linter.AdmitLinter.admitLinter
Mathlib.Linter.CountHeartbeats.countHeartbeatsLinter
Mathlib.Linter.DocPrime.docPrimeLinter
Mathlib.Linter.DoubleImports.upstreamableDeclLinter
Mathlib.Linter.DupNamespaceLinter.dupNamespace
Mathlib.Linter.Flexible.flexibleLinter
Mathlib.Linter.HashCommandLinter.hashCommandLinter
Mathlib.Linter.MinImports.minImportsLinter
Mathlib.Linter.PPRoundtrip.ppRoundtrip
Mathlib.Linter.Style.cdotLinter
Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter
Mathlib.Linter.Style.header.headerLinter
Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter
Mathlib.Linter.Style.longFile.longFileLinter
Mathlib.Linter.Style.longLine.longLineLinter
Mathlib.Linter.Style.missingEnd.missingEndLinter
Mathlib.Linter.Style.multiGoal.multiGoalLinter
Mathlib.Linter.Style.oldObtainLinter
Mathlib.Linter.Style.setOption.setOptionLinter
Mathlib.Linter.UnusedTactic.unusedTacticLinter
Mathlib.Linter.globalAttributeInLinter.globalAttributeIn
Mathlib.Linter.haveLet.haveLetLinter
Mathlib.Linter.refineLinter


17 environment linters found:

Batteries.Tactic.Lint.checkType
Batteries.Tactic.Lint.checkUnivs
Batteries.Tactic.Lint.defLemma
Batteries.Tactic.Lint.deprecatedNoSince
Batteries.Tactic.Lint.docBlame
Batteries.Tactic.Lint.docBlameThm
Batteries.Tactic.Lint.dupNamespace
Batteries.Tactic.Lint.explicitVarsOfIff
Batteries.Tactic.Lint.impossibleInstance
Batteries.Tactic.Lint.nonClassInstance
Batteries.Tactic.Lint.simpComm
Batteries.Tactic.Lint.simpNF
Batteries.Tactic.Lint.simpVarHead
Batteries.Tactic.Lint.structureInType
Batteries.Tactic.Lint.synTaut
Batteries.Tactic.Lint.unusedArguments
Batteries.Tactic.Lint.unusedHavesSuffices
-/