Reduction of arguments and `panic!`

Stream: general

[Juneyoung Lee]

I found that this command does not print panic:

#eval (.some 10:Option Int).getD (panic! "why is expression conditionally reduced?")
-- Successfully prints 10

My understanding of Lean was that it was using call-by-value semantics, hence the panic! must have raised regardless of the value of .some 10. When does panic! happen?

[Aaron Liu]

looks like it might be getting optimized out?

set_option trace.compiler.ir.result true
#eval (.some 10:Option Int).getD (panic! "why is expression conditionally reduced?")

[Kyle Miller]

The @[macro_inline] switches to call-by-name semantics https://github.com/leanprover/lean4/blob/3b0f2862196c6a8af9eb0025ee650252694013dd/src/Init/Prelude.lean#L2897

The way it does this is that the definition is inlined early on in the compiler pipeline.

[Juneyoung Lee]

Ah, makes sense! Thanks :)