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

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

[伊藤洋介]

[-- Attachment #1: Type: text/plain, Size: 6750 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 89509 bytes --]

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

[Stefan Monnier]

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

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

[伊藤洋介]

[-- Attachment #1: Type: text/plain, Size: 2361 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 3433 bytes --]

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

[Stefan Monnier]

> 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