Checker "lean4lean" on test "bugs/closure-level-subst"
Checker: lean4lean · Version: arena (bce3448) · 📄 Declaration · 🔗 Source
Test: bugs/closure-level-subst · Expected: ✋ reject · Size: 4.0 KB · Lines: 74 · lean4export: 3.1.0 · Lean: 4.35.0 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 105 ms · instructions: 581.1 M · max rss memory: 104.4 MB · run 2026-10-27 15:13:01 UTC
stderr:
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1375:4: invalid environment extension has been accessed
backtrace:
.lake/build/bin/lean4lean(+0x8730425) [0x55b3bd010425]
.lake/build/bin/lean4lean(+0x8727b37) [0x55b3bd007b37]
.lake/build/bin/lean4lean(lean_panic_fn_borrowed+0x2b) [0x55b3bd007c1b]
.lake/build/bin/lean4lean(Lean.EnvExtension.getStateUnsafe [arity↓, private]+0x910) [0x55b3b6fef560]
.lake/build/bin/lean4lean(Lean.ppExprWithInfos+0xee) [0x55b3b702bf7e]
.lake/build/bin/lean4lean(Lean.MessageData.ofExpr [λ]+0x110) [0x55b3b7033670]
.lake/build/bin/lean4lean(<apply/2>+0x9e9) [0x55b3bd0158f9]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0x164) [0x55b3b703a264]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa2a) [0x55b3b703ab2a]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0x764) [0x55b3b703a864]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa2a) [0x55b3b703ab2a]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa19) [0x55b3b703ab19]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa19) [0x55b3b703ab19]
.lake/build/bin/lean4lean(Lean.MessageData.toString+0x15) [0x55b3b703b945]
.lake/build/bin/lean4lean(Lean4Lean.Replay.throwKernelException [arity↓] (lean4lean)+0xb89) [0x55b3b6dfe759]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant [λ] (lean4lean)+0x25) [0x55b3b6e01595]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x709) [0x55b3b6e02d49]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replay (lean4lean)+0x207) [0x55b3b6e07e17]
.lake/build/bin/lean4lean([lean] main+0x9a5) [0x55b3b6c08545]
.lake/build/bin/lean4lean(+0x8725687) [0x55b3bd005687]
.lake/build/bin/lean4lean(+0x8725b55) [0x55b3bd005b55]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x9dd53) [0x7f4c78dc2d53]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x12563c) [0x7f4c78e4a63c]
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1375:4: invalid environment extension has been accessed
backtrace:
.lake/build/bin/lean4lean(+0x8730425) [0x55b3bd010425]
.lake/build/bin/lean4lean(+0x8727b37) [0x55b3bd007b37]
.lake/build/bin/lean4lean(lean_panic_fn_borrowed+0x2b) [0x55b3bd007c1b]
.lake/build/bin/lean4lean(Lean.EnvExtension.getStateUnsafe [arity↓, private]+0x910) [0x55b3b6fef560]
.lake/build/bin/lean4lean(Lean.ppExprWithInfos+0xee) [0x55b3b702bf7e]
.lake/build/bin/lean4lean(Lean.MessageData.ofExpr [λ]+0x110) [0x55b3b7033670]
.lake/build/bin/lean4lean(<apply/2>+0x9e9) [0x55b3bd0158f9]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0x164) [0x55b3b703a264]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa2a) [0x55b3b703ab2a]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0x764) [0x55b3b703a864]
.lake/build/bin/lean4lean(Lean.MessageData.formatAux+0xa2a) [0x55b3b703ab2a]
.lake/build/bin/lean4lean(Lean.MessageData.toString+0x15) [0x55b3b703b945]
.lake/build/bin/lean4lean(Lean4Lean.Replay.throwKernelException [arity↓] (lean4lean)+0xb89) [0x55b3b6dfe759]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant [λ] (lean4lean)+0x25) [0x55b3b6e01595]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x709) [0x55b3b6e02d49]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstants (lean4lean)+0x1b) [0x55b3b6e0222b]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replayConstant (lean4lean)+0x186) [0x55b3b6e027c6]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xe8) [0x55b3b6e049b8]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Std.DTreeMap.Internal.Impl.forInStep spec at Lean4Lean.Replay.replayConstants (lean4lean)+0xae) [0x55b3b6e0497e]
.lake/build/bin/lean4lean(Lean4Lean.Replay.replay (lean4lean)+0x207) [0x55b3b6e07e17]
.lake/build/bin/lean4lean([lean] main+0x9a5) [0x55b3b6c08545]
.lake/build/bin/lean4lean(+0x8725687) [0x55b3bd005687]
.lake/build/bin/lean4lean(+0x8725b55) [0x55b3bd005b55]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x9dd53) [0x7f4c78dc2d53]
/nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x12563c) [0x7f4c78e4a63c]
uncaught exception: at lower: (kernel) declaration type mismatch, 'lower' has type
[Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
Family.{1}
but it is expected to have type
[Error pretty printing expression: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
Family.{0}