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.6 s | (-53%) | 646.9 MB | (-36%) | |
| nanobruijn | 👍 | 1.0 m | (-49%) | 699.9 MB | (-31%) | |
| official-nightly | 👍 | 2.0 m | (-3%) | 997.9 MB | (-1%) | |
| official | 👍 | 2.1 m | (0%) | 1007.9 MB | (0%) | |
| official-v4.28.0 | 👍 | 2.6 m | (+24%) | 1021.1 MB | (+1%) | |
| mini | 🚫 | 41 ms | 70.3 MB | |||
| evmlean | 🚫 | 358 ms | 88.4 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| lean4lean | 💥 | 1.3 m | 992.7 MB | |||
| still-nanoda | 👍 | 1.2 m | (-43%) | 650.7 MB | (-35%) | |
| rpylean | ✋ | 4.0 m | 14.2 GB | |||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| sokonanoda | 👍 | 47.1 s | (-62%) | 838.1 MB | (-17%) | |
| parse-only | 👍 | 31.3 s | (-75%) | 948.0 MB | (-6%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |