Test "perf/discarded-argument"
Expected: 馃憤 accept 路 Size: 15.9鈥疜B 路 Lines: 367 路 lean4export: 3.1.0 路 Lean: 4.29.1 路 Timeout: 50.0鈥痵 路 馃搫 Declaration 路 馃敆 Source
The declaration to check compares
dropArg (count #n) and dropArg (count #(n+1))
where count #k evaluates to the numeral #k in 螛(k虏) reductions, and
dropArg maps every numeral to N.O.
Unfolding dropArg leaves N.O against N.O, for 螛(1). Comparing the
arguments first evaluates two numerals of different value, for 螛(n虏), and
then throws that answer away. The test asks whether a checker unfolds a
constant before looking at an argument the constant never uses.
N=200 in the Lean source. From Courant and Leroy, POPL 2026, 搂10.
| Checker | Result | 鈴憋笍 | 馃 | |||
|---|---|---|---|---|---|---|
| mathgraph | 馃憤 | 1鈥痬s | (梅222) | 35.8鈥疢B | (-45%) | |
| sokonanoda | 馃憤 | 1鈥痬s | (梅222) | 35.6鈥疢B | (-46%) | |
| nanoclo | 馃憤 | 2鈥痬s | (梅71) | 47.6鈥疢B | (-27%) | |
| con-ron | 馃憤 | 26鈥痬s | (梅6.3) | 65.0鈥疢B | (-1%) | |
| lazylean | 馃憤 | 10鈥痬s | (梅16) | 24.6鈥疢B | (梅2.7) | |
| nanoda | 馃憤 | 5鈥痬s | (梅34) | 3.3鈥疢B | (梅20) | |
| nanobruijn | 馃憤 | 22鈥痬s | (梅7.5) | 10.2鈥疢B | (梅6.5) | |
| con-leche | 馃憤 | 11鈥痬s | (梅15) | 26.0鈥疢B | (梅2.5) | |
| eink0rn | 馃憤 | 90鈥痬s | (-46%) | 48.7鈥疢B | (-26%) | |
| ind-models | 馃憤 | 695鈥痬s | (脳4.2) | 105.3鈥疢B | (+61%) | |
| official | 馃憤 | 166鈥痬s | (0%) | 65.6鈥疢B | (0%) | |
| lean4lean | 馃憤 | 1.2鈥痵 | (脳7.4) | 99.5鈥疢B | (+52%) | |
| tenet | 馃憤 | 153鈥痬s | (-8%) | 49.1鈥疢B | (-25%) | |
| nanoclo-fortran | 馃憤 | 4鈥痬s | (梅45) | 5.1鈥疢B | (梅13) | |
| lean4cobol | 馃憤 | 3.8鈥痵 | (脳23) | 16.1鈥疢B | (梅4.1) | |
| evmlean | 馃毇 | 1.3鈥痵 | 131.6鈥疢B | |||
| mini | 馃憤 | 37鈥痬s | (梅4.5) | 73.4鈥疢B | (+12%) | |
| overfull | 馃挜 | 1.7鈥痬 | 47.7鈥疢B | |||
| kiota | 馃憤 | 5鈥痬s | (梅31) | 11.4鈥疢B | (梅5.8) | |
| canonical-min | 馃毇 | 388鈥痬s | 1.1鈥疓B | |||
| rpylean | 馃憤 | 268鈥痬s | (+62%) | 37.4鈥疢B | (-43%) | |
| vow-lean-kernel | 馃憤 | 7.3鈥痵 | (脳44) | 16.8鈥疢B | (梅3.9) | |
| official-v4.28.0 | 馃憤 | 742鈥痬s | (脳4.5) | 75.5鈥疢B | (+15%) | |
| still-nanoda | 馃憤 | 31鈥痬s | (梅5.3) | 3.2鈥疢B | (梅20) | |
| nyaya | 馃挜 | 2.1鈥痬 | 15.9鈥疢B | |||
| parse-only | 馃憤 | 28鈥痬s | (梅5.9) | 65.2鈥疢B | (-1%) |