lean4
lean4 copied to clipboard
leanprover
Make the pretty printer usable for code formatting
The formatter in the pretty printer already produces pretty good output for goals and also makes a reasonable attempt at preserving comments and command-level layout: https://github.com/leanprover/lean4/blob/master/tests/lean/Reformat.lean.expected.out. But it is not yet at a point where we would reformat our code with it despite the advantages of doing so:
- consistent style between different collaborators
- no more formatting discussions in PRs
- refactorings would not have to worry about preserving/producing reasonable formatting (we should definitely preserve comments though...)
I fear I could only close it in good conscience if we used it to reformat our own codebase :) .
From my point of view there are still several challenges ahead. The applications I have in mind are mostly mathport / code action related, so this list might a bit biased.
Formatting rules for special-case formatting
The ppLine/etc. helpers are okay for the odd minor formatting tweak, but they can't do any complicated operations. (And many syntax definitions are already more than 50% pp* combinators, which is not so great for readability.)
A complicated (yet common and important) syntax is the structure instance syntax. This is used for different applications, with different formatting requirements.
{}(empty collection) should be formatted without a space.{ x := 1, y := 2 }should be formatted on a single line.{ x := 1 y := 2 }should get newlines and be ungrouped (i.e., the first{should be "hanging"):
let s := {
x := 1
y := 2
}
Particularly for 1 it would be nice if you could just add a "formatting rule" that says "format {} as "{}"".
See also (). The inline/multi-line distinction comes up in many other syntaxes as well, e.g. by simp vs by rw [foo] simp. (Unfortunately there's also things like by conv => rw [a] rw [b] rw [c] which are a single tactic but should maybe be multi-line.)
Combinators for indentation-sensitive syntax
Lean 4 has lots of indentation-sensitive syntaxes where lines need to start at specific columns. But the only available formatting combinator to achieve this is ppLine before every item (including before the enclosing withPosition). It would be great to have more principled formatting combinators that guarantee that the output satisfies checkColGt. And also general combinators for sequences that are either newline or semicolon-separated (like tactic sequences or where clauses), which handle formatting and parsing transparently and consistently.
See also current hack for by ∙ skip.
Selecting ;/, or newlines during layout
That is, choose between { x := 1, y := 2 } or the multi-line version depending on whether it fits on a single line. This is maybe not the highest priority for reformatting, but you run into it very soon if you want to print automatically generated code, where you want to print large structures without the trailing commas as in idiomatic Lean.
See also let/have/by/etc.
