This runs, and respects the content of scripts/style-extensions.txt.

I propose that actually fixing style exceptions, and removing the style tests which are not relevant for mathlib4 (e.g. I think the curly brace linter), happens in a subsequent PR.

Obviously this should eventually be rewritten in Lean, but we can use the python script for now.

Before merging, we should remove the curly braces linter though because it has lots of false positives.

I've removed the curly brace linter, the indentation linter and the unfreeze_local_instance linter, as they are not fit for purpose for Lean4. I've also added a TODO about re-implementing in Lean4!

Great, all exceptions look legit now!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build