Style linter for broad imports

Stream: mathlib4

[Michael Rothgang]

I'd like to rewrite the style linter for "import Mathlib.Tactic" (currently in Python) in Lean. I would appreciate opinions on a design decision I have. I could

• (A) write this as a text-based linter (basically, just translating the Python to Lean): this is fast and probably accurate enough
• (B) write a syntax linter, acting on import statements.

(B) might be slower, as it presumably needs to do more work - I haven't benchmarked to know if this is relevant at all. On the upside, this would yield precise error messages, directly on the import. Any opinions?

[Yaël Dillies]

B. should be pretty easy since lake exe mk_all is now a thing

[Michael Rothgang]

I know about mk_all... I don't see how this is relevant to my actual question, though. Perhaps, let me rephrase my question: as a user/as a maintainer, which type of linter would you prefer? I'm reasonably sure I can make both of them work.

[Matthew Ballard]

This desire isn’t limited to mathlib — see also https://github.com/leanprover/lean4/pull/3374#issuecomment-1952796088