Lean error codes (e.g. code 139)

Stream: lean4

[Andrés Goens]

Is there any reference to read what error codes mean? I'm getting a crash with just some error code (139) and it doesn't really tell me much more of what's going on:

error: external command `/home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/lean` exited with code 139

Rather than asking what 139 is specifically, I thought it might be worth asking how I can figure these things out on my own (didn't seem to find a thread asking about them in general)

[Kevin Buzzard]

Here's yesterday's "what does error code 139 mean?" question: https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/435877290

[Andrés Goens]

Kevin Buzzard said:

Here's yesterday's "what does error code 139 mean?" question: https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/435877290

seems to also be unanswered

[Matthew Ballard]

GPT says segfault (but perhaps that is already know to everyone here. New to me)

[Michael Stoll]

Maybe related to this...

[Andrés Goens]

FWIW my error was on a file that was not importing Mathlib (I've fixed it now, it was because I was using builtin_initalize and not initalize), but I guess I want to know how to deal with these error codes in general in the future :)

[Richard Copley]

I imagine it's 11 (SIGSEGV) with bit 7 set by something else to indicate that it's a signal rather than an error code.

[Richard Copley]

Probably by this.

[Julian Berman]

For most programs/languages it's usually but not always that yeah (a seg fault, and the error code is 128 + the real error code, with 11 being SIGSEGV).
@Andrés Goens is your error reproducible? If so you can try enabling crash reports and then that may contain something helpful to someone on the dev team.

[Julian Berman]

It depends a bit on your Linux distribution where/how to do that, but ulimit -S -c unlimited is usually involved to actually make them be written out, and then we can go find where they end up on your machine.

[Richard Copley]

@Mac Malone, would it be useful to change the message from Lake?

diff

diff --git a/src/lake/Lake/Util/Proc.lean b/src/lake/Lake/Util/Proc.lean
index 01239c7c53..ff77c9b91c 100644
--- a/src/lake/Lake/Util/Proc.lean
+++ b/src/lake/Lake/Util/Proc.lean
@@ -35,6 +35,9 @@ def proc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO Unit := do
   | .ok out =>
     if out.exitCode = 0 then
       logProcWith args out logVerbose (logOutput := if quiet then logVerbose else logInfo)
+    else if 128 <= out.exitCode then
+      logProcWith args out logError
+      error s!"external command `{args.cmd}` died with signal {out.exitCode - 128}"
     else
       logProcWith args out logError
       error s!"external command `{args.cmd}` exited with code {out.exitCode}"
@@ -46,6 +49,9 @@ def captureProc (args : IO.Process.SpawnArgs) : LogIO String := do
   | .ok out =>
     if out.exitCode = 0 then
       return out.stdout.trim -- remove, e.g., newline at end
+    else if 128 <= out.exitCode then
+      logProcWith args out logError
+      error s!"external command `{args.cmd}` died with signal {out.exitCode - 128}"
     else
       logProcWith args out logError
       error s!"external command `{args.cmd}` exited with code {out.exitCode}"

[Richard Copley]

I suppose not. It assumes the child is Lean, Bash, Perl or something that uses the same convention.

[Julian Berman]

I suspect that also will get wrong if someone actually intentionally exits with an exit code > 128 for whatever reason.

[Andrés Goens]

Julian Berman said:

For most programs/languages it's usually but not always that yeah (a seg fault, and the error code is 128 + the real error code, with 11 being SIGSEGV).
Andrés Goens is your error reproducible? If so you can try enabling crash reports and then that may contain something helpful to someone on the dev team.

@Julian Berman yep it's reproducible! Happy to do that, how do I enable crash reports?

[Julian Berman]

That's that ulimit -c unlimited line I shared -- and then I forget if systemd is responsible for where those go at this point or not -- but share what distro you're on and we can look.

[Julian Berman]

Er, to be more explicit -- run that ulimit line, and then make sure you run lean and/or lake in the same exact shell as you ran that in.

[Andrés Goens]

Hm, I guess it's not a stack overflow? it returns the same error and doesn't dump a core nor anything

[Andrés Goens]

(I'm on nixos)

[Richard Copley]

Perhaps a null (or otherwise bad) pointer dereference, then.

[Richard Copley]

Or (more likely?) an out-of-bounds array index

[Andrés Goens]

FWIW, valgrind doesn't seem to find anything strange either

[Richard Copley]

I'd suggest doing lake --verbose to find the command line of the process that crashed, then running that command in your debugger to get a backtrace.

[Andrés Goens]

oh interesting, apparently it was segfaulting, but the indirection through lake was suppressing the segfault message :/ I did get a backtrace now:

backtrace

program terminated with signal SIGSEGV, Segmentation fault.
#0 0x00007fa9fd20b4ca in lean_mark_persistent () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
(gdb) bt
#0 0x00007fa9fd20b4ca in lean_mark_persistent () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#1 0x00007fa9f7c3fef6 in initialize_Egg_Tactic_Tags () from ./.lake/build/lib/libEgg-Tactic-Tags-1.so
#2 0x00007fa9fd1fc028 in lean_run_mod_init () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#3 0x00007fa9fa70dd1c in l_Array_forInUnsafe_loop___at_Lean_registerInitAttrUnsafe___spec__22 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#4 0x00007fa9fa71157f in l_Lean_registerInitAttrUnsafe___lambda__3 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#5 0x00007fa9fd21775a in lean_apply_3 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#6 0x00007fa9fa228bd6 in l_Lean_registerParametricAttribute___rarg___lambda__1 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#7 0x00007fa9fd217798 in lean_apply_3 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#8 0x00007fa9fa6e49bf in l___private_Lean_Environment_0__Lean_finalizePersistentExtensions_loop () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#9 0x00007fa9fa6ee0ba in l_Lean_finalizeImport___lambda__2 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#10 0x00007fa9fd21636e in lean_apply_2 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#11 0x00007fa9fd21559d in lean_apply_1 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#12 0x00007fa9fbb57463 in l_Lean_withImporting___rarg () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#13 0x00007fa9fa6efbea in l_Lean_importModules___lambda__2___boxed () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#14 0x00007fa9fd21636e in lean_apply_2 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#15 0x00007fa9fd21559d in lean_apply_1 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#16 0x00007fa9fcffa71e in l_Lean_profileitIOUnsafe___rarg___lambda__1 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#17 0x00007fa9fcffa91f in l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#18 0x00007fa9fd215589 in lean_apply_1 () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#19 0x00007fa9fd15cbc4 in lean_profileit () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#20 0x00007fa9fcffa840 in l_Lean_profileitIOUnsafe___rarg () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#21 0x00007fa9fa6efa7d in lean_import_modules () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#22 0x00007fa9fc7d8f9e in l_Lean_Elab_processHeader () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#23 0x00007fa9fc1750d8 in lean_run_frontend () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#24 0x00007fa9fd0f754d in lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> > > const&) ()
from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#25 0x00007fa9fd0f9f9f in lean_main () from /home/goens/.elan/toolchains/leanprover--lean4---v4.7.0/bin/../lib/lean/libleanshared.so
#26 0x00007fa9f923efce in __libc_start_call_main () from /nix/store/1zy01hjzwvvia6h9dq5xar88v77fgh9x-glibc-2.38-44/lib/libc.so.6
#27 0x00007fa9f923f089 in __libc_start_main_impl () from /nix/store/1zy01hjzwvvia6h9dq5xar88v77fgh9x-glibc-2.38-44/lib/libc.so.6
#28 0x000055dda6d33775 in _start ()

[Kevin Buzzard]

Thanks for taking the time!

[Kevin Buzzard]

BTW is it related to this ?

[Kyle Miller]

Lean core developers are looking into that issue. There's a chance it will be fixed by lean4#4028

[Amos Turchet]

Got same problem by just doing lake exe cache get

[Kim Morrison]

Unfortunately lean4#4028 hasn't fixed the earlier issue. We're still looking.