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

[伊藤洋介]

*** 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@gmail.com