normalize

Standardize Lean file formatting to prepare for other operations, especially merge operations. Use this tool to detect when a file is unusually structured, in which case other Axle operations may behave unexpectedly.

Available Normalizations

remove_sections, expand_decl_names, remove_duplicates, split_open_in_commands, normalize_module_comments, normalize_doc_comments

By default, remove_sections, remove_duplicates, and split_open_in_commands are applied. Use the normalizations parameter to customize which operations to apply.

remove_sections

Removes section, namespace, and end commands. Declaration names are fully qualified to preserve semantics. If a noncomputable section is removed, noncomputable section is re-inserted at the top of the file to preserve semantics.

Before:

namespace MyNamespace
noncomputable section MySection

theorem foo : 1 = 1 := rfl

end MySection
end MyNamespace

After:

noncomputable section
theorem MyNamespace.foo : 1 = 1 := rfl

expand_decl_names

Fully qualifies declaration names by prepending all enclosing namespaces. Useful for making declarations unambiguous without relying on namespace context.

Before:

open Option
example (α : Type) (x : α) :
    Option.getD (some x) x = x := by
  simp [getD]

After:

open Option
example (α : Type) (x : α) :
    Option.getD (Option.some x) x = x := by
  simp [Option.getD]

remove_duplicates

Removes duplicate commands, such as repeated open statements for the same module.

Before:

open Nat
open Nat
open List

After:

open Nat
open List

split_open_in_commands

Splits open [modules] in [decl] syntax into separate open and declaration commands. This makes the structure more explicit and easier to process.

Before:

open Nat in
theorem foo : succ 0 = 1 := rfl

After:

open Nat
theorem foo : succ 0 = 1 := rfl

normalize_module_comments

Converts module documentation comments (/-! ... -/) into regular block comments (/- ... -/). Module comments are typically used for file-level documentation.

normalize_doc_comments

Converts documentation comments (/-- ... -/) into regular block comments (/- ... -/). Doc comments are typically attached to declarations to provide API documentation.

Python API

result = await axle.normalize(
    content=lean_code,
    environment="lean-4.26.0",
    normalizations=["remove_sections", "expand_decl_names"],  # Optional: specify which normalizations
    failsafe=True,  # Optional: return original if normalization fails
)
print(result.content)
print(result.normalize_stats)

CLI

Usage: axle normalize CONTENT [OPTIONS]

# Normalize a file
axle normalize theorem.lean --environment lean-4.26.0
# Normalize and save to file
axle normalize theorem.lean -o normalized.lean --environment lean-4.26.0
# Apply only specific normalizations
axle normalize theorem.lean --normalizations remove_sections,expand_decl_names --environment lean-4.26.0
# Pipeline usage
cat theorem.lean | axle normalize - --environment lean-4.26.0 | axle merge - other.lean --environment lean-4.26.0
# Disable failsafe to always return normalized output
axle normalize theorem.lean --no-failsafe --environment lean-4.26.0

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/normalize \
    -d '{"content": "import Mathlib\nsection\ntheorem foo : 1 = 1 := rfl\nend", "environment": "lean-4.26.0"}' | jq

Input Parameters

Name	Type	Required	Description
content	str	Yes	A string of Lean code
environment	str	Yes	Environment to use (e.g., "lean-4.26.0", "lean-4.25.1")
normalizations	list[str]	No	List of normalizations to apply. Options: remove_sections, expand_decl_names, remove_duplicates, split_open_in_commands, normalize_module_comments, normalize_doc_comments. Default: remove_sections, remove_duplicates, split_open_in_commands
failsafe	bool	No	If true (default), returns original content unchanged if normalization introduces errors
ignore_imports	bool	No	If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false
timeout_seconds	float	No	Maximum execution time (default: 120)

Output Fields

Name	Type	Description
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists
tool_messages	dict	Messages from normalize tool with errors, warnings, infos lists
content	str	The normalized Lean code
normalize_stats	dict[str, int]	Count of each normalization operation applied
timings	dict	Timing info: total_ms, parse_ms

Example Response

{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\ntheorem foo : 1 = 1 := rfl\n",
  "timings": {
    "total_ms": 92,
    "parse_ms": 87
  },
  "normalize_stats": {
    "remove_sections": 2
  }
}