Declaration benchmark

Each declaration is elaborated and checked by the native C kernel compiled to WebAssembly. Dependencies are checked once, in source import order. The timer includes elaboration and the final closed check; it excludes reading source files. Inspection and full normalization are not requested.

The selected deadline is polled cooperatively in JavaScript and C. Cleanup or a long operation between polls can exceed the deadline; anything over the selected deadline fails the speed target. Timings vary by machine and cache state. A timeout is a performance result, not a mathematical refutation.

Blocked entries record the first unavailable dependency reached, with its root blocker. Failed entries may indicate an elaborator or migration defect, unsupported syntax, or a faulty proof. Universe templates are listed separately: their concrete uses are checked, but the template itself is not a closed kernel judgement.

The Run button checks the current corpus locally in a worker, with live progress. Cancel stops the worker. A browser run does not upload results or change the saved benchmark. Keep this tab active for comparable timings. The command-line equivalent is npm run benchmark:cubical.