lean 4 and panics

Stream: general

[Jukka Suomela]

Hi all, I've got some fundamental misunderstanding of what "panic" means in Lean 4 (e.g. in the context of the documentation of functions like Array.get! and String.toNat!).

For example, here is a program that is utterly broken in so many different ways and that I was expecting to fail in some visible sense, either at compilation time or run time (note the array indexing overflow + attempts of parsing invalid strings as natural numbers):

def foo (x : Nat) : Nat := Id.run do
  let a : Nat := Array.mkArray0.get! x
  let b := "bad".toNat!
  panic! "bad bad"
  panic "bad bad bad"
  unreachable!
  assert! false
  x + a + b

def main : IO Unit :=
  let r := foo 123
  IO.println s!"all good, got result {r}"

Yet if I just do lake exe foo, it happily compiles it and runs it and it prints out "all good, got result 0" and terminates successfully. And if I remove just assert! false, it says "all good, got result 123".

Is there some way to ask Lean 4 to really panic in cases in which it claims to panic (when running stuff with lake)? Or should I just avoid all functions that say something about panicking in their documentation?

[Jannis Limperg]

Set environment variable LEAN_ABORT_ON_PANIC=1.

[Jukka Suomela]

@Jannis Limperg Many thanks, this helps! At least the program crashes now! It just doesn't print out anything useful, but it also doesn't complete successfully if I'm using Array.get! or String.toNat! incorrectly. And apparently assert! false is also leading to crashes now, good.

[Jukka Suomela]

I still don't understand the semantics of stuff like panic! and friends, as e.g. this still succeeds:

def foo (x : Nat) : Nat := Id.run do
  if x == 123 then
    panic! "bad bad"
  x

def main : IO Unit :=
  let r := foo 123
  IO.println s!"all good, got result {r}"

While e.g. this crashes:

def foo (x : Nat) : Nat := Id.run do
  if x == 123 then
    panic! "bad bad"
  if x == 123 then
    panic! "bad bad"
  x

def main : IO Unit :=
  let r := foo 123
  IO.println s!"all good, got result {r}"

[Jukka Suomela]

Also, is there any way to ask it to also print out something to stderr when it crashes, or do I need an external shell script for that?

[Jason Rute]

I don’t know why, but it works with single =

[Jukka Suomela]

I've noticed that there are lots of minor variants, some of which "work" and some don't and I don't really see a pattern here…

[Jason Rute]

I think the panic behavior is confusing in Lean. Maybe this is a subtle way the developers are telling us to do things right. :smile: Using IO monads errors, option types (List.get?), or just prove that the behavior is correct (.List.get). But it is annoying to not be sure your code will respect panics.

[Kyle Miller]

I think the issue is that the compiler is free to eliminate the panic since this is the Id monad, and there's no data dependency on the panic.

set_option trace.compiler.ir.rc true
def foo (x : Nat) : Nat := Id.run do
  if x == 123 then
    panic! "bad bad"
  x
/-
def foo (x_1 : @& obj) : obj :=
  inc x_1;
  ret x_1
-/

[Kyle Miller]

The IR is saying that the function was simplified to the identity function.

[Kyle Miller]

The fix is easy: make sure you have a data dependence on the panic.

def foo (x : Nat) : Nat := Id.run do
  if x == 123 then
    panic! "bad bad"
  else
    x

In the first case, it must return the result of the panic!, so it must be executed.

[Jukka Suomela]

Oh right I should use panic! like this:

def foo (x : Nat) : Nat := Id.run do
  if x == 123 then
    return panic! "bad bad"
  x

[Jukka Suomela]

I for some reason thought panic! is magic that implicitly returns but it doesn't.

[Jukka Suomela]

Would be awesome to have a compiler warning that I should use the result of panic!…

[Jason Rute]

Or a linter.

[Jukka Suomela]

OK, stuff making more sense now. Always do return panic! in this kind of context and always run everything with LEAN_ABORT_ON_PANIC=1.

[Kyle Miller]

Jukka Suomela said:

I for some reason thought panic! is magic that implicitly returns but it doesn't.

These examples make me think that it should implicitly return. That's doable, if there were a doElem macro for it.

Feel free to create a Lean 4 issue with the feedback that the version without the return was surprising that it didn't work.

[Jukka Suomela]

Btw, is there a reason LEAN_ABORT_ON_PANIC=1 isn't a default?

[Jason Rute]

Also, why does assert! return the default value even without a data dependency, but panic! doesn’t? Is assert immediately returning?

[Kyle Miller]

assert! isn't a function, it's a do element (docs#Lean.Parser.Term.doAssert)

[Kyle Miller]

It turns out it expands to assert! c; k where k is the rest of the do block, and this expands to an if/else. docs#Lean.Elab.Term.expandAssert

[Jason Rute]

Which is what maybe panic! should also be? Or is the issue that panic! also works outside of do blocks?

[Kyle Miller]

There shouldn't be a problem with it working outside of do blocks. There are a few examples of multipurpose syntax like that (even do works as a do element and as a term)

[Jannis Limperg]

Jukka Suomela said:

Btw, is there a reason LEAN_ABORT_ON_PANIC=1 isn't a default?

The reason is that this may invalidate proofs about programs with panics. From a logical perspective, panic! "..." = default, where default is some arbitrary (but fixed) element of the respective type. Hence, for example, (panic! "..." : Nat) = 0. So this is a provably correct implementation of multiplication:

import Aesop

def times : Nat → Nat → Nat
  | _, 0 => panic! "zero"
  | n, .succ m => times n m + n

theorem times_eq_mul (n m) : times n m = n * m := by
  induction m <;> aesop (add simp [times])

It's a bit of a weird tradeoff with no clear best option.

[Jason Rute]

Arguably panics shouldn’t return a predictable value (similar to partial). So then you can’t prove stuff about the panic route.

[Jason Rute]

In other words why do you want to prove theorems like the above one? Wouldn’t you want to prove if m is not 0 then times n m = n * m?

[Jason Rute]

And also, does that flag prevent you from proving that theorem? (And if the issue is that Lean proves the program gives an answer but in practice it crashes, there are lots of ways to have Lean do that without that flag, like external implementations.)

[Kyle Miller]

It's a lot easier to apply that sort of theorem, which helps a lot with formalization. Well-chosen junk values mean you can have unconditional simp lemmas.

[Kyle Miller]

I'm not sure I understand your example @Jannis Limperg, unless the point is "panic! has no logical meaning, it's just default with special runtime support, so beware"

[Jason Rute]

Yeah, why do proofs have anything to do with that flag being on as the default?

[Kyle Miller]

I'm not understanding this claim about the flag having anything to do with proofs

[Jannis Limperg]

The example shows a program, times, that is proven to behave exactly like mul. So if you run this program, arguably it should behave exactly like mul. The LEAN_ABORT_ON_PANIC flag subverts this expectation. That's my understanding of why Leo wanted it off by default.

[Jukka Suomela]

I guess it'd be fairly easy to also write a Lean program that is provably correct but crashes at run time because it tries to allocate gazillion terabytes of memory?

[Jannis Limperg]

FWIW I agree that this mostly produces weird behaviour in practice. But I can see the reason.

[Jason Rute]

Then List.get! Is a major footgun. It behaves like getD, but the user doesn’t realize that. So they are surprised when 0s silently show up in their code, and it is hard to debug, no?

[Jannis Limperg]

Yes, this occasionally happens.

[Jason Rute]

It it panicked by default then that is fine, but otherwise it is a trap.

[Jannis Limperg]

I run the Aesop test suite with LEAN_ABORT_ON_PANIC=1 for this reason, and I think Mathlib also does that.

[Jukka Suomela]

But I really like this perspective. Does a provably correct program/function in the ideal world mean:

1. it always works correctly, full stop
2. if it happens to terminate successfully (and it didn't e.g. run out of memory or panic for a similar reason) it also worked correctly?

[Kyle Miller]

Found the likely comment that told you about Leo's position @Jannis Limperg: #lean4 > add_decl_doc panic loop @ 💬

[Kyle Miller]

(This might be the only documentation about it. The Lean 4 source doesn't have any information about the choice for the default value.)

[Jason Rute]

There isn’t a great match between the semantics of the kernel math and the semantics of the code. It is at best something they try to keep functionally the same, but I don’t think there are any guarantees. A proof in Lean is a proof about the ideal version of the code, not the implementation. @Mario Carneiro complains about this sometimes.

[Jukka Suomela]

Btw, something like lake exe --abort-on-panic foo would be convenient. This kind of a flag would also be visible in lake exe --help, so unlike LEAN_ABORT_ON_PANIC=1 one might accidentally learn about it.

And it would be especially convenient if with this flag lake exe also printed out to stderr at least some basic stuff like "program crashed" when the program crashes so that it doesn't look like everything was silently OK.

This would make some difference especially for programs that don't normally print out anything but just e.g. manipulate some files.

[Jukka Suomela]

I mean writing stuff like LEAN_ABORT_ON_PANIC=1 lake exe foo || echo "something went wrong" gets somewhat tiresome and isn't that intuitive for beginners.

[Mario Carneiro]

Jason Rute said:

There isn’t a great match between the semantics of the kernel math and the semantics of the code. It is at best something they try to keep functionally the same, but I don’t think there are any guarantees.

There is at least a soft guarantee that the compiled code does not produce different (valid) results from the kernel version of the code, because violation of this leads to proofs of false via native_decide. (This guarantee is invalidated when you use implemented_by or extern, which is the equivalent of axiom for the purpose of compiler correctness, but I believe the devs try to keep the existing implemented_by and extern implementations from violating this property.)

[Mario Carneiro]

But there is no guarantee that the compiled code won't panic while the kernel code doesn't (as indeed it can't panic, that's not a thing in the type theory)

[Mario Carneiro]

From a modeling perspective, panic is just a no-op

[Mario Carneiro]

in particular it does not halt execution (and as observed, it also does not halt execution in normal compiled code either, it just reports an error to some side channel and continues unless you set a certain environment variable)

[Mario Carneiro]

if you want to halt execution you should use exceptions or other mechanisms that play well with the type system

[Mario Carneiro]

Some people will tell you that panic itself was a mistake and you shouldn't use it at all

[Niels Voss]

I could see the argument for this either way. I'm somewhat worried that at some point, someone is going to perform a critical IO action like deleting a folder, without realizing that panic doesn't stop their code, and it will cause a bunch of damage. On the other hand, having panic terminate the program basically breaks the semantics

[Niels Voss]

Maybe we need some way to track which implemented_by or partial function we rely on, in the same way that we track which axioms that are relied on?

[Mario Carneiro]

yeah, I have to remind people often not to treat panic like it early aborts

[Mario Carneiro]

I think it's not well named to give that impression

[Mario Carneiro]

I think it would be useful to have a way to check specifically for uses of panic (and a few other lean runtime functions that also have the effect of a panic, like Array.get!)

[Niels Voss]

The other problem I can see with making it abort early by default is that people will learn to rely on this, and it might be even more likely someone will use it to safeguard dangerous IO

[Niels Voss]

People coming from rust in particular are highly susceptible to this I would imagine

[Mario Carneiro]

I think it would be better to rename it

[Mario Carneiro]

Rust panics absolutely cannot continue to the next line of code

[Mario Carneiro]

they can abort or they can throw

[Niels Voss]

Some programming language have different logging levels like INFO, WARNING, ERROR, FATAL. If the intended behavior of panic is a fatal log, maybe that's what it should be renamed to?

[Mario Carneiro]

but rust panics have a type which amounts to panic : Unit -> False

[Mario Carneiro]

and this is problematic for a logic language

[Mario Carneiro]

fatal also sounds like it stops execution

[Niels Voss]

yeah, that's a problem

[Mario Carneiro]

how about just bug!

[Mario Carneiro]

which is the name for the rustc internal macro for internal compiler errors

[Niels Voss]

That sounds sort of like a temporary statement, even though it isn't

[Niels Voss]

if we rename panic, should we also have an abort! to actually stop execution?

[Mario Carneiro]

the point is that we can't really have that to begin with

[Kyle Miller]

no! or drat! would be a little amusing

[Mario Carneiro]

at least not without bringing back all the flaws that panic! has

[Mario Carneiro]

(it's easy to have this in the IO monad, but the problem is having it in pure code)

[Niels Voss]

well, I think the idea would be that abort! should only be used in areas of the code we don't care about semantics that much, like partial or unsafe

[Niels Voss]

no! or drat! would be a little amusing

What about d'oh!

[Mario Carneiro]

Keep in mind that this is not the entirety of the macro, it's followed by a string literal

[Niels Voss]

Would we also need to rename unreachable!?

[Kyle Miller]

d'oh! "the argument is out of bounds"

[Jukka Suomela]

Just a quick note: even if we set LEAN_ABORT_ON_PANIC=1, the panic message is not shown anywhere or logged anywhere, it seems to be completely lost, right? So this isn't really comparable to "logging" in other programming languages?

[Mario Carneiro]

that seems like a bug

[Mario Carneiro]

in vscode it ends up in the output panel

[Jukka Suomela]

I mean if you run e.g. LEAN_ABORT_ON_PANIC=1 lake exe foo in the terminal, you don't see anything? At least on macOS and Lean 4.14.0?

[Mario Carneiro]

there seems to be a flag to enable

[Niels Voss]

Would it be feasible to create an abort! that only works in partial and unsafe functions? I feel like terminating abruptly fits my conception of a partial function (and in most cases, aborting is probably better than looping forever)

[Mario Carneiro]

but no, the flag seems to be always on during regular code, so it should print to stderr

[Kim Morrison]

I do like the idea of renaming panic!

[Mario Carneiro]

they aren't particularly panicked, just more of a mild concern

[Kim Morrison]

Even something verbose like raise_panic_flag! might be helpful. (Less suggestive that it makes execution? Longer, to discourage people using it?)

[Mario Carneiro]

I don't think it's feasible to get rid of all the ! suffixes though

[Niels Voss]

even something like raise! is probably better than panic!

[Mario Carneiro]

nope, that one also sounds like non-local control flow

[Kim Morrison]

In any case, certainly the doc-string for panic! should mention LEAN_ABORT_ON_PANIC.

[Niels Voss]

oh, that's fair

[Mario Carneiro]

it does, although maybe not with that capitalization

[Niels Voss]

if panic! is renamed, would this mean getting rid of LEAN_ABORT_ON_PANIC?
If not, I'm not sure it will be easy to find a word that means "Possibly abort, but also possibly just log an error"

[Jukka Suomela]

Mario Carneiro said:

but no, the flag seems to be always on during regular code, so it should print to stderr

Sorry, do you mean that the message is visible currently and I'm doing something wrong if I'm not seeing it?

Or do you mean that there is a bug but the intended behavior is that the message would get printed to stderr?

[Mario Carneiro]

it seems the intended behavior is to print to stderr, and from what I can tell it is going through the motions

[Mario Carneiro]

I have not tested the code

[Mario Carneiro]

does it work if you pass lean -e?

[Mario Carneiro]

this uses a slightly different code path but should be the same as LEAN_ABORT_ON_PANIC

[Jukka Suomela]

Here is a very simple example that reproduces it for me:

def foo : Nat := Id.run do
  panic! "bad bad bad"

def main : IO Unit := do
  let r := foo
  IO.println s!"all well, got result {r}"

Running lake exe foo in the terminal gives "all well, got result 0".

And running LEAN_ABORT_ON_PANIC=1 lake exe foo in the terminal gives nothing (which was surprising to me), but the program crashes with a non-zero error code (which is of course good and intended here).

[Jukka Suomela]

@Mario Carneiro If I add #eval main in the end of the file, and then run it with lean -e, I can see the panic error message. Is this what you meant? I don't really know how to use lean -e to properly run a full Lean program (comparable to lake exe)?

[Mario Carneiro]

yes, I'm starting to suspect the issue has to do with the fact that you aren't using lean

[Jukka Suomela]

Oh, I didn't know I'm doing something wrong or unusual. :)

Isn't lake the right frontend for everything? It's after all using lean to generate C code, etc.?

[Mario Carneiro]

not wrong, there are simply multiple ways to run lean code and panic messages go in different directions depending

[Mario Carneiro]

the point here is that you are building a standalone program and running it, rather than panicking in the elaborator (e.g. via #eval)

[Jukka Suomela]

Yes, I do usually see panic messages and all kinds of useful stuff if I do quick interactive experiments by adding #eval in VS Code and looking at Lean Infoview.

[Mario Carneiro]

oh! it's panicking during initialization due to closed term extraction

[Mario Carneiro]

this is lean#1965

[Mario Carneiro]

error messages are masked during initialization

[Mario Carneiro]

to fix it you need to make your panic message not constant

[Jukka Suomela]

It also happens with e.g. this, where I guess the problem is the same (get! uses a fixed error message)?

def foo : Nat := Id.run do
  Array.mkArray0.get! 123

def main : IO Unit := do
  let r := foo
  IO.println s!"all well, got result {r}"

[Mario Carneiro]

no, here the issue is that the entire computation of foo happens at initialization time

[Mario Carneiro]

because foo is a constant

[Jukka Suomela]

Oh I see, makes sense.

[Mario Carneiro]

I tried setting set_option compiler.extract_closed false which should help but it's apparently not enough when you have global constants like foo

[Mario Carneiro]

if you make foo (_ : Unit) : Nat then it will finally output a message

[Jukka Suomela]

No, that's not enough, or at least this doesn't fix it:

def foo (_ : Unit) : Nat := Id.run do
  Array.mkArray0.get! 123

def main : IO Unit := do
  let r := foo ()
  IO.println s!"all well, got result {r}"

[Mario Carneiro]

you also need the extract_closed option

[Jukka Suomela]

Oh, right, got it!

[Jukka Suomela]

So stuff like this is apparently enough to get error messages:

set_option compiler.extract_closed false

def foo (_ : Unit) : Nat := Id.run do
  Array.mkArray0.get! 123

def main : IO Unit := do
  let r := foo ()
  IO.println s!"all well, got result {r}"

[Jukka Suomela]

@Mario Carneiro Exactly what does compiler.extract_closed do? I've got a program with this behavior:

• Seems to work fine with lake exe
• Crashes with no message with LEAN_ABORT_ON_PANIC=1 lake exe
• Seems to work fine with set_option compiler.extract_closed false + LEAN_ABORT_ON_PANIC=1 lake exe

[Mario Carneiro]

extract_closed is an optimization the compiler performs to move all closed subterms into top level definitions, which are calculated at initialization time. lean#1965 is the bug that this process occurs even to closed subterms which contain panic!, meaning that the code will panic (and abort if you have the appropriate setting) at initialization time, even if the code it was extracted from is never called. So it can cause a perfectly well defined program to crash. (This crash also occurs at initialization time, which is why there is no message.)