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.

[Martin Dvořák]

Thank you so much!!!!!!!!!!!!!!!! It works almost exactly as I wanted!

[Martin Dvořák]

How can I give you credit in the best possible way? Do you want to display your original code somewhere? I will upload only the code with my modifications (not testing atomic names, not testing inductive type declarations).

[Martin Dvořák]

https://github.com/Ivan-Sergeyev/seymour/commit/4e7c6eea2835225e282e4788a7e876cd88e7725f

[Alok Singh]

Martin Dvořák said:

How can I give you credit in the best possible way?

maybe put the code on github and in the opening module comment an ascii art that looks like him (or just "thank you so much Damiano Testa" if that's freaky)

[Martin Dvořák]

The awesome linter by @Damiano Testa now lives here:
https://github.com/madvorak/leanters

I stick to Lean 4.18.0 for my dissertation; however, if anybody wants to use the linter with a newer Lean version, let me know and I'll bump it.