`panic`ing in the interpreter

[leodemoura]

@Kha when panic is evaluated by the interpreter, the execution is interrupted as expected. However, all trace messages produced using dbgTrace are lost because the #eval command implementation redirects stdout to a buffer. Not sure what the best fix is. Here are some alternatives: 1- We register finalizers for panic. Then, #eval can set a finalizer that just dumps any intermediate output to stdout before terminating the execution. 2- We throw a C++ exception at panic instead of aborting. We will leak memory, but #eval will be able to dump the output as trace messages, and then terminate the Lean process with a panic message. 3- We don't change panic, but the interpreter intercepts it and uses a different implementation. Example: store error message, and continue the execution with the "arbitrary" element. Pro: no leaks. Cons: the computation is nonsense after the first panic, and it may diverge.

[leodemoura]

In the meantime, I added at catch at eval_cmd and used the fact that lean_unreachable throws an exception in release mode: https://github.com/leanprover/lean4/blob/master/src/runtime/object.cpp#L26

[leodemoura]

Here is a related issue: if a deep recursion is detected by the interpreter, all messages generated using dbgTrace are lost.

[Kha]

3. doesn't work if the panic/deep recursion is inside compiled C code invoked by the interpreter. This should be an issue for 2) as well - throwing C++ exceptions through C code isn't well-defined without -fexceptions, which we might not want to pay for.

[Kha]

We could of course claim that #eval is mostly for debugging and deactivate jumping into C code except for externs. In that case, shouldn't it at least theoretically be possible to switch to a different interpretation mode that correctly frees all resources by continuing to execute the RC semantics (inc, dec, consume owned arguments, ...) but skipping the pure semantics (actually doing function calls (so we terminate relatively quickly), ...)?

[leodemoura]

3. doesn't work if the panic/deep recursion is inside compiled C code invoked by the interpreter. This should be an issue for 2) as well - throwing C++ exceptions through C code isn't well-defined without -fexceptions, which we might not want to pay for.

We could you longjmp instead of exceptions to avoid -fexceptions, but we would still have the thread problem. Example: suppose interpreter calls compiled C function which is using tasks and the panic is in a different thread.

[leodemoura]

We could of course claim that #eval is mostly for debugging and deactivate jumping into C code except for externs. In that case, shouldn't it at least theoretically be possible to switch to a different interpretation mode that correctly frees all resources by continuing to execute the RC semantics (inc, dec, consume owned arguments, ...) but skipping the pure semantics (actually doing function calls (so we terminate relatively quickly), ...)?

BTW, it would not solve my original problem. The panic occurred into a primitive C function. https://github.com/leanprover/lean4/blob/master/src/kernel/instantiate.cpp#L302

I could try to move all checking and panic invocations to Lean before we invoke the extern functions. That being said, even if we make this modification, I am not sure I am willing to pay the price of not using compiled code to fix this problem.

[leodemoura]

Here is another alternative. #eval behaves differently in server and batch mode. In server mode, we use the current implementation which redirects stdout. In batch mode, we don't redirect. It feels quite reasonable to me. In Emacs or VSCode, Lean-mode would inform us that the #eval panicked, and that batch mode should be used to inspect any intermediate result.

[leodemoura]

The proposal in my last comment would only work for dbgTrace and IO.println. Messages sent using the tracing framework would be lost. We can only "view" these messages if #eval terminates without panicking. So, here is yet another proposal.

• We add a global flag to configure panic.
• The default behavior is to terminate the execution.
• In server mode, we disable default behavior and make it return the inhabitant. https://github.com/leanprover/lean4/blob/master/library/Init/Util.lean#L29 That is, the primitive implementation would take 2 arguments instead of 1.

[Kha]

The panic occurred into a primitive C function.

I see.

In server mode, we disable default behavior and make it return the inhabitant.

I'm really wary about this, especially if IO is involved. The finalizers proposal seems 100% cleaner to me; are there any disadvantages to that one, apart from a bit more implementation overhead?

[Kha]

Oh, do you mean Init.Lean.Trace? If we have monadIO m, should a MonadTracer m print out traces immediately as well if trace.as_messages (or some new option) is not set?

[leodemoura]

I'm really wary about this, especially if IO is involved.

Yes, I agree.

The finalizers proposal seems 100% cleaner to me; are there any disadvantages to that one, apart from a bit more implementation overhead?

Let's go with the finalizers. The only disadvantage is that we lose the messages produced using MonadTracer m.

[leodemoura]

Oh, do you mean Init.Lean.Trace? If we have monadIO m, should a MonadTracer m print out traces immediately as well if trace.as_messages (or some new option) is not set?

It would minimize the problem, but it would not solve it completely. For example, we have MonadTracer MetaM, but we don't have MonadIO MetaM. We could try to use unsafeIO in this case.