feat: extensible code formatter

[mhuisi]

This PR adds an extensible code formatter with formatting rules for all stable syntax declared in Lean core.

I will be on PTO for three weeks. This PR will only be merged in mid-October.

The formatter is integrated with the language server. There is deliberately no command-line integration so far.
Please do not format entire projects using the formatter until we add command-line integration. The formatting rules have not fully stabilized yet, so large re-formatting diffs may still occur.

Please also hold off on writing a huge corpus of custom formatters for now. The formatting API itself will still be subject to change a lot for a while. We will also provide a proper reference manual entry once it is more stable.

After merging this PR, we will provide some way to quickly scan the diff of formatting the entirety of core and Mathlib so that you can judge the formatting output for yourself. There will also be an opportunity to provide constructive feedback after this PR is merged.

Please appreciate that no formatter will always produce output that exactly fits your tastes, and that the main purpose of a formatter is to eliminate style discussions during code review and produce one consistent and acceptable style across an eco-system so that we can focus on more pressing work.

Significant deviations from common Lean style

Infix operators are layouted to the front of the line instead of the end of the line, and the formatter prefers breaking on infix operators. This significantly aids legibility because the infix operators at the start of the line hint at the structure of the term without having to scan to the end of the line.
This rule also includes type ascriptions, as well as the type ascription colon in signatures.
I am aware that this a significant deviation from the existing style and that it will be difficult to get used to, but after reading Lean code in dozens of different formatting styles produced by various iterations of the auto-formatter, I am strongly convinced that formatting infix operators to the start of the line is a significant improvement to readability, including in signatures.

The formatter is consistently using K&R style brackets. This style is common in core, but not in Mathlib. This bracket style has several nice layouting properties, especially when elements within the brackets need to be broken across multiple lines.

Doc strings and block comments use core-style. Specifically, in multi-line block comments and doc strings, both the opening token and the closing token are placed on their own lines, and the body is not indented.

Prefix operators are separated from the operand by a space if the operand is not an atomic term. This makes it easier to visually identify that the prefix operator is not attached to the head of the term, but to the entire term. For atomic terms, the space is still omitted.

The auto-formatter re-formats multi-line string literals to use string gaps and explicit newlines. This makes it very explicit when a string accidentally includes indentation, for example.

Implementation details

The core formatting algorithm is based on A Pretty Expressive Printer by Sorawee Porncharoenwase, Justin Pombrio and Emina Torlak with a number of adjustments and extensions to facilitate formatting a language like Lean.
Pretty Expressive optimizes a cost function instead of greedily choosing the first configuration that fits, permits designating arbitrary alternatives (including ones that change non-whitespace symbols), allows encoding unaligned concatenation and is reasonably efficient. All of these traits make it a good choice for a huge, extensible language like Lean.

The core formatting algorithm is independent of Lean and consumes a generic input document that encodes all possible layouts.
Lean's formatter then takes a Syntax that was produced by Lean's parser and transforms it into the input language of the core formatting algorithm using a set of formatters that are registered using a fmt attribute, each of which is implemented using a set of common layouting primitives. This allows for a great deal of flexibility when it is necessary, makes formatting explicit and partially protects formatters against changes to parsers via TSyntax anti-quotations.

When there is no formatter for a given Syntax, the formatter retains the formatting of that sub-tree from the input document, making it possible to use the formatter before implementing formatting rules for all syntax.

The formatter follows the philosophy that not formatting a piece of code is better than formatting it in a broken manner. Importantly, it does not attempt to automatically derive formatters for syntax where it is not clear what it should be formatted as. This means that there are default formatters for parsers that parse atomic syntax, infix operators, prefix operators and postfix operators, but no default formatters for more complex parsers - someone has to sit down, look at the syntax and decide what it should look like.

Comments are handled automatically by the formatting infrastructure. Formatters for specific kinds of Syntax need not concern themselves with how comments should be layouted and the formatting infrastructure automatically re-inserts them into the constructed formatting documents.

In case of a broken formatter (or a correct formatter for a broken parser), the formatter re-parses the output of the formatter. If the new output does not parse, it will keep the input document. When using the formatter in the language server, we do not attempt to re-elaborate the file for latency reasons, though we may do so for the future command line integration.

The formatter tries to avoid changing non-whitespace syntax. The only cases where it currently removes tokens are ones where whether a token should be placed or not depends on the specific rendering that is picked by the formatter (e.g. semi-colons when something does not fit on a single line) and could not be implemented as a separate Syntax to Syntax normalization pass before the formatter. In a few rare cases, it may also add parentheses when it cannot prove that formatting a specific subterm is sound without them.

Known issues

• There are a few rare cases in Lean's grammar where stripping a semi-colon and replacing it with a correctly aligned line break will cause the output to not parse or not elaborate anymore. These cases do not occur often, and we recommend users to wrap code in parentheses instead of using semi-colons to delimit them. We accept this as a short-coming of our grammar.
• Both in Mathlib and core, there are a few parsers that produce Syntax that is not round-tripping. The formatter validates this prior to formatting and refuses to format files where this invariant is violated. Over time, we can hopefully fix these parsers.
• The formatter is well fast enough to format all of core and Mathlib, but its performance could still be improved. We have not yet spent a significant amount of effort on optimizing it.

Future work

The formatter is not yet integrated with the delaborator or code actions for example. It is currently only a source file formatter. We will likely extend it to these other use cases as well, and central parts of the infrastructure are already in place for this (e.g. the formatter is capable of transferring arbitrary meta-data from the input Syntax to the rendering).

AI usage

Many of the formatters were generated by AI from a tight natural language spec describing exactly how to implement every single formatter and then read carefully and tested by me. The majority of the actual formatting infrastructure was designed and implemented by me.

[tydeu]

As a head-sup, this should also be imported in Lake.All.