opinionated formatter à la black

Stream: Is there code for X?

[Xavier Martinet]

Hi,

Is there a way to standardize code formatting? In Python I am very fond of black (https://github.com/psf/black), this is extremely useful when there are several people working on the same codebase and you want to avoid pointless diffs because of different formatting habits.
Is there something similar in Lean?

[Eric Wieser]

I think the closest thing we have right now is a CI script for mathlib that checks the indentation style roughtly matches #style, but it's fairly heuristic as lean is impossible for anything but lean itself to parse.

[Yaël Dillies]

Johan wrote a style linter for braces recently.

[Patrick Massot]

The more important answer is that all this will exist in Lean 4, but there is no point trying in Lean 3.