From c8fb72195b852a48090a9a95663da5fc32ac0dd5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 28 Jun 2022 13:47:34 +0200
Subject: [PATCH] feat: print panic backtraces on Linux

---
 RELEASES.md            |  3 +++
 src/runtime/object.cpp | 18 ++++++++++++++++++
 tests/common.sh        |  2 +-
 3 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/RELEASES.md b/RELEASES.md
index 1444d94e5a..9f9f4a1de5 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,9 @@
 Unreleased
 ---------
 
+* On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable `LEAN_BACKTRACE` to `0`.
+  Other platforms are TBD.
+
 * The `group(·)` `syntax` combinator is now introduced automatically where necessary, such as when using multiple parsers inside `(...)+`.
 
 * Add ["Typed Macros"](https://github.com/leanprover/lean4/pull/1251): syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit `:kind` antiquotation annotations. See PR for details.
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 77ff85853c..2c7dfd2119 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -20,6 +20,11 @@ Author: Leonardo de Moura
 #include "runtime/interrupt.h"
 #include "runtime/buffer.h"
 
+#ifdef __GLIBC__
+#include <execinfo.h>
+#include <unistd.h>
+#endif
+
 // see `Task.Priority.max`
 #define LEAN_MAX_PRIO 8
 
@@ -66,7 +71,20 @@ 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";
+#ifdef __GLIBC__
+        char * bt_env = getenv("LEAN_BACKTRACE");
+        if (!bt_env || strcmp(bt_env, "0") != 0) {
+            std::cerr << "backtrace:\n";
+            void * bt_buf[100];
+            int nptrs = backtrace(bt_buf, sizeof(bt_buf));
+            backtrace_symbols_fd(bt_buf, nptrs, STDERR_FILENO);
+            if (nptrs == sizeof(bt_buf)) {
+                std::cerr << "...\n";
+            }
+        }
+#endif
     }
+
     abort_on_panic();
     if (g_exit_on_panic) {
         std::exit(1);
diff --git a/tests/common.sh b/tests/common.sh
index 0eb7442bf3..990ac52bf3 100644
--- a/tests/common.sh
+++ b/tests/common.sh
@@ -28,7 +28,7 @@ function compile_lean {
 function exec_capture {
     # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
     # also strip intermittent "building '/nix/store/..." messages
-    "$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
+    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
 }
 
 # Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.