proof-shell-exit raises an exception "Buffer foo.v has no process"

[courtieu]

Hello, here is how to reproduce the bug:

open a coq file (say toto.v). proof script one line. hit C-c C-x <enter> yes <enter>

and you get this:

Debugger entered--Lisp error: (error "Buffer toto.v has no process")

process-send-eof() scomint-send-eof() (if proof-shell-quit-cmd (scomint-send-string proc (concat proof-shell-quit-cmd "\n")) (scomint-send-eof)) (catch (quote exited) (set-process-sentinel proc (lambda ... ...)) (proof-deactivate-scripting-auto) (proof-shell-wait (proof-ass quit-timeout)) (if proof-shell-quit-cmd (scomint-send-string proc ...) (scomint-send-eof)) (let (... ...) (while ... ... ...)) (when (memq ... ...) (message "%s, cleaning up and exiting...killing process" bufname) (kill-process proc))) (progn (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (if (and alive proc) (progn (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil))) (when (and alive proc) (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (let* ((alive ...) (proc ...) (bufname ...)) (message "%s, cleaning up and exiting..." bufname) (redisplay t) (when (and alive proc) (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil)) (proof-script-remove-all-spans-and-deactivate) (proof-shell-clear-state) (run-hooks (quote proof-shell-kill-function-hooks)) (if (and proof-multiple-frames-enable proof-shell-fiddle-frames) (proof-delete-other-frames)) (let (...) (dolist ... ...)) (message "%s exited." bufname)) proof-shell-kill-function() kill-buffer(#<killed buffer>) (let ((kill-buffer-query-functions nil)) (kill-buffer proof-shell-buffer)) (progn (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (or dont-ask (yes-or-no-p ...)) (progn (let ... ...) (setq proof-shell-buffer nil))) (when (or dont-ask (yes-or-no-p ...)) (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (buffer-live-p proof-shell-buffer) (when (or dont-ask ...) (let ... ...) (setq proof-shell-buffer nil)) (error "No proof shell buffer to kill!")) proof-shell-exit() call-interactively(proof-shell-exit nil nil)

[coquser]

The problem is coq-switch-buffer-kill-proof-shell and that proof-shell-kill-function does not take into account that a prover might get killed when scripting is deactivated.

Before kill-buffer inside proof-shell-exit actually kills the buffer and the process, it runs proof-shell-kill-function as part of the kill-buffer-hook's. proof-shell-kill-function deactivates scripting and therefore proof-deactivate-scripting-hook is run. For Coq this latter hook contains coq-switch-buffer-kill-proof-shell, which calls proof-shell-exit again. This looks like an infinite recursion, but before proof-deactivate-scripting-hook is run proof-script-buffer is set to nil, therefore the second recursive call to proof-deactivate-scripting does nothing.

The nested instance of proof-shell-kill-function kills Coq. However, the top-level instance of proof-shell-kill-function is not aware of this and tries to terminate Coq again, after proof-deactivate-scripting-auto returned.

I see two possible ways to fix this:

1. Inside proof-shell-kill-function set a global variable proof-shell-exit-in-progress. When coq-switch-buffer-kill-proof-shell sees this it refrains from calling proof-shell-exit recursively.

2. Change proof-shell-kill-function such that it can cope with the fact that provers die when scripting is deactivated.

Bye,

Hendrik

[David Aspinall]

Hi Hendrik, thanks for the diagnosis. Of course deactivate scripting was originally assumed not to kill the process. But now it may do for Coq, it seems best to try to make the code cope with this happening for any prover, so the second option would be the most robust. Would you like to propose/commit a patch? - David

[coquser]

I proposed solution 1 mainly because I think that the recursive call of proof-shell-exit is bad design.

Note that solution 1 would also work for any other prover, if they only respect the protocol to wrap calls to proof-shell-exit like

(unless proof-shell-exit-in-progress
  (proof-shell-exit t))

Bye,

Hendrik

[David Aspinall]

OK, I'm happy for you to commit that solution. Thanks - David.

[coquser]

Fixed with solution 1.

Hendrik