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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| still-nanoda | 👍 | 1.2 m | (-43%) | 643.5 MB | (-36%) | |
| sonanoda | 👍 | 1.2 m | (-41%) | 644.6 MB | (-36%) | |
| nanoda | 👍 | 58.7 s | (-53%) | 652.1 MB | (-35%) | |
| nanobruijn | 👍 | 1.0 m | (-50%) | 702.4 MB | (-30%) | |
| official-nightly | 👍 | 2.0 m | (-3%) | 998.1 MB | (-1%) | |
| official | 👍 | 2.1 m | (0%) | 1008.0 MB | (0%) | |
| official-v4.28.0 | 👍 | 2.6 m | (+24%) | 1021.2 MB | (+1%) | |
| lean4lean | 💥 | 1.3 m | 990.1 MB | |||
| rpylean | ✋ | 2.6 m | 14.1 GB | |||
| mini | 🚫 | 41 ms | 70.3 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| parse-only | 👍 | 31.3 s | (-75%) | 948.0 MB | (-6%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |