Make the pretty printer usable for code formatting

[Kha]

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...)

[Kha]

An example of a missing feature is "hanging" do/by/fun

[leodemoura]

See #867

[leodemoura]

@Kha Should we close this issue?

[Kha]

I fear I could only close it in good conscience if we used it to reformat our own codebase :) .

[gebner]

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.

1. {} (empty collection) should be formatted without a space.
2. { x := 1, y := 2 } should be formatted on a single line.
3. { 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.

[gaearon]

Hi folks! Have y’all looked at Prettier in the JS ecosystem? In particular it deals with a lot of similar complexity as what you seem to be running into. Some details about its approach:

• https://prettier.io/docs/technical-details
• https://archive.jlongster.com/A-Prettier-Formatter
• https://medium.com/@fvictorio/how-to-write-a-plugin-for-prettier-a0d98c845e70

I’m not an expert in this area so it’s hard for me to compare what’s implemented / missing but I wonder if there’s anything in Prettier’s approach, implementation and/or abstraction that would be helpful to take a look at.

Separately, I’m also lowkey curious whether it would be difficult to actually write a Prettier plugin for Lean (this would of course be a separate project and would need to somehow parse Lean into JSON, and then use Prettier’s utilities for the actual act of pretty printing). I presume this is a less favored path for folks here (not nice to cross languages or fail to reuse existing work) but I’m still wondering about technical feasibility. I’d just really like to get something running, and Prettier is pretty much the industry standard in JS land. Not sure if any non-JS plugins are good though. Of course a Lean-native implementation is probably the way to go though. But I really want to have something soon-ish as a user…