Test "perf/unroll-versus-evaluate"
Expected: 👍 accept · Size: 44.6 KB · Lines: 1.2 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 50.0 s · 📄 Declaration · 🔗 Source
The declaration to check compares
count #(n+1) and N.add (count #n) #1
where #k is the numeral with k successors, and count #k evaluates to #k
in Θ(k²) reductions.
The head constants differ. Unrolling count once turns the left side into the
right side, leaving a traversal of the shared numeral #n, for Θ(n);
evaluating both sides costs Θ(n²). The test asks which of two differing
head constants a checker chooses to unfold.
N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §2.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 2 ms | (÷12) | 46.9 MB | (-29%) | |
| mathgraph | 👍 | 2 ms | (÷13) | 48.4 MB | (-27%) | |
| nanoclo | 👍 | 4 ms | (÷8.7) | 46.4 MB | (-30%) | |
| con-ron | 👍 | 24 ms | (-22%) | 59.6 MB | (-10%) | |
| nanobruijn | 👍 | 2 ms | (÷17) | 10.6 MB | (÷6.2) | |
| nanoda | 👍 | 2 ms | (÷21) | 3.2 MB | (÷21) | |
| lazylean | 👍 | 1 ms | (÷22) | 21.8 MB | (÷3.0) | |
| con-leche | 👍 | 7 ms | (÷4.7) | 23.0 MB | (÷2.9) | |
| eink0rn | 👍 | 2 ms | (÷13) | 14.0 MB | (÷4.7) | |
| official | 👍 | 31 ms | (0%) | 65.9 MB | (0%) | |
| ind-models | 👍 | 107 ms | (×3.4) | 109.7 MB | (+67%) | |
| lean4lean | 👍 | 31 ms | (+1%) | 97.7 MB | (+48%) | |
| tenet | 👍 | 134 ms | (×4.3) | 44.9 MB | (-32%) | |
| tenet-hs | 👍 | 3 ms | (÷9.4) | 13.1 MB | (÷5.0) | |
| lean4cobol | 👍 | 25 ms | (-21%) | 17.2 MB | (÷3.8) | |
| evmlean | 🚫 | 2.2 s | 286.3 MB | |||
| mini | ⌛ | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 👍 | 1.8 s | (×59) | 1.4 GB | (×22) | |
| tenet-jvm | 👍 | 162 ms | (×5.2) | 68.7 MB | (+4%) | |
| nanoclo-fortran | 👍 | 8 ms | (÷3.7) | 8.2 MB | (÷8.1) | |
| kiota | 👍 | 8 ms | (÷4.0) | 18.5 MB | (÷3.6) | |
| metalean-fast | 👍 | 38 ms | (+23%) | 82.0 MB | (+24%) | |
| canonical-min | 🚫 | 390 ms | 1.1 GB | |||
| rpylean | 👍 | 1 ms | (÷23) | 6.0 MB | (÷11) | |
| vow-lean-kernel | 👍 | 120 ms | (×3.9) | 9.2 MB | (÷7.1) | |
| parse-only | 👍 | 30 ms | (-3%) | 65.7 MB | (0%) |