Proof General freezes after I-search

[Yosuke-Ito-345]

I'm using Proof General (Coq) on emacs, and facing a problem. If I do "proof-assert-next-command-interactive" C-c C-n after using "I-search" C-s, then the proof process gets stuck and never ends. I'm quite new to Coq and not able to fix this bug. I'd be happy if you give me some advice. I use macOS Big Sur, GNU Emacs 27.1, Proof General Version 4.5-git, Company-Coq.

[Matafou]

Hi, can you describe what you do to make this happen please? Please also give the content of the file you are using, because most often PG gets stuck because it sends a text to the coq process that is not recognize as a command by coq.

[Yosuke-Ito-345]

Thanks for your reply. This phenomenon always happens once I use "I-search" or "I-search backward". I don't do anything special. For example, I open the attached file "syllogism.v" by PG, and do "I-search", then "proof-assert-next-command-interactive" makes PG stuck. For your information, I also post the setting file "init.el" of emacs. codes.zip

[Matafou]

Sorry this is still not enough for me to understand when this happens.

• I-search (if you mean isearch-forward) is usually invoked via control-s. Is it what you do?
• Once you have invoked isearch-forward you need to type characters and then return, is it after all these actions that PG is stuck or do you do proof-assert-next-command-interactive before hitting return?
• These operations, do you perform them in the buffer of the coq file? Or in the *coq* buffer?

I dont have a mac to test this but I suspect a macos specific problem.

[Yosuke-Ito-345]

Sorry for inadequate information.

• I use "I-search" (I mean isearch-forward) via C-s.
• I did "proof-assert-next-command-interactive" after "I-search" was over. I mean, I did C-s, typed some characters, hit return, then C-c C-n made PG stuck.
• I performed these operations in the minibuffer of emacs. Precisely, I typed C-s then "I-search:" was printed in the minibuffer, and entered some characters after that. Please let me know if these explanations are not clear to you.

[Yosuke-Ito-345]

I got further information about this phenomenon. If I waited during PG was stuck for 10 minutes, then the proof process proceeded, and I got the following message.

Error: (dbus-error "Emacs not compiled with dbus support")

I looked up this error but couldn't find enough information. Do you know what it means?

[Matafou]

I have no clue. What eMacs are you using? Aquamacs?

[Yosuke-Ito-345]

Oh... I'm using the usual GNU emacs, which is downloaded from https://www.gnu.org/software/emacs/.

[monnier]

I got further information about this phenomenon. If I waited during PG was stuck for 10 minutes, then the proof process proceeded, and I got the following message.

Error: (dbus-error "Emacs not compiled with dbus support")

I looked up this error but couldn't find enough information. Do you know what it means?

Try the following:

• Enable both "Options => Enter Debugger on Error" and "Options => Enter Debugger on Quit/C-g".

• Reproduce the "freeze".

• In the middle of the freeze, hit C-g.

Hopefully you'll then get a *Backtrace* buffer showing what Emacs (that's its official spelling ;-) is currently doing. Then send us a copy of this backtrace.

[Yosuke-Ito-345]

Thanks for your help! I tried the debugger and got the following result on the Backtrace frame.

Debugger entered--Lisp error: (dbus-error "Emacs not compiled with dbus support") signal(dbus-error ("Emacs not compiled with dbus support")) 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 36.24s)" :string "" (:array) ((:dict-entry "urgency" (:variant :byte 1))) :int32 -1) notifications-notify(:body "" :urgency normal :title "Prover ready! (proof took 36.24s)" :app-icon "/Users/yosukeito/.emacs.d/elpa/company-coq-2020072...") company-coq-features/alerts--alert() company-coq-features/alerts--maybe-alert() apply(company-coq-features/alerts--maybe-alert nil) timer-event-handler([t 24670 39216 941954 nil company-coq-features/alerts--maybe-alert nil nil 0])

Although I can't see where is the cause of this freeze...

[cpitclaudel]

Ha, fascinating! Company-coq is trying to let you know that a proof completed, and since your Emacs doesn't support notifications, that breaks. Did you get this backtrace after pressing C-g? Or did you get it earlier? If you do M-x company-coq-toggle-feature RET alerts RET, do you still see the freeze after that?

[Yosuke-Ito-345]

Thanks for your reply. I partly understand what's happening in Emacs. I got this backtrace after pressing C-g. Precisely, it took several minutes to get the backtrace after C-g. I tried M-x company-coq-toggle-feature RET alerts RET, but the PG still gets stuck...

[monnier]

I got this backtrace after pressing C-g. Precisely, it took several minutes to get the backtrace after C-g.

Please report this part as a bug in Emacs, i.e. with M-x report-emacs-bug: C-g should interrupt Emacs promptly rather than only after several minutes.

[Yosuke-Ito-345]

Thanks for your help. I have just sent the bug to [email protected]. This is the first time bug reporting, so I hope I did not make a mistake.

[Matafou]

Thanks alot @monnier. Do you confirm that brew emacs is compiled without dbus?

[monnier]

@Matafou: Don't thank me too quickly, I was confused: the backtrace he got has nothing to do with C-g (indeed it says (dbus-error "Emacs not compiled with dbus support") rather than saying that we entered the debugger because of a quit signal).

So, I think that when PG is "frozen" Emacs is actually responsive and idle (so the C-g is processed right away and just runs the usual keyboard-quit).

[Matafou]

Well anyway even if C-g was bugged that wouldn't change the fact that PG (or at least company-coq) currently depends on dbus. I have no clue if this is OK to simply say "have dbus" at the right place in the documentation. Or have a test in melpa package install? How many versions of emacs in the wild do not have dbus?

[cpitclaudel]

It's an optional feature, so there's not too much to worry about, I think? I was surprised to see that the alert feature is provided even when dbus support isn't compiled in, though.

[Yosuke-Ito-345]

Well, thanks everyone. I am not so familiar with dbus, but is there any way to fix this problem by myself? As it stands, I have to restart Emacs once I mistakenly press C-s. My only idea is to unset the key C-s, which may not be a fundamental solution.

[Matafou]

Dis you try the workaround proposed by @cpitclaudel ?

[Yosuke-Ito-345]

Yes, I did, but unfortunately the situation did not change.

[cpitclaudel]

Yes, I did, but unfortunately the situation did not change.

You got the same dbus backtrace after turning off alerts?

[Yosuke-Ito-345]

No. Actually, I cannot even get the backtrace now...