Commit 2025-12-05 11:03 d8b31873

View on Github →

chore(Tactic/Linters): remove public section (#31803) Mostly as a learning exercise for me to understand the module system better.

Estimated changes

Modified Mathlib/Tactic/Linter/CommandRanges.lean

Modified Mathlib/Tactic/Linter/CommandStart.lean

deleted def Mathlib.Linter.mkWindow

Modified Mathlib/Tactic/Linter/DeprecatedModule.lean

Modified Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean

modified def Mathlib.Linter.DirectoryDependency.NamePrefixRel

deleted def Mathlib.Linter.directoryDependencyCheck

deleted def findImports

Modified Mathlib/Tactic/Linter/DocPrime.lean

Modified Mathlib/Tactic/Linter/DocString.lean

deleted def Mathlib.Linter.getDeclModifiers

Modified Mathlib/Tactic/Linter/FindDeprecations.lean

Modified Mathlib/Tactic/Linter/FlexibleLinter.lean

deleted def Mathlib.Linter.Flexible.toStained

Modified Mathlib/Tactic/Linter/GlobalAttributeIn.lean

Modified Mathlib/Tactic/Linter/HashCommandLinter.lean

Modified Mathlib/Tactic/Linter/HaveLetLinter.lean

Modified Mathlib/Tactic/Linter/Header.lean

deleted def Mathlib.Linter.copyrightHeaderChecks

deleted def Mathlib.Linter.getImportIds

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Batteries.Tactic.Lint.deprecatedNoSince

deleted def Batteries.Tactic.Lint.structureInType

Modified Mathlib/Tactic/Linter/MinImports.lean

Modified Mathlib/Tactic/Linter/Multigoal.lean

Modified Mathlib/Tactic/Linter/OldObtain.lean

Modified Mathlib/Tactic/Linter/PPRoundtrip.lean

Modified Mathlib/Tactic/Linter/Style.lean

deleted def Mathlib.Linter.Style.openClassical.extractOpenNames

deleted def Mathlib.Linter.Style.setOption.isSetOption

deleted def Mathlib.Linter.isCDot?

Modified Mathlib/Tactic/Linter/TextBased.lean

deleted inductive Mathlib.Linter.TextBased.ErrorFormat

deleted def Mathlib.Linter.TextBased.modulesOSForbidden

Modified Mathlib/Tactic/Linter/UnusedTactic.lean

Modified Mathlib/Tactic/Linter/UnusedTacticExtension.lean

Modified Mathlib/Tactic/Linter/UpstreamableDecl.lean

deleted def Lean.Name.isLocal

Modified MathlibTest/CommandStart.lean

Modified MathlibTest/FlexibleLinter.lean

Modified MathlibTest/ForbiddenModuleNames.lean

deleted def testModulesOSForbidden

Modified MathlibTest/ModuleCasing.lean

deleted def testModulesNotUpperCamelCase