run linter locally

Stream: general

[Apurva Nakade]

Is there a way to run the Lean linter locally on just one file? Like a plugin of some kind for emacs or VScode?

[Sebastien Gouezel]

#lint

at the end of the file

[Apurva Nakade]

Oh wow! Thanks!! I had no idea it was this simple.

[Kevin Buzzard]

You can even choose which linters to run :-) In the lean-liquid repo we have a lot of #lint- only unused_arguments def_lemma doc_blame at the end of files