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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| still-nanoda | 👍 | 1.3 m | (-43%) | 817.9 MB | (-32%) | |
| sonanoda | 👍 | 1.4 m | (-41%) | 815.8 MB | (-32%) | |
| nanoda | 👍 | 1.1 m | (-51%) | 830.2 MB | (-31%) | |
| nanobruijn | 👍 | 1.2 m | (-48%) | 829.2 MB | (-31%) | |
| 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%) | |
| rpylean | ✋ | 1.6 m | 14.1 GB | |||
| mini | 🚫 | 44 ms | 70.3 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| parse-only | 👍 | 42.7 s | (-70%) | 1.2 GB | (-1%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |