-
Notifications
You must be signed in to change notification settings - Fork 23
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Connected Lean 3 LSP often segfaults #203
Comments
How do you enable core dumps? |
It depends a bit on your distro -- you can typically run |
Here is the crash dump backtrace. I havent used Reading symbols from lean...
(No debugging symbols found in lean)
[New LWP 24507]
[New LWP 24504]
[New LWP 24516]
[New LWP 24513]
[New LWP 24508]
[New LWP 24509]
[New LWP 24365]
[New LWP 24519]
[New LWP 24367]
[New LWP 24506]
[New LWP 24515]
[New LWP 24512]
[New LWP 24511]
[New LWP 24366]
[New LWP 24514]
[New LWP 24510]
[New LWP 24517]
[New LWP 24505]
[New LWP 24518]
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/usr/lib64/libthread_db.so.1".
Core was generated by `lean --server -M 4096 -T 100000 */root/psyoz1/local/G400*'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0 0x000055dcc2f3a065 in lean::sexpr::get_int() const ()
[Current thread is 1 (Thread 0x7f24950ba640 (LWP 24507))]
(gdb) bt
#0 0x000055dcc2f3a065 in lean::sexpr::get_int() const ()
#1 0x000055dcc2f3af8c in lean::to_int(lean::sexpr const&) ()
#2 0x000055dcc2f41ab3 in lean::format::sexpr_kind(lean::sexpr const&) ()
#3 0x000055dcc2f4096f in lean::format::pretty(std::ostream&, unsigned int, bool, lean::format const&) ()
#4 0x000055dcc2f40d65 in lean::pretty(std::ostream&, unsigned int, bool, lean::format const&) ()
#5 0x000055dcc2f40dde in lean::pretty(std::ostream&, lean::options const&, lean::format const&) ()
#6 0x000055dcc2f40e41 in lean::operator<<(std::ostream&, std::pair<lean::format const&, lean::options const&> const&) ()
#7 0x000055dcc330e7f9 in lean::vm_obj_format_info::report(lean::io_state_stream const&, nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long, unsigned long, double, std::allocator>&) const ()
#8 0x000055dcc3312617 in lean::info_data::report(lean::io_state_stream const&, nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long, unsigned long, double, std::allocator>&) const ()
#9 0x000055dcc3310beb in lean::info_manager::get_info_record(lean::environment const&, lean::options const&, lean::io_state const&, std::pair<unsigned int, unsigned int>, nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long, unsigned long, double, std::allocator>&, std::function<bool (lean::info_data const&)>) const ()
#10 0x000055dcc3320691 in lean::report_info(lean::environment const&, lean::options const&, lean::io_state const&, std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, lean::module_info const&, std::vector<lean::info_manager, std::allocator<lean::info_manager> > const&, std::pair<unsigned int, unsigned int> const&, lean::break_at_pos_exception const&, nlohmann::basic_json<std::map, std::vector, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, bool, long, unsigned long, double, std::allocator>&) ()
#11 0x000055dcc2ee52aa in lean::server::info[abi:cxx11](std::shared_ptr<lean::module_info const> const&, std::pair<unsigned int, unsigned int> const&) ()
#12 0x000055dcc2ee5f9a in ?? ()
#13 0x000055dcc2ee9452 in ?? ()
#14 0x000055dcc2ee9dd4 in lean::delegating_task_imp::execute(void*) ()
#15 0x000055dcc30634d1 in lean::library_scopes_imp::execute(void*) ()
#16 0x000055dcc2f25cba in lean::cancellable_task_imp::execute(void*) ()
#17 0x000055dcc2f05256 in lean::task_cell<lean::server::cmd_res>::execute() ()
#18 0x000055dcc2f253e5 in lean::task_queue::execute(std::shared_ptr<lean::gtask_cell> const&) ()
#19 0x000055dcc3056cba in ?? ()
#20 0x000055dcc30590da in ?? ()
#21 0x000055dcc3058fd9 in ?? ()
#22 0x000055dcc3058e87 in ?? ()
#23 0x000055dcc2f1de8c in std::function<void ()>::operator()() const ()
#24 0x000055dcc2f1d025 in ?? ()
#25 0x000055dcc2f1d692 in ?? ()
#26 0x000055dcc2f1d591 in ?? ()
#27 0x000055dcc2f1d46c in ?? ()
#28 0x000055dcc2f1de8c in std::function<void ()>::operator()() const ()
#29 0x000055dcc2f1cf71 in ?? ()
#30 0x000055dcc2f1d857 in lean::lthread::imp::_main(void*) ()
#31 0x00007f2496292eae in start_thread (arg=0x7f24950ba640) at pthread_create.c:463
#32 0x00007f24961c22ff in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:95
(gdb) i threads
Id Target Id Frame
* 1 Thread 0x7f24950ba640 (LWP 24507) 0x000055dcc2f3a065 in lean::sexpr::get_int() const ()
2 Thread 0x7f2484ff9640 (LWP 24504) 0x000055dcc2f472a7 in bool __gnu_cxx::operator< <std::pair<lean::sexpr, unsigned int>*, std::vector<std::pair<lean::sexpr, unsigned int>, std::allocator<std::pair<lean::sexpr, unsigned int> > > >(__gnu_cxx::__normal_iterator<std::pair<lean::sexpr, unsigned int>*, std::vector<std::pair<lean::sexpr, unsigned int>, std::allocator<std::pair<lean::sexpr, unsigned int> > > > const&, __gnu_cxx::__normal_iterator<std::pair<lean::sexpr, unsigned int>*, std::vector<std::pair<lean::sexpr, unsigned int>, std::allocator<std::pair<lean::sexpr, unsigned int> > > > const&) ()
3 Thread 0x7f24777fe640 (LWP 24516) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24777fd460, clockid=2004865936, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
4 Thread 0x7f2485ffb640 (LWP 24513) __getrusage (who=RUSAGE_SELF, usage=0x7f2485ff54d0) at ../sysdeps/unix/sysv/linux/getrusage.c:29
5 Thread 0x7f24757fa640 (LWP 24508) 0x000055dcc2ecb5fa in lean::name::hash() const ()
6 Thread 0x7f2487fff640 (LWP 24509) futex_abstimed_wait_cancelable (private=0, abstime=0x7f2487ffe460, clockid=-2013273200, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
7 Thread 0x7f24960bfe40 (LWP 24365) __GI___libc_read (nbytes=4096, buf=0x55dcc44265d0, fd=0) at ../sysdeps/unix/sysv/linux/read.c:26
8 Thread 0x7f2475ffb640 (LWP 24519) futex_abstimed_wait_cancelable (private=0, abstime=0x7f2475ffa460, clockid=1979687824, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
9 Thread 0x7f24958bb640 (LWP 24367) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24958ba3f0, clockid=-1786010848, expected=0, futex_word=0x55dcc4425e90)
at ../sysdeps/nptl/futex-internal.h:320
10 Thread 0x7f2443fff640 (LWP 24506) futex_abstimed_wait_cancelable (private=0, abstime=0x7f2443ffe460, clockid=1140843408, expected=0, futex_word=0x55dcc44261e4)
at ../sysdeps/nptl/futex-internal.h:320
11 Thread 0x7f2477fff640 (LWP 24515) 0x000055dcc2ecaeab in operator new(unsigned long, void*) ()
12 Thread 0x7f24867fc640 (LWP 24512) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24867fb460, clockid=-2038451312, expected=0, futex_word=0x55dcc44261e4)
at ../sysdeps/nptl/futex-internal.h:320
13 Thread 0x7f2486ffd640 (LWP 24511) futex_abstimed_wait_cancelable (private=0, abstime=0x7f2486ffc460, clockid=-2030058608, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
14 Thread 0x7f24960bc640 (LWP 24366) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24960bb3f0, clockid=-1777618144, expected=0, futex_word=0x55dcc43b6764)
at ../sysdeps/nptl/futex-internal.h:320
15 Thread 0x7f24857fa640 (LWP 24514) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24857f9460, clockid=-2055236720, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
16 Thread 0x7f24877fe640 (LWP 24510) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24877fd460, clockid=-2021665904, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
17 Thread 0x7f2476ffd640 (LWP 24517) futex_abstimed_wait_cancelable (private=0, abstime=0x7f2476ffc460, clockid=1996473232, expected=0, futex_word=0x55dcc44261e4)
at ../sysdeps/nptl/futex-internal.h:320
18 Thread 0x7f24948b9640 (LWP 24505) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24948b8460, clockid=-1802796144, expected=0, futex_word=0x55dcc44261e0)
at ../sysdeps/nptl/futex-internal.h:320
19 Thread 0x7f24767fc640 (LWP 24518) futex_abstimed_wait_cancelable (private=0, abstime=0x7f24767fb460, clockid=1988080528, expected=0, futex_word=0x55dcc44261e4)
at ../sysdeps/nptl/futex-internal.h:320 |
Interesting. That indeed seems to be crashing in a similar spot to my layman's eyes. I tried staring at how |
I am on linux but I have not used a reverse debugger before. Would a full backtrace with debug symbols be useful, you think? If so, Ill try to submit a bug report to the lean repo. |
(I'm no expert clearly either, but yeah something like rr is somewhat easier for non C++ programmers to poke back and forth at.)
I think all the important symbols that that would get are already there, so I think not, but not 100% sure -- much more helpful would be if you know how to deterministically get the crash to happen. For me it's not deterministic, so I literally wrote a neovim function that randomly moves the cursor until it happens. |
If you can, building with release type Debug is certainly helpful. This will also enable extra assertions (and hopefully point to the actual source of the error). Maybe you could also change this line in
|
Do you mean I should change the line linked below to the snippet you posted? |
Yes! |
I am unable to reproduce the seg faults after changing the line @gebner proposed and building with release type Debug. Was the line change meant to fix the issue? |
No the change was supposed to make Lean crash faster. Can you try again with the Release build type? |
Here's a SIGABRT from a Debug build:
This one doesn't seem to mention sexpr though... so maybe it's an unrelated one? |
Oooh, this is not good. This means that the error happens somewhere else, and we're just noticing at this point.. (and we still have no idea where it happens)
Yeah, presumably. It could help to enable ASAN ( |
I've seen ~20 crashes in the past 2-3 hours, and unlike the above, these all seem to come from sexpr:dealloc_cons if my backtrace reading isn't deceiving me. E.g. the most recent one:
EDIT: OK enabling ASAN on all my leans, let's see if that helps... |
I've just developed a strong hunch that this has to do with our handling of pin updating in the |
^ one way to test this theory would be to pause/disable infoview updates whenever you start editing and only re-enable them once you're done, and see if you ever get a segfault doing this. I'm doing more reading than writing at the moment but lmk if someone else has the chance to daily-drive this. |
Thanks for the idea! I think part of the thing that makes this annoying is it's really random to reproduce. Every few weeks it will happen 50 times in a row in a 20 minute period, and then other times only once or twice a day, and I have no idea why... I want to say you're right that it mostly happens when editing though, which is extra annoying because usually that means I've finally gotten a minute to do some Lean and it's hard to context switch to learning how to C++ debug... But I'm pretty confident we'll figure it out eventually. |
On the above -- I gutted It's |
Darn, yeah if #260 is related then I still see the problem in Lean 4 with the pin window paused. So it could be an upstream issue independent of incremental vs full document sync? Though from the sound of it none of you have seen this problem in Lean 4, so maybe something's off on my end. |
Also facing this issue. My main problem is that lean.nvim does not handle it well, and I wind up having to restart neovim completely for it to work again (sometimes doing EDIT: |
I am assuming this is ARM-specific, otherwise I presume otherwise it'd be reported by others, but I often get segmentation faults in buffers with Lean 3.This now seems not-OS dependent.I enabled core dumps and grabbed the below:
This likely belongs upstream (if it's even worth fixing at all), but just filing here for now since it's always in neovim that I see these, and I'm sure at least some diagnosing of what the backtrace in there is saying will be helpful before doing so.
The text was updated successfully, but these errors were encountered: