window-live-p error (coq, aquamacs)

[coquser]

When starting PG on a .v file, or when switching from one file to another (i.e., retract current buffer, and go to point in another one), PG, generates the following error, repeatedly.

error in process filter: progn: Wrong type argument: window-live-p, nil error in process filter: Wrong type argument: window-live-p, nil

It eventually stops and behaves normally after a few seconds (1 to ten -- it seems to become longer and longer along with the process lifetime). A backtrace is included below.

I'm using the current cvs version of PG, with Aquamacs 2.4 (Emacs 23.3.50.1 inside).

Best, Damien

Debugger entered--Lisp error: (wrong-type-argument window-live-p nil)

select-window(nil norecord) (progn (select-window (get-buffer-window proof-script-buffer) (quote norecord)) (- (window-height) window-min-height)) (unwind-protect (progn (select-window ... ...) (- ... window-min-height)) (dolist (elt save-selected-window-alist) (and ... ... ...)) (when (window-live-p save-selected-window-window) (select-window save-selected-window-window ...))) (save-current-buffer (unwind-protect (progn ... ...) (dolist ... ...) (when ... ...))) (let ((save-selected-window-window ...) (save-selected-window-alist ...)) (save-current-buffer (unwind-protect ... ... ...))) (with-selected-window (get-buffer-window proof-script-buffer) (- (window-height) window-min-height)) (let ((maxhgth ...) hgt-resp nline-resp) (with-selected-window (get-buffer-window proof-response-buffer) (setq hgt-resp ...) (with-current-buffer proof-response-buffer ...) (unless ... ...) (with-current-buffer proof-response-buffer ... ...))) (progn (let (... hgt-resp nline-resp) (with-selected-window ... ... ... ... ...))) (if (and proof-three-window-enable (> ... 10) (get-buffer-window proof-response-buffer)) (progn (let ... ...))) (when (and proof-three-window-enable (> ... 10) (get-buffer-window proof-response-buffer)) (let (... hgt-resp nline-resp) (with-selected-window ... ... ... ... ...))) optim-resp-windows() run-hooks(proof-shell-handle-delayed-output-hook) (let ((start proof-shell-delayed-output-start) (end proof-shell-delayed-output-end) (flags proof-shell-delayed-output-flags)) (goto-char start) (cond (... ...) (t ... ...)) (run-hooks (quote proof-shell-handle-delayed-output-hook))) proof-shell-handle-delayed-output() (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output)) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind (proof-shell-handle-delayed-output))) (if proof-shell-last-output-kind nil (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind ...)) (if proof-tree-external-display (proof-tree-handle-delayed-output cmd flags span))) (unless proof-shell-last-output-kind (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if (proof-shell-exec-loop) (setq proof-shell-last-output-kind ...)) (if proof-tree-external-display (proof-tree-handle-delayed-output cmd flags span))) (let ((span ...) (cmd ...) (flags ...)) (setq proof-shell-last-output (buffer-substring-no-properties start end)) (proof-shell-handle-immediate-output cmd start end flags) (unless proof-shell-last-output-kind (setq proof-shell-delayed-output-start start) (setq proof-shell-delayed-output-end end) (setq proof-shell-delayed-output-flags flags) (if ... ...) (if proof-tree-external-display ...))) proof-shell-filter-manage-output(648 648) (progn (setq endpos (match-beginning 0)) (setq proof-shell-last-prompt (buffer-substring-no-properties endpos ...)) (goto-char (point-max)) (proof-shell-filter-manage-output startpos endpos)) (if (re-search-forward proof-shell-annotated-prompt-regexp nil t) (progn (setq endpos ...) (setq proof-shell-last-prompt ...) (goto-char ...) (proof-shell-filter-manage-output startpos endpos))) (let ((urgnt ...) (prev-prompt pos) (startpos pos) endpos) (goto-char pos) (if (and urgnt ...) (setq startpos ...) (if ... ... ...)) (if (re-search-forward proof-shell-annotated-prompt-regexp nil t) (progn ... ... ... ...))) (if proof-action-list (let (... ... ... endpos) (goto-char pos) (if ... ... ...) (if ... ...)) (if proof-shell-busy (progn ... ...))) (if (not pos) (proof-shell-filter-first-command) (if proof-action-list (let ... ... ... ...) (if proof-shell-busy ...))) (let ((pos ...)) (if (not pos) (proof-shell-filter-first-command) (if proof-action-list ... ...))) (save-excursion (and proof-shell-eager-annotation-start (proof-shell-process-urgent-messages)) (let (...) (if ... ... ...)))

proof-shell-filter("\n<prompt>Coq < 9 run-hook-with-args(proof-shell-filter "\n<prompt>Coq < 9

0 < </prompt>")

0 < </prompt>")

(let ((saved-point ...)) (goto-char (process-mark process)) (set-marker scomint-last-output-start (point)) (insert string) (set-marker (process-mark process) (point)) (goto-char saved-point) (run-hook-with-args (quote scomint-output-filter-functions) string) (set-marker saved-point (point))) (save-current-buffer (set-buffer oprocbuf) (let (...) (goto-char ...) (set-marker scomint-last-output-start ...) (insert string) (set-marker ... ...) (goto-char saved-point) (run-hook-with-args ... string) (set-marker saved-point ...))) (with-current-buffer oprocbuf (let (...) (goto-char ...) (set-marker scomint-last-output-start ...) (insert string) (set-marker ... ...) (goto-char saved-point) (run-hook-with-args ... string) (set-marker saved-point ...))) (progn (with-current-buffer oprocbuf (let ... ... ... ... ... ... ... ...))) (if (and string (buffer-live-p oprocbuf)) (progn (with-current-buffer oprocbuf ...))) (when (and string (buffer-live-p oprocbuf)) (with-current-buffer oprocbuf (let ... ... ... ... ... ... ... ...))) (let ((oprocbuf ...)) (when (and string ...) (with-current-buffer oprocbuf ...)))

scomint-output-filter(#<process coq> "\n<prompt>Coq < 9

0 < </prompt>")

accept-process-output(#<process coq> 0.01 nil 1) (while (and proof-shell-busy (not quit-flag) (if timecount ... t) (not ...)) (accept-process-output proverproc accepttime nil 1)) (progn (while (and proof-shell-busy ... ... ...) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait"))) (if proverproc (progn (while ... ...) (redisplay) (if quit-flag ...))) (when proverproc (while (and proof-shell-busy ... ... ...) (accept-process-output proverproc accepttime nil 1)) (redisplay) (if quit-flag (error "Proof General: quit in proof-shell-wait"))) (let* ((proverproc ...) (accepttime 0.01) (timecount ...)) (when proverproc (while ... ...) (redisplay) (if quit-flag ...))) proof-shell-wait() (progn (message "%s buffer %s..." name buf) (funcall fn) (proof-shell-wait) (message "%s buffer %s...done." name buf) (sit-for 0)) (unwind-protect (progn (message "%s buffer %s..." name buf) (funcall fn) (proof-shell-wait) (message "%s buffer %s...done." name buf) (sit-for 0)) (unless (proof-action-completed action) (error "%s of %s failed!" name buf))) (let ((fn ...) (name ...)) (unwind-protect (progn ... ... ... ... ...) (unless ... ...))) (if (proof-action-completed action) nil (let (... ...) (unwind-protect ... ...))) (unless (proof-action-completed action) (let (... ...) (unwind-protect ... ...))) (save-current-buffer (set-buffer buf) (unless (proof-action-completed action) (let ... ...))) (with-current-buffer buf (unless (proof-action-completed action) (let ... ...))) (let ((buf ...)) (with-current-buffer buf (unless ... ...))) proof-protected-process-or-retract(retract) (if action (proof-protected-process-or-retract action)) (let* ((complete ...) (action ...)) (if action (proof-protected-process-or-retract action)) (unless (and ... ...) (setq proof-previous-script-buffer proof-script-buffer) (setq proof-script-buffer nil) (if ... ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode nil) (force-mode-line-update) (run-hooks ...))) (save-current-buffer (set-buffer proof-script-buffer) (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) (with-current-buffer proof-script-buffer (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) (if (buffer-live-p proof-script-buffer) (with-current-buffer proof-script-buffer (let* ... ... ...))) (proof-with-current-buffer-if-exists proof-script-buffer (let* (... ...) (if action ...) (unless ... ... ... ... ... ... ... ...))) proof-deactivate-scripting() (progn (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!"))) (if proof-script-buffer (progn (proof-deactivate-scripting) (if proof-script-buffer ...))) (when proof-script-buffer (proof-deactivate-scripting) (if proof-script-buffer (error "You cannot have more than one active scripting buffer!"))) (save-excursion (when proof-script-buffer (proof-deactivate-scripting) (if proof-script-buffer ...)) (proof-unregister-buffer-file-name (quote tell-the-prover)) (if proof-script-buffer (proof-deactivate-scripting)) (assert (null proof-script-buffer) "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer (current-buffer)) (if (proof-locked-region-empty-p) (proof-init-segmentation)) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if (and proof-query-file-save-when-activating-scripting ...) (save-some-buffers nil ...)) (if proof-activate-scripting-hook (let ... ... ... ...))) (if (equal (current-buffer) proof-script-buffer) nil (save-excursion (when proof-script-buffer ... ...) (proof-unregister-buffer-file-name ...) (if proof-script-buffer ...) (assert ... "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if ... ...) (if proof-activate-scripting-hook ...))) (unless (equal (current-buffer) proof-script-buffer) (save-excursion (when proof-script-buffer ... ...) (proof-unregister-buffer-file-name ...) (if proof-script-buffer ...) (assert ... "Bug in proof-activate-scripting: deactivate failed.") (proof-shell-ready-prover queuemode) (setq proof-script-buffer ...) (if ... ...) (setq proof-active-buffer-fake-minor-mode t) (force-mode-line-update) (if ... ...) (if proof-activate-scripting-hook ...))) proof-activate-scripting(nil advancing) proof-assert-until-point() (if (> (proof-queue-or-locked-end) (point)) (proof-retract-until-point) (if (proof-only-whitespace-to-locked-region-p) (progn ... ...)) (proof-assert-until-point)) (save-excursion (if (> ... ...) (proof-retract-until-point) (if ... ...) (proof-assert-until-point))) proof-goto-point() call-interactively(proof-goto-point nil nil)

[coqletsgo]

I'm having a very similar (if not the same) error using ProofGeneral 4.2pre120727 in Emacs 23.4.1 in Linux. I had the same behavior in my old ProofGeneral (4.1), but with a different error message:
"error in process filter: Attempt to delete minibuffer or sole ordinary window".

Upgrading to this PG version changed the error message, but not the behavior (which means everytime I switch buffers I have to wait several seconds before being able to do anything). However, the time to wait between switches seems to remain constant, between 7-15 seconds.

As a quick workaround, commenting the following lines on coq/coq.el seems to prevent it from happening:

;; Adapt when displaying a normal message

;(add-hook 'proof-shell-handle-delayed-output-hook 'optim-resp-windows)

;; Adapt when displaying an error or interrupt

;(add-hook 'proof-shell-handle-error-or-interrupt-hook 'optim-resp-windows)

[David Aspinall]

Thanks for the report and useful follow up, it looks as if the code tries to calculate a window height of the current script buffer without checking first that the window actually exists!

I've added a patch to today's release to check this and not adjust window heights in this case, could someone confirm it works please?

[coqletsgo]

Sorry for the delay, I skipped the notification mail...

I tried updating my copy of the CVS repository and running make, but I ran into an unrelated error (lib/unicode-tokens.el:865:4:Error: `(query-replace-descr (str) (if (eq str shortcut-regexp) "shortcut" str))' is a malformed function). Then I downloaded the release from the website and installed, and it seems to have worked. Thanks!

PS: I'm not sure if I should update the status to "fixed" or "worksforme", so I'll leave it unchanged. I believe it should also work for Damien.

[coquser]

Yes, the bug disappeared for me with the current CVS version (I had the same compilation error as "coqletsgo", I did [make -k] and I ignored it...). Thanks for the fix! But now the buffers are not always properly set in three window mode: when I launch PG and go to a point in a file, or when I go to a point in a different file, I get the *response* buffer instead of my file in the left-hand side window. This bug doesn't seem to appear when using only two windows. Damien

[courtieu]

This old bug is still opened. I close it. The problem of response buffer on the left should also be fixed.