fast linting PhysLean

Stream: PhysLean

[Rein Zustand]

Currently it is based on Mathlib's Python-based linter, which I find to be too ad-hoc. But I recently tested that linting using tree-sitter is also very fast, using https://github.com/Julian/tree-sitter-lean. While the grammar is more comprehensive than the Python-based one. Any thoughts about pilot-testing this linter via GH Actions? The creator of that repo seems to be present in this Zulip organization too.

[Joseph Tooby-Smith]

I think there was an effort to port the python linters in Mathlib to Lean ones, I'm currently unsure of the status of that effort, but I think keeping things close to Mathlib would be good. But I agree that the python-based linters do feel a bit ad-hoc.

[Michael Rothgang]

Let me comment on the mathlib rewriting: I worked on this a lot in 2024, and most linters have been rewritten as syntax linters in Lean now. There are four linters remaining: the isolated by, where and "line starts with a colon" linters and the "space after <-" linter should be subsubmed by #30658. (That PR checks whitespace formatting in mathlib, and if it does not include these checks yet, it should.) There is also an in-progress linter about indentation. Once both of these land, all text-based mathlib linters can be removed, and I would prefer to remove that infrastructure.

[Michael Rothgang]

(Medium-term, an auto-formatter for Lean will make all these linters obsolete. I expect mathlib to experiment with this in the third quarter of this year.)

[Michael Rothgang]

In short: the python linters are going away in mathlib; working on them is not a good use of time. You should rather rewrite these as Lean syntax linters. @Damiano Testa and I are happy to help you with this. (We may and do have other obligations also, but I for sure will try to help. I presume the same holds for Damiano.)

[Joseph Tooby-Smith]

Thanks for the update @Michael Rothgang . What are the issues rewriting the additional linters into Lean? Is what you are suggesting the following:

We make a version of these linters in Lean for PhysLean and then once in Mathlib we remove them from PhysLean? If so, I think this would neaten things up a bit for us.

[Michael Rothgang]

Sorry for the late answer: what you're saying is not what I'm suggesting, but that's certainly an option.

[Michael Rothgang]

I hope that #30658 lands really soon; I'll be able to remove one of the Python linters immediately. The other three might require a small improvement to the whitespace linter. I'd be very happy to review a patch to that effect.