LeanFmt

LeanFmt is a structure-preserving code formatter for Lean. It parses complete Lean files with Lean's own parser, preserves source tokens and comments, and formats declarations and expressions through the fmt executable.

LeanFmt favors layouts that expose the structure of Lean code. In particular, leading operators connect continuation lines vertically while indentation shows nested expressions.

Formatting output

Before:

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)

After:

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)

Nested logical groups keep their local structure:

def leadingArrowExistentialApplicationWrap : Prop :=
  ∃ interfaceType,
    schema.lookupInterface interfaceName = some interfaceType
    ∧ ∀ interfaceField,
        interfaceField ∈ interfaceType.fields
        -> ∃ implementationField,
            Schema.lookupFieldDefinition implementationFields interfaceField.name
              = some implementationField
            ∧ fieldDefinitionImplements schema implementationField interfaceField

See the formatting design for the complete rule descriptions and more examples.

Add LeanFmt to a Lake package

Add the Git dependency to lakefile.toml:

[[require]]
name = "leanfmt"
git = "https://github.com/duckki/leanfmt.git"
rev = "v0.1.4"

Preserve the package's Lean version when resolving the dependency:

lake update --keep-toolchain

LeanFmt uses one source release across its supported Lean versions and tests the current toolchain and previous minor versions in CI. --keep-toolchain prevents Lake from replacing an older project's toolchain with the version recorded by LeanFmt. LeanFmt is then built with the project's selected Lean version, which is important because it loads that project's parser extensions and imported environments.

Projects that do not want LeanFmt in their published dependency graph may place the requirement in a separate development-tool Lake package instead. That tool package should also depend on the project by a local path so LeanFmt can load the project's dependencies and parser extensions.

Then format files or directories through Lake:

lake exe fmt LeanFmt/Formatter.lean
lake exe fmt LeanFmt
lake exe fmt --recursive LeanFmt
lake exe fmt --line-width 100 --recursive Mathlib

Directory arguments include directly contained .lean files. Pass --recursive or -r to include nested directories. Hidden files and directories discovered inside directory arguments are skipped by default. Explicitly supplied hidden paths are still processed. Pass --include-hidden to include hidden descendants during directory traversal. LeanFmt uses a 90-character line limit by default; pass --line-width N when a project uses a different convention.

To verify formatting without changing files, use --check:

lake exe fmt --check --recursive LeanFmt

The command exits nonzero if a file would change or cannot be formatted, making it suitable for CI.

Status

LeanFmt is under active development. Review formatting changes before applying it broadly. Formatting is deliberately conservative: it changes whitespace, keeps token text and order and preserves proof regions.

Project documentation

• Contributing defines the code-quality standards and local review gate.
• Design describes the style, philosophy, rules, and examples for Lean programmers considering the formatter.
• Architecture explains the implementation decisions and division between the syntax tree, rules, and renderer.
• Development covers building, testing, fixtures, tracing, profiling, validation, and contributing new rules.
• Comparison compares LeanFmt's style, architecture, and workflow with Lean's standard-library guide and pretty-lean.

License

LeanFmt is released under the MIT License.