Check Lint without making a commit

Stream: new members

[Josha Dekker]

I've recently made a PR to Mathlib, but find that the 'Lint style' check tends to find several mistakes in my formatting. Is there a way to automatically this check prior to committing, so I don't have a whole list of commits of the type "style : fixed a small lint mistake"?

[Pedro Sánchez Terraf]

You can put #lint at the end of the file, that'll catch several errors

[Pedro Sánchez Terraf]

But I'm not certain it is complete. Perhaps there are some arguments you can pass to it.

[Yaël Dillies]

#lint explicitly does not check for style

[Josha Dekker]

#lint did find an unnecessary "have" that I could get rid of, so that is nice as well! Is there a similar command that does check for style?

[Yaël Dillies]

You can Ctrl + F the regex .{101} for long lines. There will be similar regex for other lints, but there's currently no script that does them all.

[Josha Dekker]

Okay, thanks!

[Josha Dekker]

Is there some other way to commit -> revise -> remove the old commit, so that they don't stack up so quickly?

[Yaël Dillies]

You can always "rebase". But I wouldn't worry about it. All commits on your PR will get squashed by bors when merged to master.

[Josha Dekker]

Okay, great! Thanks!

[Alex J. Best]

You can run the style linters by running the script scripts/lint-style.sh. For an added bonus you can run scripts/lint-style.sh --fix which will automatically fix some issues but not all