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