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.9 s | (÷12) | 2.7 GB | (×2.0) | |
| mathgraph | 👍 | 26.3 s | (÷5.4) | 3.6 GB | (×2.7) | |
| nanoclo | 👍 | 50.4 s | (÷2.8) | 1.2 GB | (-10%) | |
| con-ron | 🚫 | 7.7 s | 1.0 GB | |||
| nanobruijn | 👍 | 1.3 m | (-45%) | 1.3 GB | (-5%) | |
| nanoda | 👍 | 1.3 m | (-46%) | 931.8 MB | (-33%) | |
| lazylean | 👍 | 1.3 m | (-46%) | 1014.2 MB | (-27%) | |
| con-leche | 🚫 | 15.9 s | 870.2 MB | |||
| tenet-jvm | 👍 | 1.3 m | (-46%) | 4.9 GB | (×3.6) | |
| eink0rn | 👍 | 2.0 m | (-16%) | 2.6 GB | (+89%) | |
| 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.5 m | (+7%) | 3.3 GB | (×2.5) | |
| tenet-hs | 👍 | 2.4 m | (+2%) | 1.5 GB | (+11%) | |
| 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 | 376.8 MB | |||
| nanoclo-fortran | 👍 | 5.6 m | (×2.4) | 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.9) | 5.8 GB | (×4.3) | |
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| parse-only | 👍 | 43.4 s | (÷3.3) | 1.4 GB | (0%) |