Recheck a compiled Lean olean file using the Lean kernel.

lake exe lean4checker <module> will replay the environment in <module>, starting from the environment provided by its imports, ensuring that the kernel accepts all declarations.

lake exe lean4checker without an argument will run lean4checker in parallel on every .olean file on the search path (note that this include Lean 4 and all dependencies of your project).

You can also use lake exe lean4checker --fresh Mathlib.Data.Nat.Basic to replay all the constants (both imported and defined in that file) into a fresh environment. This is single threaded, and may be much slower.

This is not an external verifier, as it uses the Lean kernel itself. However it is useful as a tool to detect "environment hacking", i.e. using metaprogramming facilities to build an inconsistent Lean Environment.

Usage

To run this in another Lean project, use:

lake env path/to/lean4checker

or

lake env path/to/lean4checker Mathlib.Data.Nat.Basic

to check a single file.

Caveats

Despite .olean files being "fairly cross-platform", lean4checker will reject .oleans that were compiled on a system that does not use the same bignum library as your system, so it advisable to not rely on cached .oleans.