Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 1.0 m · 📄 Declaration · 🔗 Source
A grind tactic test from the Lean 4 test suite.
This produces a theorem with a rather large proof term that needs fast reduction.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 328 ms | (÷6.6) | 516.3 MB | (×2.3) | |
| sokonanoda | 👍 | 339 ms | (÷6.4) | 586.5 MB | (×2.6) | |
| nanoclo | 👍 | 674 ms | (÷3.2) | 268.5 MB | (+18%) | |
| con-ron | 👍 | 1.4 s | (-36%) | 288.7 MB | (+27%) | |
| lazylean | 👍 | 816 ms | (÷2.6) | 86.0 MB | (÷2.7) | |
| nanoda | 👍 | 1.4 s | (-36%) | 153.2 MB | (-33%) | |
| nanobruijn | 👍 | 6.2 s | (×2.9) | 201.2 MB | (-12%) | |
| con-leche | 👍 | 3.1 s | (+42%) | 221.6 MB | (-3%) | |
| eink0rn | 👍 | 1.3 s | (-41%) | 347.7 MB | (+52%) | |
| ind-models | 👍 | 3.0 s | (+37%) | 270.7 MB | (+19%) | |
| official | 👍 | 2.2 s | (0%) | 228.1 MB | (0%) | |
| lean4lean | 👍 | 2.9 s | (+34%) | 294.6 MB | (+29%) | |
| tenet | 👍 | 3.5 s | (+62%) | 505.0 MB | (×2.2) | |
| nanoclo-fortran | 👍 | 1.4 s | (-35%) | 316.3 MB | (+39%) | |
| lean4cobol | 👍 | 31.2 s | (×14) | 192.4 MB | (-16%) | |
| evmlean | 🚫 | 306 ms | 106.0 MB | |||
| mini | 🚫 | 39 ms | 74.1 MB | |||
| overfull | 💥 | 1.5 m | 49.1 MB | |||
| kiota | 👍 | 4.2 s | (+96%) | 345.9 MB | (+52%) | |
| canonical-min | 🚫 | 986 ms | 1.1 GB | |||
| rpylean | 👍 | 4.4 s | (×2.0) | 836.9 MB | (×3.7) | |
| vow-lean-kernel | 💥 | 55.7 s | 250.2 MB | |||
| official-v4.28.0 | 👍 | 2.6 s | (+23%) | 247.9 MB | (+9%) | |
| still-nanoda | 👍 | 1.4 s | (-35%) | 152.3 MB | (-33%) | |
| nyaya | ✋ | 2.0 s | 195.0 MB | |||
| parse-only | 👍 | 557 ms | (÷3.9) | 83.0 MB | (÷2.7) |