Test "cedar"
Expected: 👍 accept · Size: 728.6 MB · Lines: 13.4 M · lean4export: 3.1.0 · Lean: 4.26.0 · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| nanoda | 👍 | 1.1 m | (-51%) | 836.1 MB | (-30%) | |
| nanobruijn | 👍 | 1.2 m | (-48%) | 852.7 MB | (-29%) | |
| official-nightly | 👍 | 2.3 m | (-3%) | 1.2 GB | (0%) | |
| official | 👍 | 2.3 m | (0%) | 1.2 GB | (0%) | |
| official-v4.28.0 | 👍 | 2.8 m | (+20%) | 1.2 GB | (+1%) | |
| mini | 🚫 | 44 ms | 70.3 MB | |||
| evmlean | 🚫 | 358 ms | 88.6 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| lean4lean | 👍 | 4.2 m | (+79%) | 1.2 GB | (+3%) | |
| still-nanoda | 👍 | 1.3 m | (-43%) | 813.9 MB | (-32%) | |
| rpylean | ✋ | 43.2 s | 2.4 GB | |||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| sokonanoda | 👍 | 1.1 m | (-52%) | 3.7 GB | (+218%) | |
| parse-only | 👍 | 42.7 s | (-70%) | 1.2 GB | (-1%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |