Zulip Chat Archive

Stream: general

Topic: run linter locally

Apurva Nakade (Apr 27 2021 at 14:07):

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 (Apr 27 2021 at 14:07):


at the end of the file

Apurva Nakade (Apr 27 2021 at 14:09):

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

Kevin Buzzard (Apr 27 2021 at 15:48):

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

Last updated: Dec 20 2023 at 11:08 UTC