check

Evaluate Lean code and collect all messages (errors, warnings, and info). Use this to check if code is valid without verification against a formal statement, or to get the output of #check / #eval statements.

Python API

result = await axle.check(
    content="import Mathlib\n#eval 2+2",
    environment="lean-4.26.0",
    mathlib_linter=False,     # Optional
    ignore_imports=False,     # Optional
    timeout_seconds=120,      # Optional
)

print(result.okay)  # True if code is valid
print(result.content)  # The processed Lean code
print(result.lean_messages.infos)  # ["4\n"]

CLI

Usage: axle check CONTENT [OPTIONS]

# Basic usage
axle check theorem.lean --environment lean-4.26.0
# Pipeline usage
cat theorem.lean | axle check - --environment lean-4.26.0
# Exit non-zero if code is invalid
axle check theorem.lean --strict --environment lean-4.26.0
# Use in shell conditionals
if axle check theorem.lean --strict --environment lean-4.26.0 > /dev/null; then
    echo "Valid Lean code"
fi

HTTP API

curl -s -X POST http://10.1.10.100:8989/v1/axle/check \
    -d '{"content": "import Mathlib\n#eval 2+2", "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")
mathlib_linter	bool	No	If true, enables Mathlib's standard linter set. Requires Mathlib. Default: false
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
okay	bool	True if Lean code is valid (no compilation errors)
content	str	The Lean code that was actually processed (after header injection if imports were ignored)
lean_messages	dict	Messages from Lean compiler with errors, warnings, infos lists
tool_messages	dict	Messages from check tool with errors, warnings, infos lists. Tool errors include structural validation issues (e.g., use of sorry, unsafe axioms).
failed_declarations	list[str]	Declaration names that failed validation
timings	dict	Timing info: total_ms

Example Response

{
  "okay": true,
  "content": "import Mathlib\n\n#eval 2+2\n",
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": ["4\n"]
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "timings": {
    "total_ms": 62
  },
  "failed_declarations": []
}