Linter against automatic opening of a namespace

Stream: general

[Martin Dvořák]

For a long time, I have been yearning for a linter against taking advantage of the automatic opening of a namespace for the declaration's name prefix. It is what I describe in lean#6855 but as a linter instead of a language feature. The way I imagine the linter to work is that the program would try to change the first letter of the declaration name (or, for example, it could prepend 'A' no matter if the name starts with 'A' already) and check that the entire declaration still compiles (including the proof if there is one) after changing the name (but not save the changed name in the file).

How hard do you think it would be to write such a linter? Can you estimate, for example, how much money I should offer to a person implementing the linter? It would come out of my pocket, not from any research budget. I have no experience with linters, so I'd like to ask here first.

[Damiano Testa]

This linter is very easy to write. In fact, this issue is one of the main reasons why it is hard to write certain linter, since simply modifying the name of a declaration and elaborating it has a lot of options of failing. The one you mention being one of them.

[Damiano Testa]

Besides being easy to write, I think that it would be also very hard to merge in mathlib...

[Martin Dvořák]

I don't intend to get it into Mathlib.