panic! not working

Stream: general

[Konstantin Weitz]

I have this piece of code:

def die : String :=
  panic! "Panic!"

def main : IO Unit :=
  let res := die
  IO.println ("Error:" ++ res ++ "END")

And I run it with:

lake build; .lake/build/bin/main

I would expect to see "Panic!" but instead I get:

Error:END

What's going on here? Any flag I can pass to fix this/invoke lean differently?

[Robin Arnez]

die is a constant, so it gets evaluated at initialization time. However, panics are not printed at initialization time. See https://github.com/leanprover/lean4/blob/f2e06ead5436e01e585a15dcc795ccb96bf3d182/src/Lean/Compiler/IR/EmitC.lean#L170 and lean4#534 for reference

[Konstantin Weitz]

Thanks @Robin Arnez . Is there a way to turn the panic back on? I have constants that are quite subtle and it would be good to get the messages for debugging when I made a mistake. I'm ok not having these constants be evaluated at init time, but don't know how to achieve that.

[Robin Arnez]

There are multiple options:

1. Use die (_ : Unit) : String and die (). That means the constant will be evaluated every time it's used though, which might be unwanted.
2. Use die : Thunk String and die.get. That means the constant will be evaluated once; but the first time it's used and not at initialization time.

[Konstantin Weitz]

Hmm, so I tried both, but neither is working. I still don't get any panic messages printed. Here is my exact code:

def die : Thunk String :=
  Thunk.mk (panic! "Panic!")

def main : IO Unit :=
  IO.println ("Error:" ++ die.get ++ "END")

and

def die (_:Unit) : String :=
  panic! "Panic!"

def main : IO Unit :=
  IO.println ("Error:" ++ die () ++ "END")

What does work for some bizzare reason, is if I add a debug message before, then it also prints the panic:

def die (_:Unit):  String :=
  dbg_trace "about to panic"
  panic! "Panic!"

def main : IO Unit :=
  IO.println ("Error:" ++ die () ++ "END")

I get

Build completed successfully.
about to panic
PANIC at die Main:192:2: Panic!
backtrace:
..

How does this work? Any better way to do it rather than having the dbg message

[Robin Arnez]

Oh, you need to put set_option compiler.extract_closed false in above the constants or otherwise it extracts them into their own auxiliary definitions

[Robin Arnez]

So:

set_option compiler.extract_closed false in
def die : Thunk String := .mk fun _ =>
  panic! "Panic!"

def main : IO Unit :=
  IO.println ("Error:" ++ die.get ++ "END")

[Robin Arnez]

Or wait is it just enough to add fun _ =>?

[Robin Arnez]

Konstantin Weitz schrieb:

and

def die (_:Unit) : String :=
  panic! "Panic!"

def main : IO Unit :=
  IO.println ("Error:" ++ die () ++ "END")

Weird, that should've worked...

[Robin Arnez]

Which version are you on?

[Konstantin Weitz]

lake --version
Lake version 5.0.0-b02228b (Lean version 4.20.0)

[Konstantin Weitz]

I'm running it as follows, not sure if that's the normal way

lake build
.lake/build/bin/main