Checker "canonical-min" on test "bugs/constlevels"
Checker: canonical-min · Version: kernel-arena (0acb45d) · 📄 Declaration · 🔗 Source
Test: bugs/constlevels · Expected: ✋ reject · Size: 15.3 KB · Lines: 283 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration
Result: 🚫 declined · exit code 2 · wall time: 1.09 s · instructions: 3.4 G · max rss memory: 1.1 GB · run 2026-10-24 16:27:15 UTC
stderr:
PANIC at List.head! Init.Data.List.BasicAux:75:12: empty list backtrace: .lake/build/bin/canonical-min-arena(+0x6093c6e) [0x560c6fd95c6e] .lake/build/bin/canonical-min-arena(+0x60940fc) [0x560c6fd960fc] .lake/build/bin/canonical-min-arena(+0x9344a) [0x560c69d9544a] .lake/build/bin/canonical-min-arena(+0x92e67) [0x560c69d94e67] .lake/build/bin/canonical-min-arena(+0xa9fe1) [0x560c69dabfe1] .lake/build/bin/canonical-min-arena(+0x60abe26) [0x560c6fdade26] .lake/build/bin/canonical-min-arena(+0x831ba) [0x560c69d851ba] .lake/build/bin/canonical-min-arena(+0x60a8df6) [0x560c6fdaadf6] .lake/build/bin/canonical-min-arena(+0x1348d78) [0x560c6b04ad78] .lake/build/bin/canonical-min-arena(+0x134c13a) [0x560c6b04e13a] .lake/build/bin/canonical-min-arena(+0x8323f) [0x560c69d8523f] .lake/build/bin/canonical-min-arena(+0xa8bf8) [0x560c69daabf8] .lake/build/bin/canonical-min-arena(+0xe2437) [0x560c69de4437] .lake/build/bin/canonical-min-arena(+0xe650e) [0x560c69de850e] .lake/build/bin/canonical-min-arena(+0x60a668a) [0x560c6fda868a] .lake/build/bin/canonical-min-arena(+0x207aa) [0x560c69d227aa] .lake/build/bin/canonical-min-arena(+0x220ec) [0x560c69d240ec] .lake/build/bin/canonical-min-arena(+0x2454f) [0x560c69d2654f] .lake/build/bin/canonical-min-arena(+0x25025) [0x560c69d27025] .lake/build/bin/canonical-min-arena(+0x25933) [0x560c69d27933] .lake/build/bin/canonical-min-arena(+0x1e792) [0x560c69d20792] /nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x2b285) [0x7f8b85820285] /nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(__libc_start_main+0x88) [0x7f8b85820338] .lake/build/bin/canonical-min-arena(+0x1f895) [0x560c69d21895] Declined: could not translate _test: Unknown constant `_inhabitedExprDummy`