Commit 2025-05-28 07:47 97bc5f6d

View on Github →

feat(Tactic/Linter/DirectoryDependency): add an allow-list for directories with few imports (#24109) Add an allow-list mechanism to the directoryDependency linter: modules covered by that list may only have imports listed in that list

Estimated changes

Modified Mathlib/Tactic/Linter/DirectoryDependency.lean

added def Lean.Name.prefix?

added def Mathlib.Linter.DirectoryDependency.NamePrefixRel.containsKey

added def Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft

added def Mathlib.Linter.DirectoryDependency.allowedImportDirs

modified def Mathlib.Linter.directoryDependencyCheck

added def findImports

Modified Mathlib/Tactic/Linter/Header.lean

Created MathlibTest/DirectoryDependencyLinter/Test.lean

Modified MathlibTest/Header.lean

Modified scripts/lint-style.lean

deleted def findImports