Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.8 MB · Lines: 200.3 k · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 273 ms | (÷7.9) | 505.5 MB | (×2.2) | |
| mathgraph | 👍 | 325 ms | (÷6.6) | 502.3 MB | (×2.2) | |
| nanoclo | 👍 | 677 ms | (÷3.2) | 280.5 MB | (+23%) | |
| con-ron | 👍 | 1.5 s | (-31%) | 378.2 MB | (+66%) | |
| nanobruijn | 👍 | 6.4 s | (×3.0) | 202.2 MB | (-11%) | |
| nanoda | 👍 | 1.4 s | (-36%) | 152.2 MB | (-33%) | |
| lazylean | 👍 | 809 ms | (÷2.7) | 86.3 MB | (÷2.6) | |
| con-leche | 👍 | 3.4 s | (+56%) | 188.9 MB | (-17%) | |
| eink0rn | 👍 | 1.3 s | (-41%) | 356.6 MB | (+56%) | |
| official | 👍 | 2.2 s | (0%) | 228.3 MB | (0%) | |
| ind-models | 👍 | 2.9 s | (+35%) | 271.8 MB | (+19%) | |
| lean4lean | 👍 | 2.9 s | (+35%) | 295.1 MB | (+29%) | |
| tenet | 👍 | 3.7 s | (+73%) | 544.2 MB | (×2.4) | |
| tenet-hs | 👍 | 2.5 s | (+18%) | 243.9 MB | (+7%) | |
| lean4cobol | 👍 | 31.1 s | (×14) | 194.0 MB | (-15%) | |
| evmlean | 🚫 | 307 ms | 107.0 MB | |||
| mini | 🚫 | 39 ms | 74.8 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 537 ms | 81.5 MB | |||
| tenet-jvm | 👍 | 3.9 s | (+83%) | 503.7 MB | (×2.2) | |
| nanoclo-fortran | 👍 | 1.4 s | (-35%) | 315.0 MB | (+38%) | |
| kiota | 👍 | 4.3 s | (+98%) | 341.6 MB | (+50%) | |
| metalean-fast | 👍 | 3.6 s | (+67%) | 238.8 MB | (+5%) | |
| canonical-min | ✋ | 979 ms | 1.1 GB | |||
| rpylean | 👍 | 4.4 s | (×2.0) | 789.0 MB | (×3.5) | |
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| parse-only | 👍 | 559 ms | (÷3.9) | 84.0 MB | (÷2.7) |