linter suggestions

Stream: mathlib4

[Floris van Doorn]

Linter suggestion:
If declaration foo exists in the root namespace, then flag any declaration Bar.foo that is not protected.

Two complications:

• Some namespaces are exported to the root namespace (e.g. MulAction.mul_smul) and should also trigger the linter (e.g. flag Matrix.mul_smul).
• Some namespaces are never opened, and requiring declarations in those namespaces to be protected might be superfluous/annoying. If we want to add a check for this, maybe the condition could be something like "has 10 declarations in the namespace that are not automatically generated or generated by a structure/inductive command".

[Asei Inoue]

nice!

[Yaël Dillies]

I already suggested this idea to @Alex J. Best back in Lean 3, and we got an implementation. The issue is that it caught way too many true positives

[Yaël Dillies]

The majority of those true positives came from lemmas of the form some_property.some_other_property. In Lean 4, this became SomeProperty.someOtherProperty, so I expect a bunch of these true positives simply vanished

[Damiano Testa]

Jireh asked about this and I wrote a script to find these and it indeed flagged about 4k exceptions.

[Damiano Testa]

This is an approximate answer: there are 4815 exceptions.