autoformatter for lean

Stream: general

[Kevin Tran]

when i use a "real" programming language, i like to use an autoformatter, because i don't like to think about formatting my code beyond "good enough". is there an autoformatter or one planned for lean?

[Johan Commelin]

Nothing for Lean 3. I guess we're all waiting for Lean 4.

[Johan Commelin]

But it might be really hard to do this for Lean 4, because its syntax is extremely flexible.

[Julian Berman]

Is there a linter? I saw mathlib used one, but it didn't seem general purpose

[Julian Berman]

(Something that doesn't fully do the autoformatting but at least complains for whatever style lean files might want to follow)

[Johan Commelin]

The linting is different from usual linters

[Johan Commelin]

The mathlib linters check that a theorem uses all its assumptions, things like that.

[Johan Commelin]

Or bad simp-lemmas, or using > instead of <

[Julian Berman]

ah

[Johan Commelin]

They aren't even technically capable of inspecting the syntax that the user wrote.

[Johan Commelin]

Because they operate on a level behind the parser.

[Julian Berman]

nod

[Matt Kempster]

Bumping this year-old thread. Are we still waiting for lean4? Is the lean4 syntax now fully specified and unchanging?

[Patrick Massot]

The Lean 4 syntax is so extensible I'm not sure this "fully specified and unchanging" question makes sense. But Lean 4 can definitely autoformat itself.

[Patrick Massot]

@Sebastian Ullrich

[Matt Kempster]

Aha, so a lean4 autoformatter would of course be a lean4 codebase. This makes sense.

Meanwhile, we are N years away from mathlib4 being the "main" mathlib. What is N? If N is large, does it justify a lean3 autoformatter in the meantime? I've noticed on many PRs that formatting causes several rounds of asynchronous communication, while also being largely automatable.

[Sebastian Ullrich]

Patrick Massot said:

The Lean 4 syntax is so extensible I'm not sure this "fully specified and unchanging" question makes sense. But Lean 4 can definitely autoformat itself.

Well enough for the goal view at least, but not for formatting source code. https://github.com/leanprover/lean4/blob/af12c91b0a50db2e474a1e9e04960966eea85499/tests/lean/Reformat.lean.expected.out shows the current state, though many edge case are not present in there.

[Patrick Massot]

Yes, my understanding is there is no hope to write a Lean 4 autoformatter in any other language. And we hope N is less than one.

[Sebastian Ullrich]

Formatting code with sensible line breaks is an art and someone would likely need to spend a month or so solely on the Lean 4 formatter to achieve remotely acceptable output

[Chris B]

One of my hopes for the Lean 4 version of the Bernardy pretty-printer is to figure out the best way to leverage it as a library for making formatters; I think it can significantly reduce the amount of work needed to get good (but still customizable) formatting. I haven't pushed the update yet, but I implemented a much more efficient handling for blocks of text to allow for incorporation of docs and comments.

If anyone's actually interested in making a full-blown formatter, get in touch and I'll work with you to figure out the best way to adapt it to work with Lean syntax trees.