Auto run Linter from #lint

Stream: general

[Moritz R]

Batteries has a cool impossibleInstance linter that runs when writing #lint.
Can i enable it to run automatically on my file, like the long lines linter does (that i think might be from mathlib?)

[Anne Baanen]

This kind of linter ("environment linter") doesn't run as you type: they are designed to run on a whole library at once to ensure overall consistency. In this case, however, looks like impossibleInstance only needs to see the current declaration, so we can turn it into a different kind of linter ("syntax linter") that is able to run as you type. That would take some amount of work though.

For now, if you don't want to write #lint on the bottom of your files, you can also run the command lake exe runLinter. In GitHub CI, the lean-action can automatically call the command for you.