codestyle checker?

Stream: new members

[Shanghe Chen]

Hi is it currently a codestyle checker generally or specifically for mathlib? I fount the guidelines and it's nice if there is a codestyle checker for it

[Luigi Massacci]

put #lint at the end of your file

[Shanghe Chen]

Thanks! I dont know this command before :tada:

[Michael Rothgang]

There is also a style linter (currently mostly written in Python; I'm gradually rewriting it in Lean). Running ./scripts/lint-style.sh in a terminal will run the linter on all of mathlib - so you will see if you introduced new errors. The linter implements a few checks from the style guidelines, but not all of them.

[Michael Rothgang]

There is talk about an auto-formatter for Lean: I personally believe it will happen eventually, but I won't make precise bets when exactly this will happen.

[Shanghe Chen]

Thanks! I will check these too!