max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: output panics into Lean's redirected stderr (#4952)

Browse source 
...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
This commit is contained in:
Sebastian Ullrich 2024-08-12 14:15:15 +02:00 • committed by GitHub
parent c5114c971a
commit dd4e26f247
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 30 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/runtime/object.cpp
View file

@ -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

2
tests/lean/run/structure.lean
View file

@ -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]