Optional timeout warning when waiting for the proof shell

[andyqhan]

With bad tactics in Coq (#514), Proof General will hang forever (but can be interrupted with C-c C-c or C-c C-x). In response to @hendriktews's workaround suggestion, this PR exposes a variable proof-shell-timeout-warn that, if an integer, enables a minibuffer warning after waiting on the proof shell for more than proof-shell-timeout-warn seconds.

It doesn't fix the core issue, but the minibuffer warning will remind users of using C-c C-c and C-c C-x to cancel scripting.

The text of the warning is "This command is taking a while. Is it malformed? Do C-c C-c or C-c C-x to abort." Default timeout is 30 seconds.

[Matafou]

Sorry for the delay, I will review your PR shortly. Thanks for it!

[Matafou]

I am not sure this test is necessary. Why would the shell be busy if an error is detected? Probably not harmful.

[andyqhan]

I left it in, but can remove if you'd like.

[Matafou]

General remarks. Other remarks in the code.

• You should probably not make a PR from your own "master" branch. You should define a dedicated branch in you repository instead. No big deal.
• While testing I noticed that the message is displayed sometimes apparently for no reason. It seems this happens when PG processes comments. Maybe because in this cases PG do not send anything to coq actually, and this gets no response either. Probably a missing cancel-timer somewhere. I will investigate a bit more.
  This almost good I would say.

[Matafou]

• Probably a missing cancel-timer somewhere. I will investigate a bit more.

It is just that the timer should not be launched when the semi's type is 'comment.

[andyqhan]

@Matafou I've implemented your suggestions — thank you so much for the review!

• You should probably not make a PR from your own "master" branch. You should define a dedicated branch in you repository instead. No big deal.

My bad, I'll make sure to do that in the future.

• While testing I noticed that the message is displayed sometimes apparently for no reason. It seems this happens when PG processes comments. Maybe because in this cases PG do not send anything to coq actually, and this gets no response either. Probably a missing cancel-timer somewhere. I will investigate a bit more.

I changed the conditional for arming the timer to:

(if (and proof-shell-timeout-warn
         (not (eq (caar semis) 'comment)))

I'm not sure whether this is what you had in mind.

[hendriktews]

Thanks for your contribution!
In #514 I described an approach that sets and clears the timer for each command sent to Coq. Instead, your approach is to set and clear the timer only once for each asserted region. This is also possible. However, you need to consider two points.

1. Comments, as pointed out already by @Matafou: If the asserted region consists only of comments, then proof-add-to-queue might process them without calling proof-shell-exec-loop. Checking whether the first element is a comment (as you do now) is not good enough, because the asserted region may consist of a mixture of comments and real commands. If you want to stick to your approach, I suggest to move setting up the timer to proof-add-to-queue after the leading comments have been processed there.
2. quickly asserting twice: I believe it is possible to assert another region while the previous region is still processing. In this case, you will never kill the timer for the first region.

[hendriktews]

The indentation seems wrong here. Would it be possible to fix that?

[andyqhan]

Thank you for the speedy review.

I'm reconsidering the need for this PR, because I can't seem to get the MWE given in #514 to hang (probably because of the fixes in 0fdb1ae, I'm getting Syntax Error: Lexer: Undefined token). However, if the maintainers still think there's a need, I'd be happy to continue working on this feature — it's just that not being able to reproduce the hanging anymore means that I have trouble working on it further.

[Matafou]

If you want a script where coq still hangs you can use this:

Lemma foobar: True.
Proof.
  idtac.+ }

[andyqhan]

Ok, I believe I've fixed the issues. I'm not quite sure what to do with the case when someone can assert quickly multiple times in a row (the timer won't start if it's already running — that may help), but it now doesn't start the timer if the processed region was all comments. In order to do this, per @hendriktews 's suggestion, I've moved setting the timer to proof-add-to-queue, and arm the timer only when the length of proof-shell-slurp-comments is less than the length of proof-action-list (that is, when the region isn't only comments). Could someone take a look?

[Matafou]

It seems to work, but is it really what we expect?
When one launch a big thunk of coq commands, if the global execution of the whole thunk takes more that 30sec we get the message. One would expect that we put a timer on each command. No?

[hendriktews]

It seems to work, but is it really what we expect?

No. It seems that my comment from March 21, that the approach followed here is also possible, was wrong. I would suggest to follow my outline in #514 instead.

[andyqhan]

I moved the timer setup to proof-shell-insert, which should mean that it is armed per command and not per region. I tried putting it in proof-shell-exec-loop like hendriktews suggested, but it seems that if a command hangs, that function isn't called. In order to deal with the fact that a region can take more than proof-shell-timeout-warn seconds to complete, I cancel the timer before setting it if the timer exists. Also, I'm checking that the argument of proof-shell-insert is a visible command by checking that the callback is 'proof-done-advancing — I'm not sure whether this is the best way.

(I believe those two tests are failing because of some problem fetching from Docker servers? Not sure)