Test "std"
Expected: 👍 accept · Size: 526.1 MB · Lines: 10.0 M · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 9.8 m · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 10.3 s | (÷10) | 873.7 MB | (0%) | |
| sokonanoda | 👍 | 10.9 s | (÷9.4) | 1006.7 MB | (+15%) | |
| nanoclo | 👍 | 33.5 s | (÷3.1) | 841.8 MB | (-4%) | |
| con-ron | 👍 | 51.3 s | (÷2.0) | 994.4 MB | (+14%) | |
| lazylean | 👍 | 58.5 s | (-43%) | 670.4 MB | (-23%) | |
| nanoda | 👍 | 54.6 s | (-47%) | 671.3 MB | (-23%) | |
| nanobruijn | 👍 | 56.0 s | (-46%) | 756.4 MB | (-13%) | |
| con-leche | 👍 | 2.0 m | (+16%) | 879.9 MB | (+1%) | |
| eink0rn | 👍 | 1.4 m | (-21%) | 1.9 GB | (×2.2) | |
| ind-models | 👍 | 2.1 m | (+21%) | 863.8 MB | (-1%) | |
| official | 👍 | 1.7 m | (0%) | 873.7 MB | (0%) | |
| lean4lean | 👍 | 2.4 m | (+40%) | 1.0 GB | (+19%) | |
| tenet | 👍 | 1.8 m | (+7%) | 2.8 GB | (×3.3) | |
| nanoclo-fortran | 👍 | 2.1 m | (+21%) | 1.7 GB | (+95%) | |
| lean4cobol | ⌛ | 0 ms | 0 B | |||
| evmlean | 🚫 | 0 ms | 0 B | |||
| mini | 🚫 | 0 ms | 0 B | |||
| overfull | 💥 | 1.1 m | 19.2 MB | |||
| kiota | ⌛ | 0 ms | 0 B | |||
| canonical-min | 🚫 | 31.0 s | 1.9 GB | |||
| rpylean | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | 💥 | 1.2 m | 434.2 MB | |||
| official-v4.28.0 | 👍 | 2.5 m | (+48%) | 1.0 GB | (+17%) | |
| still-nanoda | 👍 | 1.1 m | (-34%) | 651.3 MB | (-25%) | |
| nyaya | 🚫 | 0 ms | 0 B | |||
| parse-only | 👍 | 27.8 s | (÷3.7) | 873.5 MB | (0%) |