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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 47440 in the body.
You can then email your comments to 47440 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: 伊藤洋介 <glacier345 <at> gmail.com>
To: bug-gnu-emacs <at> gnu.org
Subject: 27.1; Quit/C-g does not interrupt Emacs promptly.
Date: Sun, 28 Mar 2021 10:26:24 +0900

[Message part 1 (text/plain, inline)]

*** 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.
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 44.29s)" :string "" (:array) ((:dict-entry "urgency"
(:variant :byte 1))) :int32 -1)
  notifications-notify(:body "" :urgency normal :title "Prover ready!
(proof took 44.29s)" :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 24671 54603 609259 nil
company-coq-features/alerts--maybe-alert nil nil 0])


In GNU Emacs 27.1 (build 1, x86_64-apple-darwin18.7.0, NS appkit-1671.60
Version 10.14.6 (Build 18G95))
of 2020-08-12 built on builder10-14.porkrind.org
Windowing system distributor 'Apple', version 10.3.2022
System Description:  macOS 11.2.3

Recent messages:
Debug on Error enabled globally
Debug on Quit enabled globally
Coq project file detected: /Users/yosukeito/Actuary/_CoqProject. [2 times]
Starting: coqtop -topfile /Users/yosukeito/Actuary/Papers/syllogism.v
-emacs -Q /Users/yosukeito/Actuary Actuary
Capability detection complete: dynamic completion is available.
Hit M-x proof-layout-windows to reset layout
M-x proof-prf for goals; M-x proof-layout-windows refreshes [2 times]
Starting coq process... done.
Quit
Entering debugger...

Configured using:
'configure --with-ns '--enable-locallisppath=/Library/Application
Support/Emacs/${version}/site-lisp:/Library/Application
Support/Emacs/site-lisp' --with-modules'

Configured features:
NOTIFY KQUEUE ACL GNUTLS LIBXML2 ZLIB TOOLKIT_SCROLL_BARS NS MODULES
THREADS JSON PDUMPER

Important settings:
  value of $LANG: ja_JP.UTF-8
  locale-coding-system: utf-8-unix

Major mode: Debugger

Minor modes in effect:
  show-paren-mode: t
  leaf-key-override-global-mode: t
  tooltip-mode: t
  global-eldoc-mode: t
  electric-indent-mode: t
  mouse-wheel-mode: t
  tool-bar-mode: t
  menu-bar-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  blink-cursor-mode: t
  auto-composition-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t
  buffer-read-only: t
  line-number-mode: t
  transient-mark-mode: t

Load-path shadows:
None found.

Features:
(shadow sort mail-extr emacsbug message rmc format-spec rfc822 mml
mml-sec epa derived epg epg-config gnus-util rmail rmail-loaddefs
mm-decode mm-bodies mm-encode mail-parse rfc2231 mailabbrev gmm-utils
mailheader sendmail rfc2047 rfc2045 ietf-drums mm-util mail-prsvr
mail-utils help-fns cl-print debug backtrace find-func time-date
warnings misearch multi-isearch coq-unicode-tokens proof-unicode-tokens
company-oddmuse company-keywords company-etags etags fileloop generator
xref project company-gtags company-dabbrev-code company-dabbrev
company-files company-clang company-capf company-cmake company-semantic
company-template company-bbdb disp-table help-at-pt company-coq
company-coq-utils company-coq-tg company-coq-abbrev notifications dbus
pulse yasnippet shr text-property-search url-cookie url-domsuf url-util
puny svg xml dom paren hideshow noutline outline dash company-math
math-symbol-lists company edmacro kmacro pcase which-func imenu coq
advice coq-diffs coq-par-compile coq-seq-compile coq-compile-common
compile comint ansi-color coq-abbrev coq-local-vars local-vars-list
coq-system proof proof-shell pg-user pg-goals pg-response proof-toolbar
pg-assoc proof-tree proof-auxmodes pg-custom proof-splash proof-script
proof-menu proof-utils scomint proof-syntax bufhist proof-config
proof-faces proof-useropts pg-pamacs proof-compat pg-vars coq-mode
coq-smie smie coq-syntax coq-db diff-mode easy-mmode holes span
coq-indent init yatexhks yatex19 yatexsec yatex yatexadd yatexflt
yatexlib hydra ring lv el-get el-get-autoloading el-get-list-packages
el-get-dependencies el-get-build el-get-status pp el-get-methods
el-get-fossil el-get-svn el-get-pacman el-get-github-zip
el-get-github-tar el-get-http-zip el-get-http-tar el-get-hg el-get-go
el-get-git-svn el-get-fink el-get-emacswiki el-get-http el-get-notify
el-get-emacsmirror el-get-github el-get-git el-get-elpa el-get-darcs
el-get-cvs el-get-bzr el-get-brew el-get-builtin el-get-apt-get
el-get-recipes el-get-byte-compile el-get-custom cl-extra help-mode
el-get-core autoload radix-tree lisp-mnt cl dired dired-loaddefs
leaf-keywords leaf finder-inf cus-edit cus-start cus-load wid-edit
proof-site proof-autoloads info package easymenu browse-url url-handlers
url-parse auth-source cl-seq eieio eieio-core cl-macs eieio-loaddefs
password-cache json subr-x map url-vars seq byte-opt gv bytecomp
byte-compile cconv cl-loaddefs cl-lib japan-util tooltip eldoc electric
uniquify ediff-hook vc-hooks lisp-float-type mwheel term/ns-win ns-win
ucs-normalize mule-util term/common-win tool-bar dnd fontset image
regexp-opt fringe tabulated-list replace newcomment text-mode elisp-mode
lisp-mode prog-mode register page tab-bar menu-bar rfn-eshadow isearch
timer select scroll-bar mouse jit-lock font-lock syntax facemenu
font-core term/tty-colors frame minibuffer cl-generic cham georgian
utf-8-lang misc-lang vietnamese tibetan thai tai-viet lao korean
japanese eucjp-ms cp51932 hebrew greek romanian slovak czech european
ethiopic indian cyrillic chinese composite charscript charprop
case-table epa-hook jka-cmpr-hook help simple abbrev obarray
cl-preloaded nadvice loaddefs button faces cus-face macroexp files
text-properties overlay sha1 md5 base64 format env code-pages mule
custom widget hashtable-print-readable backquote threads kqueue cocoa ns
multi-tty make-network-process emacs)

Memory information:
((conses 16 417471 21029)
(symbols 48 29035 5)
(strings 32 134196 3754)
(string-bytes 1 3208544)
(vectors 16 40463)
(vector-slots 8 824202 24544)
(floats 8 125 237)
(intervals 56 3766 83)
(buffers 1000 19))

-- 
伊藤洋介
Yosuke Ito
glacier345 <at> gmail.com

[Message part 2 (text/html, inline)]

Message #8 received at 47440 <at> debbugs.gnu.org (full text, mbox):

From: Stefan Monnier <monnier <at> iro.umontreal.ca>
To: 伊藤洋介 <glacier345 <at> gmail.com>
Cc: 47440 <at> debbugs.gnu.org
Subject: Re: bug#47440: 27.1; Quit/C-g does not interrupt Emacs promptly.
Date: Sun, 28 Mar 2021 00:13:39 -0400

> *** 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

Message #11 received at 47440 <at> debbugs.gnu.org (full text, mbox):

From: 伊藤洋介 <glacier345 <at> gmail.com>
To: Stefan Monnier <monnier <at> iro.umontreal.ca>
Cc: 47440 <at> debbugs.gnu.org
Subject: Re: bug#47440: 27.1; Quit/C-g does not interrupt Emacs promptly.
Date: Sun, 28 Mar 2021 16:28:54 +0900

[Message part 1 (text/plain, inline)]

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 <at> 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 <at> gmail.com

[Message part 2 (text/html, inline)]

Message #16 received at 47440-done <at> debbugs.gnu.org (full text, mbox):

From: Stefan Monnier <monnier <at> iro.umontreal.ca>
To: 伊藤洋介 <glacier345 <at> gmail.com>
Cc: 47440-done <at> debbugs.gnu.org
Subject: Re: bug#47440: 27.1; Quit/C-g does not interrupt Emacs promptly.
Date: Sun, 28 Mar 2021 16:05:03 -0400

> 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.

I misunderstood what was going on, indeed (the C-g was presumably
processed right away as it should and the backtrace you get later is
unrelated to the C-g).  So I think there's no sign of a bug in Emacs
itself here.  Actually the backtrace you sent already made it clear
since it said "Emacs not compiled with dbus support".
I was not paying much attention, it seems, sorry.

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

Your explanation was fine.  The confusion was all mine ;-)


        Stefan

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.