panic!

Stream: lean4

[Reid Barton]

Is it possible to get #eval of a panic! to produce an error or something?

[Mario Carneiro]

it does produce an error

[Mario Carneiro]

it goes in the output view / you get a popup

[Arthur Paulino]

I don't get a popup with this:

def AAA : Nat := panic! "AAA!"
#eval AAA -- 0

[Reid Barton]

I'm not exactly sure where I should look for it in emacs, but I don't see an error anywhere obvious

[Mario Carneiro]

in vscode when I paste that in a new file I get a popup "Lean server printed an error: PANIC at AAA Test:1:17: AAA! backtrace:" with a button "show stderr output" that opens the output panel containing a backtrace

[Arthur Paulino]

I recall seeing this popup once in VS Code :thinking: No idea about emacs though. But this is looking like a #xy question

[Mario Carneiro]

That said, #eval already intercepts stdout writes to turn them into diagnostics, it would make sense to also intercept panics and turn them into error diagnostics

[Mario Carneiro]

that would require some runtime support though, currently panics are logged to stderr and then forgotten, so the server has no way to know that it even happened - it may as well be a panic in the server itself

[Reid Barton]

I'm not sure what would be the xy; I have code that uses assert! to assert invariants and I would like to test it with #eval

[Mario Carneiro]

lack of effective panic reporting on emacs is definitely an issue

[Mario Carneiro]

but I don't know anything about emacs mode so I can't speak to that

[Mario Carneiro]

I recall they used to be reported in more normal places and it was toned down because it was too disruptive

[Reid Barton]

I still find it extremely weird that the program keeps running after a failing assert!

[Reid Barton]

maybe I should be using some other kind of assert!!?

[Mario Carneiro]

do you want it to take down the server?

[Mario Carneiro]

What happens if you call False.rec? The program surely can't continue after that

[Mario Carneiro]

oh yeah, that's what I'm talking about...

unsafe def myPanic!! (s : String) : α :=
  Empty.rec (let _ : Inhabited Empty := ⟨False.elim lcProof⟩; panic! s)
unsafe def AAA : Nat := myPanic!! "AAA!"
#eval AAA -- server crash

(don't try this at home)

[Reid Barton]

axiom f : False

def myAssert (b : Bool) : Int :=
  if b then 7 else f.elim

#eval myAssert false            -- 7 !

[Mario Carneiro]

yeah, this is obviously not reliable since it's using UB and lean will optimize away branches leading to False.rec

[Reid Barton]

In Haskell error just raises an (imprecise) exception, and ghci will catch and report it

[Mario Carneiro]

yeah we've talked about catching panics in other threads, it adds a lot of complexity to the runtime

[Mario Carneiro]

in lean BaseIO can't throw exceptions at all, that's all layered on in IO which is using the except monad

[Mario Carneiro]

which kind of precludes throwing IO exceptions from pure code

[Mario Carneiro]

I think you could have a primitive like catchPanic : BaseIO A -> BaseIO (Except String A) though which catches any panics caused by the input (pure) code (so it's not really an IO exception but essentially plays the same role as one)

[Reid Barton]

I would think at the least you could kill the thread in a controlled way, and collect the exception from the parent thread

[Mario Carneiro]

it's not a thread, it's running on the main thread IIRC

[Reid Barton]

Well, that can be changed presumably?

[Mario Carneiro]

we probably don't want to do that for every use of evalConst

[Reid Barton]

I don't know what evalConst is but I'm sure it can be done for every #eval in the source code at least

[Reid Barton]

Are threads that expensive? In GHC it's pretty reasonable to create a million threads say

[Mario Carneiro]

there are some other cases where code is run at compile time for an input expression, for example what should by simp (config := panic! "") do?

[Mario Carneiro]

lean's threading mechanism is built around tasks which are on a threadpool. They are relatively cheap, but I don't know how complicated it would be to abort them

[Reid Barton]

rwbarton@operad:/tmp$ ghci -XTemplateHaskell
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
Prelude> $( error "hi" )

<interactive>:1:1: error:
    • Exception when trying to run compile-time code:
        hi
CallStack (from HasCallStack):
  error, called at <interactive>:1:4 in interactive:Ghci1
      Code: error "hi"
    • In the untyped splice: $(error "hi")
Prelude>

[Reid Barton]

For sure these kinds of issues are not high priority though.

[Arthur Paulino]

As an annoying workaround, the assert!' idea isn't too bad. You can make it print the message with dbg_trace and then manually panic! with the same message

[Mario Carneiro]

that doesn't solve the issue that the code continues despite the assertion failure though

[Mario Carneiro]

hm, what happens if you print to stderr inside #eval?

[Mario Carneiro]

it appears to be indistinguishable from regular print

#eval IO.eprintln "hi" -- hi

[Sebastian Ullrich]

There's an old TODO for capturing panics during #eval like we do for stderr/out: https://github.com/leanprover/lean4/blob/10d2403e8330d4a5d9539daed77dc30783589870/src/runtime/object.cpp#L100

[Michael Wahlberg]

How do we use nomatch tactic?

[Arthur Paulino]

@Michael Wahlberg I think your question is on the wrong thread. Do you want to start a new thread?