search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
488 stars 86 forks source link

PG hangs sporadically #524

Closed jgrosso closed 3 years ago

jgrosso commented 3 years ago

Often, PG becomes slow and unresponsive—the goals window doesn't update for ~30 seconds at a time, for example, but manually calling proof-layout-windows causes the UI to update.

I've run a CPU+mem profile during one of the hangs, and nothing looked out-of-the-ordinary.

(Just to confirm it wasn't the proof file itself, I've compared CoqIDE and Proof General with the same file, line number, specific tactic I'm evaluating, etc., and CoqIDE finishes quickly and as expected.)

Unfortunately, it's hard for me to give more specific details since it doesn't happen consistently or with a discernible reason.

cpitclaudel commented 3 years ago

Ouch, thanks for the report.

Unfortunately, it's hard for me to give more specific details

Can you give the output of M-x report-emacs-bug, as well as the list of packages that you're using in Coq buffers, and maybe a screenshot or video of what it looks like when PG is frozen?

jgrosso commented 3 years ago

Please let me know if I can give any other information.

Screen captures of general wonkiness (I occassionally used the Spacemacs keybinding for proof-layout-windows when PG was stuck, i.e. when , l p for goals: , l l refreshes shows up in the minibuffer): https://imgur.com/a/LbPLWVg

emacs-bug-report:

In GNU Emacs 28.0.50 (build 1, x86_64-apple-darwin19.6.0, NS appkit-1894.60 Version 10.15.6 (Build 19G2021))
 of 2020-09-30 built on macbook-pro-3.lan
Repository revision: 89f064104c25f8b4362ef54d28fd4bce18f6af3b
Repository branch: feature/native-comp
Windowing system distributor 'Apple', version 10.3.1894
System Description:  Mac OS X 10.15.7

Configured using:
 'configure --prefix=/usr/local/opt/gccemacs
 --enable-locallisppath=/usr/local/opt/gccemacs/opt/gccemacs/site-lisp
 --with-mailutils --with-ns --with-imagemagick --with-cairo
 --with-modules --with-xml2 --with-gnutls --with-json --with-rsvg
 --with-nativecomp --disable-silent-rules --disable-ns-self-contained
 --without-dbus CFLAGS=-I/usr/local/Cellar/gcc/10.2.0/include
 'LDFLAGS=-L/usr/local/Cellar/gcc/10.2.0/lib/gcc/10
 -I/usr/local/Cellar/gcc/10.2.0/include''

Configured features:
JPEG TIFF GIF PNG RSVG IMAGEMAGICK GLIB NOTIFY KQUEUE ACL GNUTLS LIBXML2
ZLIB TOOLKIT_SCROLL_BARS XIM NS MODULES NATIVE_COMP THREADS JSON PDUMPER
LCMS2

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

Major mode: Coq

Minor modes in effect:
  eval-sexp-fu-flash-mode: t
  global-evil-surround-mode: t
  evil-surround-mode: t
  company-coq-mode: t
  company-coq--keybindings-minor-mode: t
  show-paren-mode: t
  goto-address-prog-mode: t
  bug-reference-prog-mode: t
  auto-highlight-symbol-mode: t
  global-flycheck-mode: t
  highlight-numbers-mode: t
  highlight-parentheses-mode: t
  rainbow-delimiters-mode: t
  show-smartparens-global-mode: t
  show-smartparens-mode: t
  smartparens-mode: t
  yas-global-mode: t
  yas-minor-mode: t
  holes-mode: t
  global-vi-tilde-fringe-mode: t
  vi-tilde-fringe-mode: t
  evil-escape-mode: t
  global-display-line-numbers-mode: t
  display-line-numbers-mode: t
  projectile-mode: t
  recentf-mode: t
  global-magit-file-mode: t
  magit-file-mode: t
  global-git-commit-mode: t
  async-bytecomp-package-mode: t
  global-subword-mode: t
  subword-mode: t
  winner-mode: t
  company-mode: t
  global-spacemacs-whitespace-cleanup-mode: t
  spacemacs-whitespace-cleanup-mode: t
  winum-mode: t
  pupo-mode: t
  global-undo-tree-mode: t
  undo-tree-mode: t
  spaceline-info-mode: t
  save-place-mode: t
  savehist-mode: t
  persp-mode: t
  global-hl-todo-mode: t
  purpose-mode: t
  eyebrowse-mode: t
  evil-mc-mode: t
  global-anzu-mode: t
  anzu-mode: t
  editorconfig-mode: t
  outline-minor-mode: t
  counsel-mode: t
  ivy-mode: t
  delete-selection-mode: t
  clean-aindent-mode: t
  which-key-mode: t
  override-global-mode: t
  shell-dirtrack-mode: t
  evil-mode: t
  evil-local-mode: t
  spacemacs-leader-override-mode: t
  global-spacemacs-leader-override-mode: t
  global-hl-line-mode: t
  xterm-mouse-mode: t
  global-auto-revert-mode: t
  ido-vertical-mode: t
  global-page-break-lines-mode: t
  global-eldoc-mode: t
  electric-indent-mode: t
  mouse-wheel-mode: t
  prettify-symbols-mode: t
  menu-bar-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  auto-composition-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t
  column-number-mode: t
  line-number-mode: t
  global-visual-line-mode: t
  visual-line-mode: t
  transient-mark-mode: t
  hs-minor-mode: t

Load-path shadows:
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/magit-section-20201022.1623/magit-section hides /Users/joshuagrosso/.emacs.d/elpa/28.0/develop/magit-20201028.1912/magit-section
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/ht-20200217.2331/ht hides /Users/joshuagrosso/.emacs.d/core/libs/ht
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/spinner-1.7.3/spinner hides /Users/joshuagrosso/.emacs.d/core/libs/spinner
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/dash-20200803.1520/dash hides /Users/joshuagrosso/.emacs.d/core/libs/dash
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-stan hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-stan
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-exp hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-exp
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-J hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-J
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-emacs-lisp hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-emacs-lisp
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-css hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-css
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-lob hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-lob
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-irc hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-irc
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-forth hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-forth
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-macs hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-macs
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-version hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-version
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-scheme hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-scheme
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-abc hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-abc
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-C hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-C
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-capture hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-capture
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ref hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ref
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-clojure hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-clojure
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-mouse hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-mouse
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ledger hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ledger
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-ctags hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-ctags
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-entities hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-entities
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-archive hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-archive
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-screen hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-screen
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-bibtex hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-bibtex
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-haskell hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-haskell
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-asymptote hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-asymptote
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-table hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-table
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-eww hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-eww
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-org hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-org
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-num hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-num
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-plot hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-plot
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-rmail hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-rmail
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-awk hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-awk
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-groovy hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-groovy
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-octave hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-octave
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-faces hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-faces
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-colview hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-colview
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-R hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-R
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-timer hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-timer
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ebnf hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ebnf
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-mobile hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-mobile
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-fortran hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-fortran
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-shell hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-shell
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-perl hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-perl
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-sqlite hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-sqlite
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-sed hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-sed
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-list hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-list
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ruby hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ruby
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-eval hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-eval
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-habit hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-habit
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-clock hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-clock
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-goto hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-goto
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-html hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-html
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-src hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-src
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-lisp hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-lisp
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-eshell hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-eshell
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ditaa hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ditaa
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-pcomplete hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-pcomplete
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-lint hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-lint
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-latex hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-latex
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-sass hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-sass
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-io hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-io
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-tangle hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-tangle
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-calc hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-calc
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-java hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-java
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-icalendar hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-icalendar
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-mhe hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-mhe
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-attach-git hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-attach-git
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-md hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-md
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-beamer hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-beamer
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-element hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-element
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-protocol hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-protocol
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-mscgen hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-mscgen
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-gnuplot hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-gnuplot
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-tempo hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-tempo
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-latex hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-latex
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-w3m hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-w3m
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-id hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-id
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-vala hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-vala
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-man hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-man
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-feed hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-feed
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-lua hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-lua
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-table hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-table
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-ocaml hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-ocaml
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-coq hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-coq
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-gnus hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-gnus
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-picolisp hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-picolisp
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-indent hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-indent
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-lilypond hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-lilypond
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-matlab hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-matlab
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-datetree hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-datetree
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-docview hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-docview
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-python hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-python
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-makefile hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-makefile
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-duration hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-duration
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-agenda hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-agenda
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-dot hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-dot
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-js hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-js
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-publish hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-publish
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-inlinetask hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-inlinetask
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-org hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-org
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-keys hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-keys
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-core hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-core
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-compat hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-compat
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-odt hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-odt
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-info hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-info
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-plantuml hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-plantuml
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-eshell hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-eshell
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-ascii hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-ascii
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-loaddefs hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-loaddefs
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-hledger hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-hledger
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-maxima hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-maxima
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ol-bbdb hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ol-bbdb
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-macro hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-macro
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-sql hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-sql
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-attach hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-attach
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-processing hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-processing
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ox-texinfo hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ox-texinfo
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-crypt hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-crypt
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-footnote hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-footnote
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/org-install hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/org-install
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-comint hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-comint
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/org-plus-contrib-20201012/ob-shen hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/org/ob-shen
/Users/joshuagrosso/.emacs.d/elpa/28.0/develop/hierarchy-20190425.842/hierarchy hides /usr/local/opt/gccemacs/share/emacs/28.0.50/lisp/emacs-lisp/hierarchy

Features:
(overseer pkg-info epl auto-compile packed elisp-slime-nav flycheck-elsa
flycheck-package package-lint finder eval-sexp-fu vc-mtn vc-hg vc-bzr
vc-src vc-sccs vc-svn vc-cvs vc-rcs shadow sort mail-extr emacsbug
sendmail smex magit-bookmark bookmark pp tabify tramp tramp-loaddefs
trampver tramp-integration files-x tramp-compat ls-lisp ffap org-clock
diary-lib diary-loaddefs cal-iso org-eldoc evil-org ob-js ob-shell
org-download org-attach org-id url-http url-auth url-gw nsm
org-superstar toc-org image-file image-converter ol-eww eww url-queue
mm-url ol-rmail ol-mhe ol-irc ol-info ol-gnus nnselect nnir gnus-art
mm-uu mml2015 mm-view mml-smime smime dig gnus-sum url url-proxy
url-privacy url-expand url-methods url-history mailcap gnus-group
gnus-undo gnus-start gnus-dbus gnus-cloud nnimap nnmail mail-source utf7
netrc nnoo parse-time iso8601 gnus-spec gnus-int gnus-range gnus-win
gnus nnheader ol-docview doc-view jka-compr image-mode exif ol-bibtex
bibtex ol-bbdb ol-w3m org-habit org-agenda org-refile coq-unicode-tokens
proof-unicode-tokens evil-surround company-oddmuse company-keywords
company-etags etags fileloop company-gtags company-dabbrev-code
company-dabbrev company-files company-clang company-capf company-cmake
company-semantic company-template company-bbdb help-at-pt company-coq
company-coq-utils company-coq-tg company-coq-abbrev alert log4e
notifications dbus gntp pulse shr kinsoku url-cookie url-domsuf svg xml
dom paren company-math math-symbol-lists goto-addr vc-git vc
vc-dispatcher bug-reference auto-highlight-symbol evil-lisp-state
flycheck highlight-numbers parent-mode highlight-parentheses hideshow
rainbow-delimiters smartparens-config smartparens-org smartparens-text
smartparens yasnippet-snippets yasnippet coq coq-diffs coq-par-compile
coq-seq-compile coq-compile-common 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 holes span coq-indent
editorconfig-core editorconfig-core-handle editorconfig-fnmatch
vi-tilde-fringe diminish evil-escape display-line-numbers face-remap
disp-table projectile grep recentf tree-widget org-re-reveal url-util
ox-gfm ox-md ox-odt rng-loc rng-uri rng-parse rng-match rng-dt rng-util
rng-pttrn nxml-parse nxml-ns nxml-enc xmltok nxml-util ox-latex
ox-icalendar ox-html table ox-ascii ox-publish ox org-element orgit
evil-magit git-rebase magit-submodule magit-obsolete magit-popup
magit-blame magit-stash magit-reflog magit-bisect magit-push magit-pull
magit-fetch magit-clone magit-remote magit-commit magit-sequence
magit-notes magit-worktree magit-tag magit-merge magit-branch
magit-reset magit-files magit-refs magit-status magit magit-repos
magit-apply magit-wip magit-log which-func magit-diff smerge-mode
diff-mode magit-core magit-autorevert magit-margin magit-transient
magit-process magit-mode git-commit transient magit-git magit-section
magit-utils log-edit message rmc puny rfc822 mml mml-sec epa gnus-util
rmail rmail-loaddefs text-property-search mailabbrev mail-utils
gmm-utils mailheader pcvs-util add-log with-editor async-bytecomp async
org ob ob-tangle ob-ref ob-lob ob-table org-macro org-footnote org-src
ob-comint org-pcomplete org-list org-faces org-entities time-date
org-version ob-emacs-lisp org-table org-keys org-loaddefs find-func
cal-menu calendar cal-loaddefs avl-tree generator ol ob-exp ob-core
org-compat ob-eval org-macs cap-words superword subword winner server
merlin-company merlin-cap merlin crm company opam-user-setup xterm-color
spacemacs-whitespace-cleanup ws-butler winum spacemacs-purpose-popwin
window-purpose-x imenu-list imenu ibuf-ext ibuffer ibuffer-loaddefs
unicode-fonts undo-tree diff symbol-overlay string-inflection
spaceline-config spaceline-segments spaceline powerline
powerline-separators powerline-themes saveplace savehist popwin
persp-mode osx-trash org-rich-yank ivy-hydra ivy-avy avy hl-todo
window-purpose window-purpose-fixes window-purpose-prefix-overload
window-purpose-switch let-alist window-purpose-layout
window-purpose-core window-purpose-configuration window-purpose-utils
eyebrowse evil-unimpaired f evil-textobj-line evil-mc
evil-mc-command-execute evil-mc-command-record evil-mc-cursor-make
evil-mc-region evil-mc-cursor-state evil-mc-undo evil-mc-vars
evil-mc-known-commands evil-mc-common evil-anzu anzu emr popup s
editorconfig ediprolog noutline outline counsel xdg xref project dired
dired-loaddefs compile swiper ivy flx delsel ivy-faces ivy-overlay colir
color clean-aindent-mode agda2 w3m-load proof-site proof-autoloads cl
tex-site hybrid-mode evil-evilified-state which-key use-package
use-package-ensure use-package-delight use-package-diminish
use-package-bind-key bind-key use-package-core hydra lv cus-edit
cus-start cus-load evil evil-keybindings evil-integration evil-maps
evil-commands reveal flyspell ispell evil-jumps evil-command-window
evil-types evil-search evil-ex shell pcomplete comint ansi-color
evil-macros evil-repeat evil-states evil-core evil-common windmove
thingatpt rect evil-digraphs evil-vars ring bind-map quelpa mm-decode
mm-bodies mm-encode mail-parse rfc2231 rfc2047 rfc2045 mm-util
ietf-drums mail-prsvr lisp-mnt help-fns radix-tree hl-line xt-mouse
autorevert filenotify comp cl-extra wid-edit spacemacs-dark-theme
spacemacs-common format-spec info finder-inf ido-vertical-mode ido
core-spacemacs core-spacebind core-use-package-ext core-transient-state
core-micro-state core-toggle core-keybindings core-fonts-support
core-themes-support core-display-init core-jump core-release-management
core-custom-settings core-configuration-layer eieio-compat
core-progress-bar core-spacemacs-buffer core-funcs ht dash help-mode
warnings package browse-url url-handlers url-parse auth-source cl-seq
password-cache json map url-vars seq eieio byte-opt bytecomp
byte-compile cconv eieio-core eieio-loaddefs epg epg-config
core-command-line core-debug edmacro kmacro derived profiler easymenu
core-hooks page-break-lines easy-mmode core-env load-env-vars rx
core-dotspacemacs advice core-emacs-backports core-dumper subr-x spinner
cl-macs gv cl-loaddefs cl-lib 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 button
loaddefs faces cus-face pcase macroexp files window text-properties
overlay sha1 md5 base64 format env code-pages mule custom widget
hashtable-print-readable backquote threads kqueue cocoa ns lcms2
multi-tty make-network-process emacs)

Memory information:
((conses 16 1393232 1395873)
 (symbols 48 90538 126)
 (strings 32 321642 152968)
 (string-bytes 1 12629819)
 (vectors 16 106343)
 (vector-slots 8 2892698 663256)
 (floats 8 927 8246)
 (intervals 56 20917 23392)
 (buffers 992 21))
cpitclaudel commented 3 years ago

Thanks. Do you see the same problem if you turn off company-coq? (I'm guessing yes, because it would cause a real freeze, not just a refresh hang, but…).

jgrosso commented 3 years ago

It might take a while to get a good test because the problem is sporadic, but the next time I start running into issues I'll disable company-coq and see if that helps (and then report back here). (Very preliminary investigation on my part indicates it might, but I don't have nearly enough evidence yet to proceed.)

jgrosso commented 3 years ago

Just for the sake of completeness, one symptom I notice often is that if I call e.g. evil-section-forward-begin (since I'm using Spacemacs with Vim bindings) several times in quick succession, the goals/responses windows will only advance part of the way through the proof script (the background highlighting in the proof file buffer itself, however, is correct).

EDIT: Without knowing anything about PG's internals: it feels like I'm "overwhelming" it somehow by giving it commands too quickly. Not sure if that makes sense or not, but that's the intuitive feel on my end.

jgrosso commented 3 years ago

@cpitclaudel I've finally been able to (briefly) screen-capture the significant difference that disabling company-coq makes, both in terms of the hanging and also overall performance.

https://youtu.be/DI5UkAjs0iQ

cpitclaudel commented 3 years ago

Thanks for your patience, this is terrible. Any chance to M-x profiler-start, do a few back-and-forths, then M-x profiler-report? I wonder if it's garbage collection. (On my machine company-coq freezes Emacs when the completion lists that it loads from Coq get very long.)

djeis97 commented 3 years ago

It's the spinner in company-coq, I discovered the issue myself a week or so ago. Even when it's not actually part of the modeline, when enabled the code for it runs a timer that forces modeline refreshes 20 times a second by default (company-coq-features/spinner-delay). If refreshing your modeline isn't super cheap then my guess is that overwhelms something going on in the background. Regardless, I used to experience this exact slowdown and disabling the spinner fixed it for me.

cpitclaudel commented 3 years ago

Ah, snap, that would make sense. Modelines have become a lot more complex in the last few years, and when I wrote this I had a simple modeline. Should we just turn it off?

dbp commented 3 years ago

I just wanted to flag that I think I've been having the same issue... Essentially, over time Proof General becomes slower and slower (can take 10+ seconds to evaluate a single statement) -- I was just quitting emacs and restarting, which would fix the issue temporarily, but after finding this issue, disabling company-coq seems to have permanently fixed the problem (though, I miss having it!).

cpitclaudel commented 3 years ago

Can you try the fix suggested in the message above?

cpitclaudel commented 3 years ago

(That is, just disabling the spinner feature using M-x customize-variable company-coq-disabled-features?

cpitclaudel commented 3 years ago

(Done in https://github.com/cpitclaudel/company-coq/commit/7423ee253951a439b2491e1cd2ea8bb876d25cb7)

dbp commented 3 years ago

I just set that; I'll let you know if the issue recurs. Thanks!

cpitclaudel commented 3 years ago

Thanks a lot. I've disabled it for everyone in any case.

dbp commented 3 years ago

Just to follow up, I think this was indeed the issue, as it hasn't recurring in the last week or so (and it was a multiple times daily experience before...).

cpitclaudel commented 3 years ago

Thanks a lot for reporting, testing, and confirming. I will close this issue, then.