Rewriting Python style linters in Lean

Stream: PR reviews

[Michael Rothgang]

#13339 is one of the first steps towards rewriting all style linters in Python, blocking further progress. Can I interest somebody in reviewing it? It's almost all code motion (from a file in scripts to a new file in Mathlib/Utils), plus one easy refactoring.
CC @Damiano Testa who originally wrote the code

[Kim Morrison]

Looks good. Perhaps we can add a note in the lakefile warning about the hardcoding?

[Michael Rothgang]

Done. While at this, I realised one possible defect in the code: getLeanLibs on mathlib also yields the the lean_lib docs; should this be excluded as well?

[Matthew Ballard]

http://speed.lean-fro.org/mathlib4/run-detail/c08c756c-9478-422c-8729-73459c2ca228

[Michael Rothgang]

Oh, that seems unexpected. This PR was purely moving code...
Can you help me interpret these numbers - what does "linting" mean? Is this simply measuring "there's a new file in mathlib" (and the time was spent just on the script before) - I guess not, but I have very little idea what this means. Help welcome.

[Matthew Ballard]

This seems to not be a hiccup, instructions for linting jumped 14.2% and the linting wall clock jumped 17.3% (~90 seconds) and the instructions haven't come down.

I am bit stumped by this atm. Perhaps I am being dense.

[Matthew Ballard]

We will see if it is real soon #13779

[Matthew Ballard]

Not fake

[Matthew Ballard]

I can't believe it is taking 90s to lint that single file but what is another explanation?

[Matthew Ballard]

Can confirm that just adding Mathlib.Util.GetAllModules alone is enough for the regression.

[Mario Carneiro]

By the way, the thread title is somewhat ambiguous, I wasn't sure if it meant rewriting style linters to use Python (instead of lean / something else?)

[Michael Rothgang]

Can an admin rename this to "Rewriting Python style linters in Lean", please? I just tried, but cannot any more?

[Johan Commelin]

Done

[Matthew Ballard]

It was the Lake import

[Matthew Ballard]

Do we need getLeanLibs in Mathlib proper for whatever is coming next?

[Michael Rothgang]

I just approved your PR - short answer: no, I'm not aware of any reason we do.

[Michael Rothgang]

Filed #13836 to lint on importing Lake in Mathlib, with a clear warning explaining the reason.

[Michael Rothgang]

By the way: I'd love to rewrite this all in Lean. In Python, I have to choose between adding a second error variant or trying to thread extra data through it - Lean's inductive types are just much nicer. If you'd like to see this happen, you'd love to hear your opinion here.

[Michael Rothgang]

Status update: this is bottle-necked on a review of #13620, for providing the equivalent infrastructure in Lean. Subsequent linters can be reviewed in parallel.

[Michael Rothgang]

Michael Rothgang said:

Status update: this is bottle-necked on a review of #13620, for providing the equivalent infrastructure in Lean. Subsequent linters can be reviewed in parallel.

Thanks for the feedback! I responded.

[Kim Morrison]

Okay, I'm happy with just an explanation in the comments of the difficulty with error handling there.

[Michael Rothgang]

Thanks for the review! The next step could be to land #14012 - making lake exe lint_style produce human-readable output by default. (This also paves the way towards granular updates of file length exceptions, which @Patrick Massot (and others before) asked for the other day.)

[Michael Rothgang]

I just realised that #13620 breaks update-style-exceptions.py on master: the style exception entries will be in the wrong format. Sorry for this! #14012 fixes this as well; I had not realised this changes was already required...

[Michael Rothgang]

Less urgent: #13240 rewrites the copyright header check in Lean; I just rebased this on master.

[Michael Rothgang]

Thanks for the reviews! #14058 rewrites the "adaptation note" linter in Lean; #14059 (depending on that, but is reviewable already) does the "broad imports" (e.g. Mathlib.Tactic) one.

[Michael Rothgang]

#14093 rewrite the line length check in Lean (and fixes some small oversights from the "broad imports" linter, which were inconsequential).

[Michael Rothgang]

#14676 contains some easy refactoring of lint_style, split out for ease of reviewing

[Michael Rothgang]

#14697, building on this, rewrites update-style-exceptions in Lean.
In particular, if you encounter e.g. a "file to large error", you can just run lake exe lint_style --update and it will update the style exceptions accordingly. It does a minimal update: obsolete entries are removed, but where possible, existing entries are kept.

[Michael Rothgang]

Michael Rothgang said:

#14697, building on this, rewrites update-style-exceptions in Lean.
In particular, if you encounter e.g. a "file to large error", you can just run lake exe lint_style --update and it will update the style exceptions accordingly. It does a minimal update: obsolete entries are removed, but where possible, existing entries are kept.

The blocking PR has landed and I have rebased and fixed up this PR: it's now ready for review.

[Michael Rothgang]

#14757 is ready for review: minor style tweaks and renaming the executable to lint-style. Should be an easy diff.

[Michael Rothgang]

#15438 is a one-line fix for an error message, and should be very easy to review

[Michael Rothgang]

#15051 removes lint-style.sh. The executable bit check is moved to the build.yml files, and the calling of lint-style.py is moved to the existing print-style-errors.sh script.
(That script can be removed once all Python style linters have been rewritten in Lean, which will hopefully happen soon.)

[Michael Rothgang]

#16332 ports the linter for windows line endings to Lean
It also lays the groundwork for a fair chunk of the remaining linters, by porting the functionality of auto-fixing linters. Review appreciated (best reviewed as a whole).

[Michael Rothgang]

Building on that, #16334 rewrites the trailing whitespace check in Lean

[Johan Commelin]

cc @Damiano Testa @Jon Eugster

[Michael Rothgang]

Responded to Damiano's comment on the trailing whitespace linter.

[Kim Morrison]

@Michael Rothgang :writing: on #16332.

[Michael Rothgang]

Periodic reminder that #16334 and #16532 are awaiting review. Each rewrites a text-based style linter from Python in Lean.
The former PR has been up for review for over two months now, with no activity at all in the past 6 weeks; it's a +-20 lines PR. (The latter PR depends on the former, and is comparatively simple.)

[Michael Rothgang]

CC @Kim Morrison on the above

[Kim Morrison]

#16334

[Kim Morrison]

:peace_sign: #16532. I'm slightly surprised that we're linting for this, but given it's just a change in implementation, not behaviour, I guess I can't complain. :-)

[Kevin Buzzard]

Kim is also testing emojibot here :-)

[Michael Rothgang]

#22727 rewrites three more Python style linters in Lean

[Michael Rothgang]

It depends on two rounds of fixes, namely #22726 and #22728.

[Michael Rothgang]

#22728 has run into a style bikeshed: I will start a zulip thread about this, but possibly not very soon

[Michael Rothgang]

#22727 is ready for review again: all dependencies have been merged. (I can split out the ~30 lines of style fixes if preferred; as they don't seem controversial to me, I don't have to.)