feat: print panic backtraces on Linux

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.

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);

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.