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 | (+20%) | |
| mathgraph | 👍 | 11.3 s | (÷9.9) | 931.6 MB | (0%) | |
| nanoclo | 👍 | 36.3 s | (÷3.1) | 855.3 MB | (-8%) | |
| con-ron | 👍 | 58.3 s | (-48%) | 1008.9 MB | (+9%) | |
| nanobruijn | 👍 | 1.0 m | (-45%) | 793.8 MB | (-15%) | |
| nanoda | 👍 | 1.0 m | (-46%) | 695.3 MB | (-25%) | |
| lazylean | 👍 | 1.0 m | (-45%) | 710.3 MB | (-24%) | |
| con-leche | 👍 | 2.2 m | (+19%) | 731.3 MB | (-21%) | |
| eink0rn | 👍 | 1.5 m | (-21%) | 2.0 GB | (×2.2) | |
| official | 👍 | 1.9 m | (0%) | 929.7 MB | (0%) | |
| ind-models | 👍 | 2.1 m | (+11%) | 763.6 MB | (-18%) | |
| lean4lean | 👍 | 2.6 m | (+41%) | 1.1 GB | (+18%) | |
| tenet | 👍 | 2.0 m | (+7%) | 2.8 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 | 325.2 MB | |||
| tenet-jvm | 👍 | 1.0 m | (-45%) | 4.8 GB | (×5.3) | |
| nanoclo-fortran | 👍 | 2.3 m | (+22%) | 1.7 GB | (+88%) | |
| kiota | ⌛ | 0 ms | 0 B | |||
| metalean-fast | 👍 | 6.5 m | (×3.5) | 2.0 GB | (×2.3) | |
| 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) | 930.1 MB | (0%) |