ADV-050 · evidence animation · replay

Cristian Guerra · QA Automation · Medellín, Colombia · @criguex

Fresh kernel replay

leanchecker --fresh ignores the compiled files and re-checks every declaration, Mathlib included, from an empty environment.

0.0 / 20.0 s

How to read this animation: Bars show the recorded replay time. The kernel panel shows which kernel implementations have actually examined the proofs; lean4lean could not be built for Lean 4.34 and never examined them.

Accessible explanation, equations, and source records


Open the evidence animation gallery · Download standalone HTML