Test "std"
Expected: 👍 accept · Size: 569.0 MB · Lines: 10.8 M · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 7.8 s | (÷14) | 1.1 GB | (+17%) | |
| mathgraph | 👍 | 11.3 s | (÷9.9) | 915.8 MB | (-2%) | |
| nanoclo | 👍 | 36.3 s | (÷3.1) | 840.2 MB | (-10%) | |
| con-ron | 👍 | 50.3 s | (÷2.2) | 937.2 MB | (+1%) | |
| nanobruijn | 👍 | 1.0 m | (-45%) | 793.8 MB | (-15%) | |
| nanoda | 👍 | 1.0 m | (-46%) | 701.7 MB | (-25%) | |
| lazylean | 👍 | 1.0 m | (-45%) | 708.9 MB | (-24%) | |
| con-leche | 👍 | 1.9 m | (0%) | 696.8 MB | (-25%) | |
| tenet-jvm | 👍 | 1.0 m | (-45%) | 4.8 GB | (×5.3) | |
| eink0rn | 👍 | 1.5 m | (-20%) | 2.0 GB | (×2.2) | |
| official | 👍 | 1.9 m | (0%) | 930.0 MB | (0%) | |
| ind-models | 👍 | 2.1 m | (+11%) | 765.5 MB | (-18%) | |
| lean4lean | 👍 | 2.6 m | (+41%) | 1.1 GB | (+18%) | |
| tenet | 👍 | 2.0 m | (+9%) | 2.9 GB | (×3.1) | |
| tenet-hs | 👍 | 2.0 m | (+9%) | 1.3 GB | (+41%) | |
| lean4cobol | ⌛ | 0 ms | 0 B | |||
| evmlean | 🚫 | 0 ms | 0 B | |||
| mini | 🚫 | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 23.3 s | 277.0 MB | |||
| nanoclo-fortran | 👍 | 2.3 m | (+24%) | 1.7 GB | (+92%) | |
| kiota | ⌛ | 0 ms | 0 B | |||
| metalean-fast | 👍 | 6.5 m | (×3.5) | 2.0 GB | (×2.2) | |
| canonical-min | ✋ | 33.5 s | 2.0 GB | |||
| rpylean | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| parse-only | 👍 | 29.9 s | (÷3.8) | 929.9 MB | (0%) |