[Merged by Bors] - move: new Mathlib.Tactic.Linter dir

[adomani]

Create a new Mathlib/Tactic/Linter dir and move there the linters. Currently the new dir contains only one file, but there are more linters in PRs.

---

This was brought up by @thorimur in the context of #11019. The suggestion there was to add a Mathlib.Command.Linters dir, but maybe the extra Command layer can be skipped -- at least for now.

---

[eric-wieser]

Linter might be better than Linters, to match how we have Tactic not Tactics.

[adomani]

Eric, thanks! I made the change Linters → Linter.

[thorimur]

I think we should put this in a section under ProofWidgets just to keep this file organized (since it's no longer in alphabetical order), so that it looks something roughly like

...
-- Hopefully `lake` will be able to handle tests later.
import ProofWidgets

-- Import Mathlib-specific linters.
import Mathlib.Linter.Lint

-- Now import all tactics defined in Mathlib that do not require theory files.
import Mathlib.Mathport.Rename
...

likely also with a change to the module doc

...
We include some commented out imports here, with an explanation of their theory requirements,
to save some time for anyone wondering why they are not here.

We also import theory-free linters, commands, and utilities which are useful to have low in the 
import hierarchy.
-/
...

(Sorry, the fact that github doesn't let me make suggestions on non-modified code is relevant once more... 😅)

[adomani]

Thanks! If I implemented your suggestions, assuming that I understood them correctly!

[grunweg]

This also seems blocked on zulip consensus.

[grunweg]

Per zulip, it seems there is sufficient consensus to go ahead with this one (with an e.g. Mathlib/Tactic/Linter directory).
Can you fix the merge conflicts and change these? After these, this PR seems ready to go for me.

awaiting-author

[adomani]

@grunweg: I updated a little bit in auto-pilot mode. Is this what you had in mind? I wonder if, as a consequence of the Mathlib.Tactic.Linter dir, there is the need of a Linter.lean file, analogous to ``Mathlib.Tactic.lean`.

[grunweg]

@adomani Thanks; I think I meant something like this.
Your comment seems spot on; I think the current structure can be improve a bit.

• Perhaps, Mathlib/Tactic/Linter.lean can move to Mathlib/Tactic/Linter/All.lean
• the current Tactic/Linter/Lint.lean file can get a more descriptive name/be split up more descriptively. (For instance, dupNamespace feels like a style lint to me, but structureInType feels like a different kind... not sure how to name that.)

Long-term, I think separate files for style linters, text-based ones and environment linters, for example, could be a useful classification. At the moment, there a few landed linters, so splitting could also happen later imho.

[grunweg]

It could be useful to think where e.g. all your in-flight linters want to land in the end - if the structure can house them, I think it's good enough!

[adomani]

Ok, I'll leave this as is for now and we can discuss how many "generic linter import" files we have later on.

I will probably have to update shake to "ignoreAll/..." the new path also.

[grunweg]

Fine with me - re-organising linters can also happen in a future PR.
As the zulip consensus seems to be about this PR (not #12899, oops), let me go ahead and propose to
maintainer merge

[github-actions]

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

[grunweg]

Somehow, I've thought more about this --- here's a more detailed proposal how mathlib's linters could end up. (For a follow-up PR.) In the medium to long term, I see at least three useful categories of linters:

• text-based linters: they are based on reading the source code only. In practice, only style linters will have this form.
  Currently, there are none of them; most lints in lint-style.py can (and imho should) be rewritten this way: for example, checking the copyright header, authors line, line length, isolated "where" or "by"

• style linters: they are about coding style only; they do not affect code correctness (nor scalability of mathlib)
  This includes checking for broad imports (like "Mathlib.Tactic"), duplicate names, the "theorems without a docstring" or the multi-goal linters. They can be syntax-based; I suspect most of them will be (but this fact is not important).

• "global linters": they are about global coherence properties of mathlib. (I imagine most if not all of these will be environment linters.) Code violating them may compile, but this comes at a cost for building a coherent library. This includes

• the "structureInType" lint (currently in Lint.lean)

• the Finite/Fintype and DecidableEq linter (by urkud in feat: add Decidable, Fintype, Encodable linters #10235), as well as fpvandoorn's dual linter (somewhere on zulip)

• many still unported mathlib3 linters, e.g. for dangerous instances

Accordingly, I can imagine grouping Tactic/Linter as

• All.lean: referencing all lints, perhaps giving an overview of the different categories and referring to the separate files
• TextBased.lean: text-based linters (which are in practice all about style)
• Style.lean: style linters (presumably all operating on syntax)
• Global.lean: linters about global coherence properties; better name welcome

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

[eric-wieser]

Why did this come back?

[adomani]

I think that this comment made me add it. I suspect that it was there at the time that this PR was opened, then the other PR was merged, the import possibly removed, but when this PR was looked at again, no one noticed that it was still here.