local linting in porting wiki?

Stream: mathlib4

[Siddhartha Gadgil]

Since CI takes a long time, I generally do the following before pushing once things look fine to quickly fix errors:

scripts/lint-style.sh
lake build
build/bin/runLinter

For me at least this is much faster that waiting for CI errors. Should this be suggested on the porting wiki?

[Kevin Buzzard]

I compile and lint the file I'm working on with #lint at the end of the file, but this is less robust than the suggestion above because e.g. a new simp lemma added in one file can make a simp linter complain in another file. It does have a high success rate though.

[Siddhartha Gadgil]

I also prefer not having to make and undo changes.