Test "perf/shared-subterm"
Expected: 👍 accept · Size: 50.1 KB · Lines: 1.3 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
The declaration to check compares
ldepth (perfect #n leaf) and ldepth2 (perfect #n leaf)
where perfect #n leaf builds the perfect binary tree of depth n in n steps
that each duplicate the tree so far, and ldepth and ldepth2 both return
the length of the leftmost path.
The head constants differ, so both sides are evaluated, and neither traversal
looks beyond the leftmost path: ldepth walks n nodes for Θ(n), ldepth2
folds n additions over growing numerals for Θ(n²). The test asks whether a
checker consumes the tree through its representation, for Θ(n²), or
expands it into the 2ⁿ nodes of its normal form.
N=1000 in the Lean source. From Courant and Leroy, POPL 2026, §10.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 6 ms | (÷10) | 56.5 MB | (-22%) | |
| ind-models | 👍 | 216 ms | (×3.7) | 110.1 MB | (+53%) | |
| official-nightly | 👍 | 58 ms | (-2%) | 73.4 MB | (+2%) | |
| evmlean | 🚫 | 2.0 s | 137.6 MB | |||
| nanoda | 👍 | 15 ms | (÷4.0) | 6.0 MB | (÷12) | |
| mini | 💥 | 20.2 s | 13.1 GB | |||
| lean4lean | 👍 | 76 ms | (+29%) | 105.4 MB | (+46%) | |
| sokonanoda | 👍 | 6 ms | (÷9.6) | 56.5 MB | (-22%) | |
| zignodamus | 👍 | 8 ms | (÷7.6) | 16.0 MB | (÷4.5) | |
| nanoclo | 👍 | 9 ms | (÷6.7) | 62.4 MB | (-13%) | |
| nanobruijn | 👍 | 14 ms | (÷4.4) | 17.5 MB | (÷4.1) | |
| kiota | 👍 | 15 ms | (÷4.1) | 20.0 MB | (÷3.6) | |
| official | 👍 | 59 ms | (0%) | 72.0 MB | (0%) | |
| vow-lean-kernel | 👍 | 309 ms | (×5.2) | 26.0 MB | (÷2.8) | |
| rpylean | 👍 | 38 ms | (-35%) | 46.8 MB | (-35%) | |
| official-v4.28.0 | 👍 | 68 ms | (+16%) | 79.1 MB | (+10%) | |
| still-nanoda | 👍 | 15 ms | (÷4.0) | 6.1 MB | (÷12) | |
| nyaya | 💥 | 5.1 s | 412.4 MB | |||
| parse-only | 👍 | 30 ms | (-49%) | 62.3 MB | (-13%) |