bug#47440: 27.1; Quit/C-g does not interrupt Emacs promptly.

[伊藤洋介]

Dear Stefan,

Thanks for your help!

I tried as you say, and the result was that I got the message

D-Bus error: "Emacs not compiled with dbus support"

in the minibuffer.

Actually, the freeze did not happen.

I mean, the situation seemed to be the same as before entering `M-x eval-buffer RET`.

Maybe the word "freeze" was inappropriate.

What I wanted to convey is as follows.

I did "I-search" (C-s) then "proof-assert-next-command-interactive" (C-c C-n),

but the proof process got stuck.

Here, "got stuck" means that Emacs did not go out of the proof process for several minutes.

During that situation, I could move the cursor but I could not interrupt the proof process by Quit/C-g or tool-bar interrupt.

The backtrace that I sent earlier was shown immediately after the proof process was over,

say, several minutes after Emacs got stuck.

I apologize if my explanation is confusing, since I am not so fluent in English.

2021年3月28日(日) 13:13 Stefan Monnier <monnier@iro.umontreal.ca>:

> *** This report is related to the Proof General Issues "Proof General
> freezes after I-search #565. ***

> I use Proof General Version 4.5-git, Company-Coq.

> The bug description is as follows.
> I did "I-search" (C-s) then "proof-assert-next-command-interactive" (C-c
> C-n), but the proof process got stuck.
> So I pressed "Quit" (C-g), however the backtrace did not appear
> promptly.

> For your information, the backtrace is the following.
[...]

Could you try to put the following in say ~/tempfile.el

    (require 'dbus)
    (dbus-call-method
     :session "org.freedesktop.Notifications"
     "/org/freedesktop/Notifications" "org.freedesktop.Notifications"
     "Notify" :string "Emacs" :uint32 0
     :string "/Users/yosukeito/.emacs.d/elpa/company-coq-2020072..."
     :string "Prover ready! (proof took 44.29s)"
     :string "" '(:array) '((:dict-entry "urgency" (:variant :byte 1)))
     :int32 -1)

then do `emacs -Q ~/tempfile.el` and in that Emacs do
`M-x eval-buffer RET`.

This should presumably suffer from the same freeze as you
saw with company-coq.  Then hit C-g while it's frozen.
Does it still fail to interrupt Emacs immediately?


        Stefan

--

伊藤洋介

080-5057-6931

glacier345@gmail.com