From dd4e26f24760ca847578d2a4e08ad30b82291c56 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 12 Aug 2024 14:15:15 +0200
Subject: [PATCH] feat: output panics into Lean's redirected stderr (#4952)

...unless we are about to kill the process anyway (which is not the
default)

Ensures panics are visible as regular messages in the language server
and properly ordered in relation to other messages on the cmdline
---
 src/runtime/object.cpp        | 40 ++++++++++++++++++++++++++---------
 tests/lean/run/structure.lean |  2 --
 2 files changed, 30 insertions(+), 12 deletions(-)

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 1d2a74c765..06128fafe5 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -46,12 +46,18 @@ Author: Leonardo de Moura
 
 namespace lean {
 
+static bool should_abort_on_panic() {
+#ifdef LEAN_EMSCRIPTEN
+    return false;
+#else
+    return std::getenv("LEAN_ABORT_ON_PANIC");
+#endif
+}
+
 static void abort_on_panic() {
-#ifndef LEAN_EMSCRIPTEN
-    if (std::getenv("LEAN_ABORT_ON_PANIC")) {
+    if (should_abort_on_panic()) {
         abort();
     }
-#endif
 }
 
 extern "C" LEAN_EXPORT void lean_internal_panic(char const * msg) {
@@ -83,27 +89,41 @@ extern "C" LEAN_EXPORT void lean_set_panic_messages(bool flag) {
     g_panic_messages = flag;
 }
 
+static void panic_eprintln(char const * line) {
+    if (g_exit_on_panic || should_abort_on_panic()) {
+        // If we are about to kill the process, we should skip the Lean stderr buffer
+        std::cerr << line << "\n";
+    } else {
+        io_eprintln(lean_mk_string(line));
+    }
+}
+
 static void print_backtrace() {
 #ifdef __GLIBC__
     void * bt_buf[100];
     int nptrs = backtrace(bt_buf, sizeof(bt_buf) / sizeof(void *));
-    backtrace_symbols_fd(bt_buf, nptrs, STDERR_FILENO);
-    if (nptrs == sizeof(bt_buf)) {
-        std::cerr << "...\n";
+    if (char ** symbols = backtrace_symbols(bt_buf, nptrs)) {
+        for (int i = 0; i < nptrs; i++) {
+            panic_eprintln(symbols[i]);
+        }
+        // According to `man backtrace`, each `symbols[i]` should NOT be freed
+        free(symbols);
+        if (nptrs == sizeof(bt_buf)) {
+            panic_eprintln("...");
+        }
     }
 #else
-    std::cerr << "(stack trace unavailable)\n";
+    panic_eprintln("(stack trace unavailable)");
 #endif
 }
 
 extern "C" LEAN_EXPORT object * lean_panic_fn(object * default_val, object * msg) {
-    // TODO(Leo, Kha): add thread local buffer for interpreter.
     if (g_panic_messages) {
-        std::cerr << lean_string_cstr(msg) << "\n";
+        panic_eprintln(lean_string_cstr(msg));
 #ifdef __GLIBC__
         char * bt_env = getenv("LEAN_BACKTRACE");
         if (!bt_env || strcmp(bt_env, "0") != 0) {
-            std::cerr << "backtrace:\n";
+            panic_eprintln("backtrace:");
             print_backtrace();
         }
 #endif
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index 8ee536e3ea..5ed24f9719 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -40,7 +40,6 @@ do let env ← getEnv
    check $ !isStructure env `Nat
    check $ !isStructure env `D
    IO.println (getStructureFieldsFlattened env `S4)
-   IO.println (getStructureFields env `D)
    IO.println (getPathToBaseStructure? env `S1 `S4)
    IO.println (getParentStructures env `S4)
    IO.println (getAllParentStructures env `S4)
@@ -50,7 +49,6 @@ do let env ← getEnv
 /--
 info: #[const2ModIdx, constants, extensions, extraConstNames, header]
 #[toS2, toS1, x, y, z, toS3, w, s]
-#[]
 (some [S4.toS2, S2.toS1])
 #[S2, S3]
 #[S2, S1, S3]