Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 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 | 👍 | 364 ms | (÷6.1) | 498.5 MB | (×2.2) | |
| ind-models | 👍 | 3.0 s | (+33%) | 267.9 MB | (+16%) | |
| official-nightly | 👍 | 2.2 s | (-4%) | 227.7 MB | (-1%) | |
| evmlean | 🚫 | 305 ms | 107.3 MB | |||
| nanoda | 👍 | 1.4 s | (-38%) | 153.1 MB | (-34%) | |
| mini | 🚫 | 39 ms | 74.1 MB | |||
| lean4lean | 👍 | 2.9 s | (+29%) | 292.9 MB | (+27%) | |
| sokonanoda | 👍 | 395 ms | (÷5.7) | 538.5 MB | (×2.3) | |
| zignodamus | 👍 | 492 ms | (÷4.5) | 483.6 MB | (×2.1) | |
| nanoclo | 👍 | 679 ms | (÷3.3) | 298.5 MB | (+29%) | |
| nanobruijn | 👍 | 6.1 s | (×2.7) | 208.1 MB | (-10%) | |
| kiota | 👍 | 4.4 s | (+95%) | 505.7 MB | (×2.2) | |
| official | 👍 | 2.2 s | (0%) | 231.0 MB | (0%) | |
| vow-lean-kernel | 👍 | 58.8 s | (×26) | 383.5 MB | (+66%) | |
| rpylean | 👍 | 4.8 s | (×2.1) | 838.1 MB | (×3.6) | |
| official-v4.28.0 | 👍 | 2.6 s | (+18%) | 247.2 MB | (+7%) | |
| still-nanoda | 👍 | 1.4 s | (-37%) | 152.7 MB | (-34%) | |
| nyaya | ✋ | 2.0 s | 195.6 MB | |||
| parse-only | 👍 | 564 ms | (÷4.0) | 78.3 MB | (÷2.9) |