feat: enforce that Algebra.Notation imports no other files inside algebra

[grunweg]

by extending the broadImports check of the header linter accordingly.
This enforces some of the rules set in #22640.

---

[github-actions]

PR summary a01470fa27

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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).

[grunweg]

About the review requests:

• @YaelDillies Can you check I got the logic exactly right, please?
• @adomani Can you double-check the implementation?
  Both are hopefully quick, and not urgent from my side.

[adomani]

Does this prevent also transitive importing? That is, a direct import will get flagged, but what if there is no direct import, but there is a transitive one?

I wonder whether this should be regulated by an extension of the assert_not_imported machinery that is directory-aware.

[leanprover-community-mathlib4-bot]

!bench

[YaelDillies]

Thanks

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[leanprover-bot]

Here are the benchmark results for commit f982972.
There were no significant changes against commit 2186c5f.

[github-actions]

File	Instructions	%
build	+1.504⬝10⁹	(+0.00%)
CI run

[grunweg]

Does this prevent also transitive importing? That is, a direct import will get flagged, but what if there is not direct import, but there is a transitive one?

I wonder whether this should be regulated by an extension of the assert_not_inported machinery that is directory-aware.

Very good question! This only lints direct imports. I agree transitive imports should also be caught.

If you have a pointer to how to extend assert_not_imported, I'm happy to try. (This is not my highest priority though, so might take some time.) In the mean-time, we could land this with an issue about the generalisation - or wait for the better fix instead. Either way is fine with me.

[adomani]

What if, instead of checking that there is an import ... syntax, you actually inspect docs#Lean.Environment.allImportedModuleNames, filter out the ones ones that should not be there and assert that the rest is empty?

This check should only run on the appropriate set of modules, so that, on most files, just the prefix check on the name will run.

[grunweg]

That's a great idea, thanks!