Zulip Chat Archive

Stream: general

Topic: Mathlib linting


view this post on Zulip Bhavik Mehta (Jun 14 2020 at 16:36):

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?

view this post on Zulip Kevin Buzzard (Jun 14 2020 at 16:39):

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

view this post on Zulip Bhavik Mehta (Jun 14 2020 at 16:41):

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

view this post on Zulip Jalex Stark (Jun 14 2020 at 16:58):

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.

view this post on Zulip Bhavik Mehta (Jun 14 2020 at 16:59):

See also ormolu for Haskell

view this post on Zulip Bryan Gin-ge Chen (Jun 14 2020 at 17:02):

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.

view this post on Zulip Rob Lewis (Jun 14 2020 at 17:10):

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.


Last updated: May 16 2021 at 20:13 UTC