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%) | 830.8 MB | (-31%) |
| nanobruijn | 👍 | 1.3 m | (-44%) | 917.2 MB | (-24%) |
| 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%) |
| lean4lean | 👍 | 4.2 m | (+79%) | 1.2 GB | (+2%) |
| mini | 🚫 | 45 ms | 70.1 MB | ||
| always-decline | 🚫 | 1 ms | 2.8 MB | ||
| always-reject | ✋ | 1 ms | 2.8 MB | ||
| rpylean | ✋ | 43.0 s | 14.1 GB | ||
| parse-only | 👍 | 42.7 s | (-70%) | 1.2 GB | (-1%) |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |