Pretty-Printing: A Graduate Course in Rust

A hands-on graduate-level crash course in the theory and engineering of pretty-printers (a.k.a. code formatters), built up from first principles in Rust. The end goal is to write a complete pretty-printer for System F omega with macros, and along the way to read and re-implement every classical algorithm in the literature.

This course exists because Lean 4 currently lacks a real pretty-printer and linter. By working through it, the reader should gain enough background to contribute one to the Lean / Mathlib / CSLib community, or to write a formatter for any other language (toy or production).

Audience

You should be comfortable with:

• Rust at the level of The Rust Programming Language (chapters 1 to 17).
• Basic discrete math: induction, recursion, big-O complexity.
• The lambda calculus at the level of Pierce's TAPL chapters 5, 9, 23, 30.

No prior knowledge of pretty-printing is assumed.

How to use the course

Each directory NNNN-topic/ contains:

• README.md lecture notes with full theory, paper references, and worked examples.
• src/lib.rs annotated with // #anchor: name ... // #end blocks. The README pulls fenced code from these anchors via make inject-snippets. Code never drifts from prose because both are tested in CI.
• src/exercises.rs with easy, medium, hard exercises (all returning todo!()).
• src/solutions.rs with reference solutions.
• tests/ verifying both the examples and the solutions.

Courses are sequential. Complete them in order. Each exercise is annotated with a difficulty tag.

Course outline

Part I: Foundations

#	Topic	What you learn
0000	Introduction	What is a pretty-printer? History and taxonomy.
0001	Naive printer	The string-concat baseline and why it is wrong.
0002	Document model	The Doc algebra: text, line, concat, nest, group.

Part II: Classical algorithms (paper-by-paper)

#	Algorithm	Reference
0003	Two-stack streaming, O(n)	Oppen, Pretty Printing, TOPLAS 1980
0004	Monoidal combinators	Hughes, Design of a Pretty-printing Lib, 1995
0005	Algebraic, lazy, choice-based	Wadler, A Prettier Printer, 1998
0006	Strict re-implementation	Lindig, Strictly Pretty, 2000
0007	Combinator extensions	Leijen, wl-pprint, 2001

Part III: Advanced layout

#	Algorithm	Reference
0008	Constant-space, linear-time	Swierstra and Chitil, Linear, bounded, functional pretty-printing, JFP 2009
0009	Optimal, Pareto frontier	Bernardy, A Pretty But Not Greedy Printer, ICFP 2017

Part IV: From documents to source code

#	Topic	Reference / focus
0010	Operator precedence, prefix/postfix	Ramsey, Unparsing Expressions With Prefix and Postfix Operators, SP&E 1998
0011	Real-world formatters survey	rustfmt, prettier, black/ruff, ocamlformat, gofmt, dprint
0012	Trivia, comments, idempotence	Concrete vs abstract syntax, roundtrip property
0013	Lexer	Building a tokenizer for System F omega
0014	Parser	Pratt-style recursive descent

Part V: System F family

#	Topic	What you build
0015	System F printer	Polymorphic types, term/type abstractions
0016	System F omega	Type-level lambdas and kinds
0017	Macros	A small Lisp-style macro layer
0018	Final	A polished CLI bundling everything

Building

make setup            # rustup + components
make build            # cargo build --workspace
make test             # cargo test --workspace
make ci               # full local CI pipeline

The first build takes a minute or two; subsequent builds are incremental.

Snippet machinery

Code in README.md files is never edited directly. Instead, the Examples or lib.rs files contain anchors:

// #anchor: my_example
fn demo() -> i32 { 42 }
// #end

And the README references them:

```rust fromFile:src/lib.rs#my_example
```

(indented four spaces above so the script does not try to inject it).

CI runs make check-snippets to ensure the README is in sync with the code. A pre-commit hook (make setup-hooks) runs the injection on staged READMEs.

References

The full bibliography is in REFERENCES.md. Per-course references are listed at the end of each lecture's README.

Lore

The lore/ directory contains long-form essays: the history of pretty-printing in Lisp and Smalltalk, why the same algorithm shows up in three different forms in three different functional languages, etc.

License

Apache 2.0.