Commit 2024-08-27 23:34 50a89e23

View on Github →

chore(Linter/TextBased): namespace declarations (#16203) Currently, all declarations of the text-based linters live in the root namespace; this can cause conflicts (and is to be used sparingly anyway).

Estimated changes

Modified Mathlib/Tactic/Linter/TextBased.lean

deleted inductive BroadImports

deleted inductive ComparisonResult

deleted def ErrorContext.find?_comparable

deleted structure ErrorContext

deleted inductive ErrorFormat

added inductive Mathlib.Linter.TextBased.BroadImports

added inductive Mathlib.Linter.TextBased.ComparisonResult

added def Mathlib.Linter.TextBased.ErrorContext.find?_comparable

added structure Mathlib.Linter.TextBased.ErrorContext

added inductive Mathlib.Linter.TextBased.ErrorFormat

added inductive Mathlib.Linter.TextBased.OutputSetting

added def Mathlib.Linter.TextBased.StyleError.errorCode

added def Mathlib.Linter.TextBased.StyleError.errorMessage

added inductive Mathlib.Linter.TextBased.StyleError

added def Mathlib.Linter.TextBased.allLinters

added def Mathlib.Linter.TextBased.broadImportsLinter

added def Mathlib.Linter.TextBased.checkFileLength

added def Mathlib.Linter.TextBased.compare

added def Mathlib.Linter.TextBased.copyrightHeaderLinter

added def Mathlib.Linter.TextBased.formatErrors

added def Mathlib.Linter.TextBased.isCorrectAuthorsLine

added def Mathlib.Linter.TextBased.lintFile

added def Mathlib.Linter.TextBased.lintModules

added def Mathlib.Linter.TextBased.outputMessage

added def Mathlib.Linter.TextBased.parse?_errorContext

added def Mathlib.Linter.TextBased.parseStyleExceptions

deleted inductive OutputSetting

deleted def StyleError.errorCode

deleted def StyleError.errorMessage

deleted inductive StyleError

deleted def allLinters

deleted def broadImportsLinter

deleted def checkFileLength

deleted def compare

deleted def copyrightHeaderLinter

deleted def formatErrors

deleted def isCorrectAuthorsLine

deleted def lintFile

deleted def lintModules

deleted def outputMessage

deleted def parse?_errorContext

deleted def parseStyleExceptions

Modified scripts/lint-style.lean