replicating lint errors

Stream: new members

[Matias Heikkilä]

So while working on a PR I got a sneaky lint error on the CI. Is there a way to replicate this locally? What failed was continuous integration / Lint mathlib (push)

[Jireh Loreaux]

You can click it to see exactly what the problem was.

[Matias Heikkilä]

Oh yea, noticed that, but just wondered what's the usual workflow like. This is just coming from a software developer background, where we usually run [something] lint locally, and the CI is basically there just as a sanity check that everybody has remembered to run lint

[Matias Heikkilä]

it seems that there is #lint_all which is (maybe?) what the CI does, but that does take quite some time

[Johan Commelin]

You can write #lint at the bottom of a file (or anywhere, really), to run the linters that are written in Lean.

[Johan Commelin]

It only lints the code above #lint. (Hence the suggestion to put it at the bottom of the file.)

[Johan Commelin]

You can also run ./scripts/lint-style.sh to run the coding-style linters, implemented in python.

[Matias Heikkilä]

Ah @Johan Commelin thanks! :laughter_tears: I noticed #lint but never realized it lints what's ABOVE

[Matias Heikkilä]

It sorta looks like #include or #pragma so I just placed it in the beginning from an old habit