Skip to content
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.

Sign up for GitHub

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

Jump to bottom

some company-coq commands make emacs segfault #159

Closed
dredozubov opened this issue Apr 1, 2017 · 23 comments
Closed

some company-coq commands make emacs segfault #159

dredozubov opened this issue Apr 1, 2017 · 23 comments

Comments

@dredozubov
Copy link

dredozubov commented Apr 1, 2017 •
edited
Loading

I'm using Emacs 25.1.1 from https://emacsformacosx.com, HEAD Proof General revision 2cff44522ab8bdca8d73e3819f6ab89984f2c97c and company-coq. When I input a tactic name and press C-h, emacs crashes with a segfault: Fatal error 11: Segmentation faultzsh: abort /Applications/Emacs.app/Contents/MacOS/Emacs. I can achieve the same result with C-c C-a C-e. There's definitely a bug in Emacs(it segfaults after all), but company-coq probably does something that leads to it and I lack the expertise to find what that is.

What's peculiar - I can't seem to reproduce the same problem on a buffer from company-coq-tutorial, but it's 100% reproducible on my setup with any file from Software Foundations book(e.g. Logic.v). I would appreciate any tips in hunting this issue down.
@cpitclaudel
Copy link
Owner

Well, that's exciting. Sorry about this :/

Some questions:

  • Does it happen with all tactics? (the C-h thing) Does it happen in all files/buffers? If so, it's be tempting to blame libxml. The C-c C-a C-e would tend to confirm this
  • Can you get a backtrace? Run Emacs under gdb with gdb /path/to/emacs, then run run, and when it crashes type bt full. But I'm going to guess that we won't have debugging symbols.
  • Did you install specific fonts? Is there a lag before Emacs crashes, during which it consumes a lot of memory?

Thanks!

@dredozubov dredozubov changed the title some company-coq commands makes emacs segfault some company-coq commands make emacs segfault Apr 1, 2017
@dredozubov
Copy link
Author

Does it happen with all tactics? (the C-h thing) Does it happen in all files/buffers? If so, it's be tempting to blame libxml. The C-c C-a C-e would tend to confirm this

I tried around 5 built-in tactics and got the same result - segfault. Can you explain what's the role of libxml library in these processes?

Can you get a backtrace? Run Emacs under gdb with gdb /path/to/emacs, then run run, and when it crashes type bt full. But I'm going to guess that we won't have debugging symbols.

I don't have them in my current build, so I've decided to describe the issue before I start emacs re-building dance and all that fun. :)

Did you install specific fonts? Is there a lag before Emacs crashes, during which it consumes a lot of memory?

First of all. I'm using one of OS X system fonts(Menlo). It crashes pretty quickly and i wasn't able to see how much memory it consumes in the last moment, before crash it keeps its normal memory profile.

That question led me to some experimentation and it seems like disabling prettification helps with this issue.
I had this piece of configuration in my emacs config:

(add-hook 'coq-mode-hook
          (lambda ()
            (setq-local prettify-symbols-alist
                        '(("Proof." . ?∵) ("Qed." . ?■)
                          ("Defined." . ?□)
                          ("Alpha" . ?Α) ("Beta" . ?Β) ("Gamma" . ?Γ)
                          ("Delta" . ?Δ) ("Epsilon" . ?Ε) ("Zeta" . ?Ζ)
                          ("Eta" . ?Η) ("Theta" . ?Θ) ("Iota" . ?Ι)
                          ("Kappa" . ?Κ) ("Lambda" . ?Λ) ("Mu" . ?Μ)
                          ("Nu" . ?Ν) ("Xi" . ?Ξ) ("Omicron" . ?Ο)
                          ("Pi" . ?Π) ("Rho" . ?Ρ) ("Sigma" . ?Σ)
                          ("Tau" . ?Τ) ("Upsilon" . ?Υ) ("Phi" . ?Φ)
                          ("Chi" . ?Χ) ("Psi" . ?Ψ) ("Omega" . ?Ω)
                          ("alpha" . ?α) ("beta" . ?β) ("gamma" . ?γ)
                          ("delta" . ?δ) ("epsilon" . ?ε) ("zeta" . ?ζ)
                          ("eta" . ?η) ("theta" . ?θ) ("iota" . ?ι)
                          ("kappa" . ?κ) ("lambda" . ?λ) ("mu" . ?μ)
                          ("nu" . ?ν) ("xi" . ?ξ) ("omicron" . ?ο)
                          ("pi" . ?π) ("rho" . ?ρ) ("sigma" . ?σ)
                          ("tau" . ?τ) ("upsilon" . ?υ) ("phi" . ?φ)
                          ("chi" . ?χ) ("psi" . ?ψ) ("omega" . ?ω)))))

If i disable it, Emacs doesn't seem to segfault anymore!

@cpitclaudel
Copy link
Owner

Aha, the prettification thing is on a good track. There was a long thread about certain fonts crashing Emacs not so long ago on bug-gnu-emacs. Can you try enabling these prettifications in a fundamental-mode buffer and seeing if the problem exists there too ?

@dredozubov
Copy link
Author

@cpitclaudel Do you mean fundamental-mode + company-coq-mode? I don't see how it's possible to trigger the issue in pure fundamental-mode.

@cpitclaudel
Copy link
Owner

I meant prettify-symbols-mode + fundamental-mode (prettify-symbols-alist exists outside of company-coq-mode: it's part of a minor mode call prettify-symbols-mode)

@dredozubov
Copy link
Author

I haven't seen any problems with prettify-symbols-mode, so I'm not sure what are you looking for in this particular setup. The only way to trigger the segfault is C-h when I see company-based tactic dropdown and C-c C-a C-e with a type error "in scope". What behaviour do you expect to see in fundamental-mode buffer with prettificatioin?

@cpitclaudel
Copy link
Owner

cpitclaudel commented Apr 1, 2017 •
edited
Loading

What surprises me is that C-h shouldn't invoke more prettification, so the fact that disabling prettification fixes the segfault is surprising. C-c C-a C-e and C-h use libxml to render an HTML-based documentation page.

@anton-trunov
Copy link
Contributor

I've experienced segfaults as well. I'm using GNU Emacs 25.2.1 (x86_64-apple-darwin16.5.0, NS appkit-1504.82 Version 10.12.4 (Build 16E195)) installed via homebrew on macOS.
It seems that having this ("Proof." . ?∵) in prettify-symbols-alist promotes the segfaults, which occur when ∵ is visible.

@cpitclaudel
Copy link
Owner

@anton-trunov do you have a way to reliably reproduce the issue?

@anton-trunov
Copy link
Contributor

anton-trunov commented Jun 6, 2017 •
edited
Loading

The following reliably segfaults on my machine:

Goal 0 = 0.
Proof.
id

If I put the point after id and type t, company-coq shows the autocompletion menu, then C-h causes a segfault, provided Proof. is rendered as ∵. Actually, anything that invokes the menu + C-h would crash Emacs.

@cpitclaudel
Copy link
Owner

Ouch.
I wonder if that might be a libxml issue, since that's what used to render docs.
How comfortable do you feel with Emacs' debugger and with your platform's debugging tool (GDB or LLDB?). A backtrace would be useful.

@anton-trunov
Copy link
Contributor

Here is a log of my attempt of running Emacs under lldb. Please tell me if you'd like more than this.

➜  ~ lldb /usr/local/Cellar/emacs/25.3/Emacs.app/Contents/MacOS/Emacs
(lldb) target create "/usr/local/Cellar/emacs/25.3/Emacs.app/Contents/MacOS/Emacs"
Current executable set to '/usr/local/Cellar/emacs/25.3/Emacs.app/Contents/MacOS/Emacs' (x86_64).
(lldb) run
Process 21443 launched: '/usr/local/Cellar/emacs/25.3/Emacs.app/Contents/MacOS/Emacs' (x86_64)
### [At this point I did exactly what I wrote in my previous post]
Process 21443 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=2, address=0x7fff5f3aefd8)
    frame #0: 0x0000000100018e58 Emacs`get_next_display_element + 44
Emacs`get_next_display_element:
->  0x100018e58 <+44>: callq  *(%r12,%rax,8)
    0x100018e5c <+48>: movb   %al, %r13b
    0x100018e5f <+51>: movq   0x838(%rbx), %rcx
    0x100018e66 <+58>: testl  %ecx, %ecx

At this point (lldb) bt spits out 60290 entries:

* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=2, address=0x7fff5f3aefd8)
  * frame #0: 0x0000000100018e58 Emacs`get_next_display_element + 44
    frame #1: 0x000000010001988e Emacs`get_next_display_element + 2658.
...  (these are all identical)
    frame #60207: 0x000000010001988e Emacs`get_next_display_element + 2658.
    frame #60208: 0x000000010001b29e Emacs`move_it_in_display_line_to + 3968
    frame #60209: 0x0000000100018b3f Emacs`move_it_to + 807
    frame #60210: 0x0000000100020522 Emacs`move_it_vertically + 70
    frame #60211: 0x0000000100051d3e Emacs`Fwindow_end + 423
    frame #60212: 0x0000000100102847 Emacs`Ffuncall + 983
    frame #60213: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60214: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60215: 0x0000000100102cae Emacs`call1 + 46
    frame #60216: 0x00000001001095b7 Emacs`mapcar1 + 459
    frame #60217: 0x00000001001097d2 Emacs`Fmapc + 78
    frame #60218: 0x0000000100102847 Emacs`Ffuncall + 983
    frame #60219: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60220: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60221: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60222: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60223: 0x0000000100102c7a Emacs`call0 + 25
    frame #60224: 0x0000000100054031 Emacs`run_funs + 29
    frame #60225: 0x0000000100053eda Emacs`run_window_configuration_change_hook + 427
    frame #60226: 0x00000001000543f3 Emacs`set_window_buffer + 851
    frame #60227: 0x00000001000548fa Emacs`Fset_window_buffer + 178
    frame #60228: 0x000000010010285b Emacs`Ffuncall + 1003
    frame #60229: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60230: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60231: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60232: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60233: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60234: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60235: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60236: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60237: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60238: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60239: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60240: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60241: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60242: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60243: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60244: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60245: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60246: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60247: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60248: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60249: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60250: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60251: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60252: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60253: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60254: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60255: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60256: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60257: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60258: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60259: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60260: 0x0000000100103253 Emacs`funcall_lambda + 730
    frame #60261: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60262: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60263: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60264: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60265: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60266: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60267: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60268: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60269: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60270: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60271: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60272: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60273: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60274: 0x00000001001023a2 Emacs`Fapply + 579
    frame #60275: 0x00000001001027d0 Emacs`Ffuncall + 864
    frame #60276: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60277: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60278: 0x00000001001023a2 Emacs`Fapply + 579
    frame #60279: 0x00000001001027d0 Emacs`Ffuncall + 864
    frame #60280: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60281: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60282: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60283: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60284: 0x000000010013280c Emacs`exec_byte_code + 2035
    frame #60285: 0x0000000100102710 Emacs`Ffuncall + 672
    frame #60286: 0x00000001000fd6e2 Emacs`Ffuncall_interactively + 58
    frame #60287: 0x00000001001027d0 Emacs`Ffuncall + 864
    frame #60288: 0x00000001000fdbaa Emacs`Fcall_interactively + 1203
    frame #60289: 0x000000010010285b Emacs`Ffuncall + 1003
    frame #60290: 0x0

@cpitclaudel
Copy link
Owner

Great, thanks! Which version of Emacs are you using? Some font-related segfaults were fixed in Emacs 25. If it's not that, I'll ask the Emacs dev about this backtrace.

@anton-trunov
Copy link
Contributor

anton-trunov commented Sep 25, 2017 •
edited
Loading

GNU Emacs 25.3.1 (x86_64-apple-darwin16.7.0, NS appkit-1504.83 Version 10.12.6 (Build 16G29)) of 2017-09-25.
Emacs was installed via Homebrew with Cocoa support.

@cpitclaudel
Copy link
Owner

Snap, OK.
That's enough for me to ask for guidance on emacs-devel; thanks a lot. One last thing if you still have the time and patience, though: it'd be great to have an idea of where (on the list side) we are when the crash happens. You can get an idea of that by stepping through the code with the ELisp debugger. I can provide guidance on that, if you want to try :)
Thanks again!

@anton-trunov
Copy link
Contributor

Of course I want to try -- it's the least thing I can do to support this awesome tool!

@cpitclaudel
Copy link
Owner

Neat :) In that case, we can start this way:

First, confirm that running M-: (company-coq-doc-buffer-refman #("idtac" 0 5 (anchor ("9t" . 868)))) does crash Emacs. This is the function that eventually gets called from pressing C-h in the completion menu.

If it doesn't crash (and instead displays the doc buffer), then we'll have a very narrow piece of code left to debug. But most likely it will crash.

If it does crash, run M-x find-function company-coq-doc-buffer-refman to open a buffer pointing to the implementation of that function in company-coq's sources. There, you can press C-u C-M-x to instrument the function.

After this, use M-: (company-coq-doc-buffer-refman #("idtac" 0 5 (anchor ("9t" . 868)))) again to start stepping through the function with edebug. You can press space so step over the current form. Emacs should crash at some point, and the last point you'll have gotten to while debugging will tell you which function caused the crash. Then you can redo the same, but on the second time press i with your point right before the faulty form (for example, if the crash happens while running (company-coq-doc-refman-put-html doc-full-path), then press i with your point right before the opening parenthesis. This will step into the function, and in that function's body you can repeat the process (stepping through with space) to find the faulty form.

Let me know if I can clarify anything!

@anton-trunov
Copy link
Contributor

Thank you for such nice instructions!

As you predicted it fails (only if the proof symbol is visible at the moment I hit M-:). And here is the call stack:

(company-coq-doc-buffer-refman #("idtac" 0 5 (anchor ("9t" . 868))))
(company-coq-doc-refman-put-html doc-full-path)
(shr-insert-document doc)
(set-window-hscroll nil 0)

set-window-hscroll invocation makes Emacs crash

@anton-trunov
Copy link
Contributor

Hi @cpitclaudel! Did you by any chance send this set-window-hscroll stuff to emacs-devel?

@cpitclaudel
Copy link
Owner

AH, no, not yet :/ Sorry about this. This completely fell of my radar. I'll do it today.

@cpitclaudel
Copy link
Owner

Turns out that the bug had been reported by @dredozubov last July, and subsequently fixed in Emacs 26; see https://debbugs.gnu.org/cgi/bugreport.cgi?bug=27761 . Sorry for the trouble; I wasn't included in the bug thread, and I didn't hear about it until now.

@dredozubov
Copy link
Author

@cpitclaudel Sorry, I forgot to mention it at the time!
@anton-trunov can you still reproduce it with Emacs 26?

@anton-trunov
Copy link
Contributor

@dredozubov I upgraded my Emacs to 26.0.91 (9.0) and it appears the bug has been fixed.
Thanks a lot everybody!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@dredozubov @anton-trunov @cpitclaudel