[Merged by Bors] - feat(Tactic/Linter/DirectoryDependency): add an allow-list for directories with few imports

[grunweg]

Add an allow-list mechanism to the directoryDependency linter: modules covered by that list may only have imports listed in that list --- i.e., new top-level directory imports are forbidden by default.
To prove the implementation works, we add entries for the Lean, Util and Tactic/Linter directories in mathlib.
A future PR will convert the entries for e.g. Logic, Control or Testable to this allow-list.

This PR is a follow-up to #23088. Further refactorings (such as parsing the lists of exceptions from a JSON file)
can happen in subsequent PRs.

---

Open question: instead of manually filtering for imports of external projects, should I instead just lint only mathlib imports?

Future question: add further tests; this mechanism is somewhat undertested. I'm happy to work on this, but am not sure if this should block this PR. The lack of tests is certainly pre-existing.

[github-actions]

PR summary 05d0a12a07

Import changes exceeding 2%

%	File
+100.00%	Mathlib.Tactic.Linter.DirectoryDependency

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Linter.DirectoryDependency	1	2	+1 (+100.00%)

Import changes for all files

Files	Import difference
Mathlib.Tactic.Linter.DirectoryDependency	1

---

Declarations diff

+ Lean.Name.prefix?
+ allowedImportDirs
+ containsKey
+ getAllLeft

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

I'm a bit worried about the large amount of messages being confusing. Especially since the warning for Mathlib.Util.AssertExists subsumes the warnings for the transitive imports of that file. Do you have an idea how to deduplicate that?

[grunweg]

Good point about the large number of warnings. The linter code only sees the transitive imports in the end --- so just warning about user imports is not easy (and sometimes the "bad imports" really come in transitively). I can imagine a few ways of improving this experience:

• if syntactical imports are not allowed, error about these first
• cap the number of warnings to e.g. five and add a note "only showing the first 5 of N warnings"
• only list the full import chain for the first 5 imports, but still list the remaining modules: not sure if that's helpful.

If the issue is e.g. aesop being imported, I am not interested in seeing warnings about all 300 modules individually. For mathlib modules, one could try matching the bad imports to top-level directories from the allow-list...

So, there are a few options. What do you think, which of these are appropriate as opposed to overkill?

[Vierkantor]

I think I have a working approach: when describing the import path, we can check if one of the modules is already forbidden. If so, we can drop the message since another error will supersede it. I took the liberty of pushing that change so you can try it out, feel free to modify/revert if you have better ideas!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[grunweg]

Sorry for the delay; I have too many things at once that I want my attention. I should hopefully be able to review your commit soon. Would you like to merge master, so this can then proceed quickly after that?

[kim-em]

I'd be happy with this in as is. We can keep iterating.

bors d+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Thanks! I just checked and agree with the last commit.
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style