Test "std"
Expected: 👍 accept · Size: 526.1 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The complete Std library export from Lean 4.
This test contains the standard library extensions beyond core Lean 4, including:
- Enhanced data structures (HashMap, RBTree, etc.)
- Additional mathematical operations
- Extended list and array operations
- Utility functions and theorems
This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.
| Checker | Result | ⏱️ | 🧠 | ||
|---|---|---|---|---|---|
| nanoda | 👍 | 58.5 s | (-53%) | 655.4 MB | (-35%) |
| nanobruijn | 👍 | 1.1 m | (-46%) | 758.4 MB | (-25%) |
| official-nightly | 👍 | 2.0 m | (-3%) | 997.8 MB | (-1%) |
| official | 👍 | 2.1 m | (0%) | 1006.8 MB | (0%) |
| official-v4.28.0 | 👍 | 2.6 m | (+24%) | 1021.1 MB | (+1%) |
| lean4lean | 💥 | 1.3 m | 992.9 MB | ||
| mini | 🚫 | 41 ms | 70.1 MB | ||
| always-decline | 🚫 | 1 ms | 2.8 MB | ||
| always-reject | ✋ | 1 ms | 2.8 MB | ||
| rpylean | ✋ | 2.8 m | 14.1 GB | ||
| parse-only | 👍 | 31.3 s | (-75%) | 948.0 MB | (-6%) |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |