Test "cedar"
Expected: 👍 accept · Size: 832.0 MB · Lines: 15.3 M · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 15.7 m · 📄 Declaration · 🔗 Source
Lean formalization of, and proofs about, Cedar.
Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.
This test case exports the whole Cedar module and as such contains even unused parts Init and
Batteries.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 11.8 s | (÷12) | 2.7 GB | (+99%) | |
| mathgraph | 👍 | 26.3 s | (÷5.4) | 3.7 GB | (×2.8) | |
| nanoclo | 👍 | 50.4 s | (÷2.8) | 1.2 GB | (-10%) | |
| con-ron | 🚫 | 9.0 s | 1.0 GB | |||
| nanobruijn | 👍 | 1.3 m | (-45%) | 1.3 GB | (-5%) | |
| nanoda | 👍 | 1.3 m | (-46%) | 939.4 MB | (-32%) | |
| lazylean | 👍 | 1.3 m | (-46%) | 1015.4 MB | (-27%) | |
| con-leche | 🚫 | 14.4 s | 676.9 MB | |||
| eink0rn | 👍 | 2.0 m | (-16%) | 2.4 GB | (+80%) | |
| official | 👍 | 2.4 m | (0%) | 1.4 GB | (0%) | |
| ind-models | 👍 | 3.7 m | (+58%) | 1.0 GB | (-23%) | |
| lean4lean | 👍 | 3.2 m | (+37%) | 1.6 GB | (+17%) | |
| tenet | 👍 | 2.4 m | (+3%) | 3.4 GB | (×2.5) | |
| tenet-hs | 👍 | 2.4 m | (+2%) | 1.5 GB | (+10%) | |
| lean4cobol | ⌛ | 0 ms | 0 B | |||
| evmlean | 🚫 | 0 ms | 0 B | |||
| mini | 🚫 | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 33.6 s | 379.8 MB | |||
| tenet-jvm | 👍 | 1.3 m | (-45%) | 4.9 GB | (×3.6) | |
| nanoclo-fortran | 👍 | 5.4 m | (×2.3) | 2.9 GB | (×2.1) | |
| kiota | ⌛ | 0 ms | 0 B | |||
| metalean-fast | 👍 | 3.7 m | (+59%) | 2.0 GB | (+48%) | |
| canonical-min | ✋ | 48.4 s | 2.5 GB | |||
| rpylean | 👍 | 6.7 m | (×2.8) | 5.5 GB | (×4.1) | |
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| parse-only | 👍 | 43.4 s | (÷3.3) | 1.4 GB | (0%) |