Commit 2025-03-31 05:22 480c4981

feat(Tactic/Linter): a linter for directory dependencies (#23088) This is a linter that enforces that modules in certain directories should not import modules in certain others. For example, Mathlib.Algebra.Notation can only import Mathlib.Algebra files that are also in Mathlib.Algebra.Notation. The goal is that this improves modularity and organization in where we put files. At least it should force us to think a bit more about the directory structure of Mathlib. There are certainly things to improve: the prefix search can probably be optimized using a trie or similar, and the list of directories is autogenerated based on the current state. But it works, so I want to make this PR and at least start the discussion.