proof-shell: Don't ask about killing the proof assistant on exit

[hendriktews]

This PR is only about the commit in the title. To avoid conflicts, it builds on PR #791.

I have disabled this silly question about killing Coq when quitting Emacs decades ago already. IMO we don't need a user option to control this behavior.

[monnier]

• ;; If one quits Proof General, it's clear that the proof
• ;; assistant needs to be killed - don't ask.

[ Nitpick: the flag affects the behavior when one quits Emacs, rather than Proof General. I don't think we even have a clear notion of "quitting Proof General". ]

e.g. if we do M-x shell RET then C-x C-s, exactly as you say, "if we quit Emacs, it's clear that the nested shell needs to be killed", but Emacs will still ask for confirmation.

I'm not sure which behavior is better here (my own use of Coq is sufficiently limited that I don't think it's representative), but the main issue is whether killing the process would lose information, IOW it's whether the state of the process is likely to contain information that the user cannot trivially recreate (e.g. by restarting the process).

For M-x shell we consider that it's sufficiently common to have such important state (for example because the shell is currently running a command whose interruption would leave a mess).

[erikmd]

@monnier thanks for your feedback!

regarding your main point:

it's whether the state of the process is likely to contain information that the user cannot trivially recreate (e.g. by restarting the process).

it appears than unlike M-x shell processes, coqtop processes generally generally don't contain "critical state information", so I guess this amounts to a +1 for @hendriktews 's proposition.

[andreas-roehler]

Being in favour of the change.