Mathlib linting

Stream: general

[Bhavik Mehta]

Is it possible to make a linter or code formatter which enforces (some of) mathlib's style, for instance adding braces so that there's only one goal at a time in a completed proof?

[Kevin Buzzard]

I could add it to nng and force mathematicians to code properly :-)

[Bhavik Mehta]

Actually what I want is kind of the opposite of that - when I'm writing lean hastily I somehow avoid all indentation and braces, so it'd be great if there was some magical button I could press which auto-formats the code

[Jalex Stark]

Such things exist in other domains, see e.g. black, an auto-formatter for python. I don't know how hard they are to write.

[Bhavik Mehta]

See also ormolu for Haskell

[Bryan Gin-ge Chen]

I remember some discussions about this (but not where they took place, sadly). My takeaway was that this would become much easier in Lean 4.

[Rob Lewis]

It's very hard to write something that's aware of both Lean 3 semantics (e.g. number of goals at a given line) and input syntax. I think the closest things that exist right now are format_lean (or am I mixing names here?) that query a Lean server for information at each line. It would take a lot of work to turn this into what you're after, but I think it's the only approach, Lean 3 metaprograms can't really understand input syntax. As Bryan says, I understand the Lean 4 picture will be different.