text-based linters

Stream: mathlib4

[Jon Eugster]

Working with text-based linters, I believe that Mathlib.Tactic.Linter.TextBased is in the wrong place:

it is only used by the script lake exe lint lint-style, but with its current location, it is automatically imported by Mathlib.Tactic. Therefore, any change to the linter causes an unnecessary rebuild of almost the entire Mathlib.
(for context, these are the linters which do not need a built mathlib (and no env) as they directly look at the source files)

I guess it should (similarly to Cache, LongestPole, etc.) live somewhere outside the Mathlib library. @Damiano Testa @Michael Rothgang any opinions?

[Damiano Testa]

I would be happy to move them to at least scripts.

[Damiano Testa]

I've also somehow behaved as though they are technical debts to be converted to syntax linters... :smile:

[Michael Rothgang]

Good catch; changing a text-based linter should not cause a rebuild of most of mathlib. That said, I think there's a much simpler fix: there should be no need to import Linter.TextBased anywhere in mathlib; the import in Mathlib.Linter.TextBased can simply be removed. (I think I accidentally introduced this at some point, oops.)

[Michael Rothgang]

The import of TextBased in Mathlib/Tactic.lean is a red herring: that file is never imported in mathlib (coincidentally, a text-based linter enforces this).

[Jon Eugster]

You're ofc right, I thought I looked at the import graph and got the impression that both Mathlib.Tactic.Linter and Mathlib.Tactic where imported early, but I confused it with Mathlib.Tactic.Common.

Ill PR the fix you propse in a second

[Michael Rothgang]

I'll be busy today, so cannot approve on github (as the PR is not filed yet). But if the fix is indeed just removing the one line import, let me maintainer delegate that already - i.e. feel free to maintainer merge on my behalf.