Test "perf/grind-ring-5"
Expected: 👍 accept · Size: 9.7 MB · Lines: 199.2 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| nanoda | 👍 | 1.5 s | (-38%) | 151.9 MB | (-34%) | |
| nanobruijn | 👍 | 6.7 s | (+174%) | 202.0 MB | (-13%) | |
| official-nightly | 👍 | 2.4 s | (-3%) | 222.5 MB | (-4%) | |
| official | 👍 | 2.4 s | (0%) | 231.2 MB | (0%) | |
| official-v4.28.0 | 👍 | 2.7 s | (+10%) | 244.1 MB | (+6%) | |
| mini | 🚫 | 43 ms | 70.3 MB | |||
| evmlean | 🚫 | 360 ms | 88.3 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| lean4lean | 👍 | 3.4 s | (+41%) | 303.3 MB | (+31%) | |
| still-nanoda | 👍 | 1.5 s | (-39%) | 151.5 MB | (-34%) | |
| rpylean | 👍 | 7.4 s | (+204%) | 1.2 GB | (+436%) | |
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| sokonanoda | 👍 | 1.1 s | (-53%) | 357.2 MB | (+55%) | |
| parse-only | 👍 | 635 ms | (-74%) | 86.0 MB | (-63%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-99%) |