lean_sys/
panic.rs

1use crate::{
2    lean_box, lean_mk_string_from_bytes, lean_panic_fn, lean_set_exit_on_panic,
3    lean_set_panic_messages,
4};
5
6/// A panic handler implementation. This is useful when
7/// writing FFI libraries for Lean, where people may want to disable rust's `std`.
8/// ```ignore
9/// #![no_std]
10/// #[panic_handler]
11/// fn panic(info: &core::panic::PanicInfo) -> ! {
12///    lean_sys::panic::panic_handler(info)
13/// }
14/// ```
15pub fn panic_handler(info: &core::panic::PanicInfo) -> ! {
16    #[allow(deprecated)] // the payload() function always returns None
17    let message = if let Some(s) = info.payload().downcast_ref::<&str>() {
18        s.as_bytes()
19    } else {
20        b"panic inside Rust FFI, no message available"
21    };
22    unsafe {
23        let string = lean_mk_string_from_bytes(message.as_ptr(), message.len());
24        loop {
25            lean_set_panic_messages(true);
26            lean_set_exit_on_panic(true);
27            lean_panic_fn(lean_box(0), string);
28        }
29    }
30}