I would like to report three interrelated issues that I noticed in the
current CVS version of ProofGeneral.


1. Now the behavior of [C-x C-c] is not really consistent with the one of
[C-c C-x].
Indeed, the second command calls yes-or-no-p before killing the
prover, while the first one now exits Emacs silently!
By the way, it is neither consistant with, e.g., the behavior of the
interactive OCaml toplevel that we can run with [M-x run-caml].

I propose two different suggestions:

1.1. Get back to the previous standard behavior, namely remove
in generic/proof-shell.el:
;; PG manages the prover process, don't query user on exit
 (get-buffer-process proof-shell-buffer) nil)
The advantage of the previous behavior is is that it prevents the user
from inadvertently shutdown his session.

1.2. Otherwise, in order to make both behaviors possible,
create a custom option `proof-query-on-exit' and
a function with the same name that updates the flag accordingly.


2. Moreover, the command [C-c C-x] does not take into account its
optional argument DONT-ASK, which would be very useful either
(namely, allowing the user to do [C-u C-c C-x] to skip the invocation
of yes-or-no-p itself).
To fix this, I believe
(defun proof-shell-exit (&optional dont-ask)
should be replaced with
(defun proof-shell-exit (&optional dont-ask)
 (interactive "P")


3. Finally, it seems the function `proof-shell-exit' raises
systematically an unexpected error.

To reproduce it, run the (Coq) prover, then try:
[M-: (setq debug-on-error t) RET]
[C-c C-x]


Hoping you will be able fixing these issues for the pending release.

Kind regards,


PS: I use Coq-8.3pl2 and GNU Emacs 23.3.1

√Črik Martin-Dorel
PhD student, ENS de Lyon, LIP
ProofGeneral-devel mailing list

Reply via email to