nano-lean

A minimalist (but complete) parallel Lean type checker in Rust built on unbound, using de Bruijn indices for binders.

We built it on NbE (normalization by evaluation), in the Berger and Schwichtenberg tradition which is why it's so fast, because beta reduction is just an environment push and every value remembers its own normal form.

The package providers four binaries:

• nl-fast: the main fast typechecker
• nl-ref: reference kernel for checking core-syntax files and exports
• nl-mutate: mutation tester that edits an export and diffs every checker's verdict
• nl-watch: a fast cached build watch tool for Lake projects

Successfully type-checks all of Mathlib (718k declarations) with 0 errors and 0 timeouts.

# Install nl-fast and nl-ref
cargo install --git https://github.com/sdiehl/nano-lean

# Check a Lean export (NDJSON or blean)
nl-fast FILE.ndjson [-j THREADS] [--import-threads N]
nl-fast FILE.blean [-j THREADS]

# Reject an export whose primitives differ from a trusted export of Init
nl-fast --prelude init.blean FILE.blean

# Skip declarations a previous run accepted
nl-fast --cache FILE.accepted FILE.blean

# Check one module over its imports' interfaces, from `olean-export join -m`
nl-fast VIEW.blean [--check-imports]

# Check one declaration straight from oleans, decoding only the proofs it needs
nl-fast --olean Init --declaration Nat.add_comm

# Rebuild and recheck a Lake project on every save, from its root
nl-watch MODULE [-j THREADS]

# Check a core-syntax file
nl-ref examples/core.ltc

# Check an export with the reference kernel, optionally in parallel
nl-ref --export FILE.ndjson
nl-ref --export-parallel JOBS [--memory-mib MIB] FILE.ndjson

# Write a core-syntax file's declarations as an NDJSON export
nl-ref --emit FILE.ltc > FILE.ndjson

# Mutate an export and report checker disagreements, shrinking each finding
nl-mutate [--seed N] [--per-op N] [--op NAME] [--out DIR] FILE.ndjson

Checking Mathlib

Exports come from olean-export, run inside a Mathlib checkout so lake env can find its oleans.

# Install the exporter
cargo install olean-export

# Fetch Mathlib and its prebuilt oleans (no compile)
git clone --depth 1 https://github.com/leanprover-community/mathlib4 && cd mathlib4
lake exe cache get

# Export Mathlib to a file, then check it
lake env olean-export Mathlib -o mathlib.ndjson
nl-fast mathlib.ndjson

# Or pipe it straight through
lake env olean-export Mathlib -q | nl-fast

# The blean binary format is smaller and faster to load, nl-fast detects it
lake env olean-export Mathlib -f blean -o mathlib.blean
nl-fast mathlib.blean

# Convert an existing export between NDJSON and blean
olean-export convert mathlib.ndjson -o mathlib.blean

Performance

Checking all of Mathlib from the blean binary export:

	M5 -j 1	M5 -j 10	M4 Max -j 14
Wall time	57.4 s	16.7 s	11.85 s
Kernel check	53.5 s	12.5 s	7.55 s
Peak memory footprint	7.5 GB	9.2 GB	10.7 GB

Checking the full imported environment of OpenAI's Navier–Stokes and Euler proofs from the blean binary export

	M4 Max -j 14
Wall time	17.13 s
Kernel check	12.11 s
Peak memory footprint	12.29 GB

Checking the full imported environment of CSLib from the blean binary export

	M4 Max -j 14
Wall time	4.42 s
Kernel check	2.75 s
Peak memory footprint	6.92 GB

Checking OpenAI's quasi-Riemann hypothesis proof and its dependencies from the blean binary export

	M4 Max -j 14
Wall time	3.66 s
Kernel check	2.58 s
Peak memory footprint	7.42 GB

Checking OpenAI's Erdős reciprocal-sum proof and its dependencies from the blean binary export

	M4 Max -j 14
Wall time	23.33 s
Kernel check	19.11 s
Peak memory footprint	26.42 GB

Caching

--cache FILE skips declarations a previous run accepted and records the new ones. Each declaration is keyed by a hash over its whole dependency closure, so editing a declaration rechecks it and everything that depends on it, and a new checker version starts the file over.

The keys and the file format come from olean-export's key and accepted modules, so other checkers can share one store, each in its own section. With olean-export --per-module and join, an unchanged module's export can be reused as is too.

nl-fast --cache mathlib.accepted mathlib.blean
nl-fast --cache mathlib.accepted --cache-audit mathlib.blean  # recheck everything

In nano-lean.toml, cache = "mathlib.accepted" turns it on and --no-cache turns it off for one run.

Configuration

nl-fast reads nano-lean.toml from the working directory if one exists, or the file given with --config. Every key is optional and a flag on the command line overrides it. A relative prelude or cache path resolves against the file's directory.

threads = 10
steps = 200000000
arena_mib = 3072
session_mib = 64
fallback = false
term_core = false
prelude = "init.blean"
axioms = ["propext", "Classical.choice", "Quot.sound"]
cache = "mathlib.accepted"
cache_audit = false

Without the file the defaults are one thread, no prelude check, no axiom restriction and no cache.

License

Released under the MIT License. See LICENSE for details.