Test "cedar"
Expected: 👍 accept · Size: 790.9 MB · Lines: 14.6 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 29.6 s | (÷4.9) | 6.6 GB | (×4.4) | |
| ind-models | 👍 | 3.5 m | (+45%) | 1.2 GB | (-21%) | |
| official-nightly | 👍 | 2.2 m | (-8%) | 1.3 GB | (-10%) | |
| evmlean | 🚫 | 0 ms | 0 B | |||
| nanoda | 👍 | 1.2 m | (÷2.0) | 873.6 MB | (-43%) | |
| mini | 🚫 | 0 ms | 0 B | |||
| lean4lean | 👍 | 3.0 m | (+25%) | 1.5 GB | (+2%) | |
| sokonanoda | 👍 | 32.4 s | (÷4.4) | 6.9 GB | (×4.6) | |
| zignodamus | 👍 | 40.5 s | (÷3.6) | 8.3 GB | (×5.5) | |
| nanoclo | 👍 | 48.9 s | (÷2.9) | 1.4 GB | (-7%) | |
| nanobruijn | 👍 | 1.2 m | (-48%) | 887.0 MB | (-42%) | |
| kiota | ✋ | 40.3 s | 1.3 GB | |||
| official | 👍 | 2.4 m | (0%) | 1.5 GB | (0%) | |
| vow-lean-kernel | 💥 | 1.5 m | 510.7 MB | |||
| rpylean | 👍 | 3.8 m | (+57%) | 4.9 GB | (×3.3) | |
| official-v4.28.0 | 👍 | 3.1 m | (+30%) | 1.5 GB | (+1%) | |
| still-nanoda | 👍 | 1.4 m | (-42%) | 884.0 MB | (-42%) | |
| nyaya | 🚫 | 0 ms | 0 B | |||
| parse-only | 👍 | 42.0 s | (÷3.4) | 1.5 GB | (-1%) |