leanfmt

leanfmt is an opinionated formatter for Lean code, written in Lean.

It is built for projects that care about trust as much as style: leanfmt parses files with Lean's own parser, loads project syntax extensions, preserves source tokens and comments, and refuses to silently rewrite code when its safety checks do not pass.

The style is structural. Continuation lines lead with the token that explains how they connect, while indentation shows the nesting.

def parenthesizedConjunctionChain (schema : Schema) : Prop :=
  namesAreUnique (schema.allTypes.map TypeDefinition.name)
  ∧ schema.objectType schema.queryType
  ∧ (∀ typeDefinition,
      typeDefinition ∈ schema.types -> typeDefinitionWellFormed schema typeDefinition)
  ∧ (∀ typeName objectTypeName,
      objectTypeName ∈ schema.getPossibleTypes typeName
      -> schema.objectType objectTypeName)

See the formatting design for the full style guide and more examples.

Why Use It

Lean-native: uses Lean's parser and the active Lake environment, so custom syntax is handled in the same context as your project.
Structure-preserving: works from a lossless syntax tree and formats whitespace around the code you wrote.
Conservative by design: checks token preservation, comments, parsing, and idempotence; if formatting cannot be proven safe, the original source stays in place.
Practical for adoption: format one file, a directory, or only files changed in a branch.

Quick Start

Add leanfmt to lakefile.toml:

[[require]]
name = "leanfmt"
git = "https://github.com/duckki/leanfmt.git"
rev = "vX.Y.Z"

Resolve the dependency without changing your project's Lean toolchain:

lake update --keep-toolchain

Format a file:

lake exe fmt MyProject/File.lean

Check formatting in CI:

lake exe fmt --check -r MyProject

Usage

Common options:

--version              Print the installed leanfmt and Lean version.
--line-width <number>  Set the target line width. Default: 90.

Format Common Targets

# One file
lake exe fmt MyProject/File.lean

# Files directly inside a directory
lake exe fmt MyProject

# A directory tree
lake exe fmt -r MyProject

# A project with a 100-column convention
lake exe fmt --line-width 100 -r MyProject

Directory traversal skips hidden descendants by default. Explicitly supplied hidden paths are still processed. Pass --include-hidden to include hidden descendants.

Check Without Rewriting

lake exe fmt --check -r MyProject

--check prints needs formatting: PATH for each file that would change and exits nonzero if a file would change or cannot be formatted, which makes it suitable for CI and pre-commit validation. Workers report file errors and check results directly; only abnormal exits and launch failures get an additional batch-level message.

Format Only Current Changes

This is the easiest way to adopt leanfmt incrementally.

# Check staged Lean files before committing
lake exe fmt --check $(git diff --cached --name-only --diff-filter=ACMR -- '*.lean')

# Format Lean files changed since HEAD
lake exe fmt $(git diff --name-only --diff-filter=ACMR HEAD -- '*.lean')

# CI: check files changed on this branch
lake exe fmt --check $(git diff --name-only --diff-filter=ACMR origin/main...HEAD -- '*.lean')

Run these commands only when the git diff --name-only ... '*.lean' list is nonempty. If your repository uses spaces in file names, pass those paths explicitly.

Tune The Run

# Use a specific worker count
lake exe fmt --jobs 8 -r MyProject

# Print the installed formatter version
lake exe fmt --version

Multi-file invocations use concurrent workers by default. leanfmt follows the selected Lake environment for each file group, including imported syntax extensions. Inputs without a common Lake root use the caller's environment. Each exact import group runs in a short-lived worker, even with --jobs 1. Use a lower worker count for memory-heavy imports.

--parser-integration lean-bench explicitly enables an audited LeanBench adapter that postpones benchmark setup commands during parsing. It accepts only audited imported implementations; other versions report an error. No integration is enabled by default. See the parser-effect contract for supported versions and library-provided annotations.

Leave Code Alone

Preserve the next complete syntax node:

-- leanfmt: off next
def handAligned   :   Nat:=
       1

Preserve a manual source region:

-- leanfmt: off
def handAligned   :   Nat:=
       1
-- leanfmt: on

leanfmt still formats parseable chunks outside ignored regions and keeps marker lines and enclosed lines unchanged, apart from normal line-ending handling.

Safety Model

leanfmt's formatter pipeline is intentionally narrow:

Lean parser
  -> lossless syntax tree
  -> syntax regrouping
  -> spacing and line-break rules
  -> width-aware renderer
  -> preservation and idempotence checks

The formatter preserves code tokens, token order, comments, and protected source regions. With --check-exception --check-idempotent, CI can also fail on unexpected code changes, actionable line overflow, or a non-idempotent result. Formatter development for first-class syntax can add --check-missing-rules to fail when a syntax node has no registered line-break rule.

leanfmt0.4.5