Non-fatal panics in IO

Stream: lean4

[Eric Wieser]

How can I make panic! behave as it does in a pure context within IO? This doesn't work:

#eval show IO Nat from do
    let ohno : Nat := panic!"wat"  -- panic isn't shown
    return 1

#eval show IO Nat from do
    pure <| panic!"wat"  -- panic isn't shown
    return 1

#eval show IO Nat from do
    let ohno := panic!"wat"  -- panic works, returns `1`
    return ohno + 1

[Eric Wieser]

#lean4 > ✔ Evaluation order @ 💬 seems somewhat relevant

[Aaron Liu]

it seems to be getting optimized out since the value isn't used

[Aaron Liu]

does that not happen in a pure context too?

[Eric Wieser]

cc Sebastian Ullrich, since the solutions you used in lean4#7321 look like they don't work anymore, suggesting those panics are now silent

[Eric Wieser]

#eval show IO Nat from do
    letI : Inhabited (IO Nat) := ⟨pure 1⟩
    panic!"wat"

#eval show IO Nat from do
    show BaseIO Unit from panic!"wat"
    return 1

both work