Proof process hang with bad tactics in Coq

[mgree]

When running the following script:

Theorem thm : True.
Proof. assert True.{ reflexivity. } apply H. Qed.

The proof process will hang when it gets to the first opening brace. I'm able to break things with C-c C-x, but some students have reported a general Emacs hang.

I'm running Emacs 26.3, Coq 8.10.2 (students are running 8.12.0), and ProofGeneral 20200623.1748. I'm on macOS 10.13.6.

[cpitclaudel]

The general Emacs hang seems surprising; do you / they have a repro? Otherwise, yes, there are many known ways to confuse the REPL, including defining notations that include periods or sending things to Coq that looks like sentence endings to Proof General. Migrating away from the REPL is the only robust solution here, I think.

[mgree]

I'm trying to work with students to get a repro, but (a) it's challenging with novices (this is a CS 2 course!) and (b) it's even more challenging with remote instruction. It could be that they're not aware of appropriate ways to break from the prover loop.

My understanding is that there are some longer term plans to switch to a better protocol... do you know where I can track that progress?

[cpitclaudel]

It could be that they're not aware of appropriate ways to break from the prover loop.

I think pressing C-c C-c should break out of that loop (:crossed_fingers:)

My understanding is that there are some longer term plans to switch to a better protocol... do you know where I can track that progress?

We don't really have progress being tracked, unfortunately

[hendriktews]

Hi, your line

Proof. assert True.{ reflexivity. } apply H. Qed.

is syntactically not correct, both coqtop and coqc report an error on it (just recording this here for those for which this is not obvious). Proof General hangs, because the Proof General parser decides to send `assert True.{` as one command to coqtop. For coqtop however, this is not a complete command, so it doesn't send a reply and then Proof General is waiting for ever. Emacs stays responsive, but the communication with Coq is in a deadlock. Instead of C-c C-x, which kills the prover, you can also try C-c C-c, which only sends an interrupt. This is also in the tool-bar and in the Proof General menu (Interrupt). I agree that it would be nice to get a decent error in Proof General for this example. However, I am not sure what could be done. We might be able to fix the regular expressions such that for this example Proof General sends a command that directly gives an error. But there will always remain examples that the regular expressions won't parse correctly... Therefore I don't think that improving the regular expressions makes sense. We could also add a timeout. But some proof commands take really long, therefore I don't think there exists a default timeout that satisfies both you and other power users... We could show a message on long running proof commands that hints on how to interrupt such things with C-c C-c.

[mgree]

C-c C-c does break for me, and such a hint or message would be helpful. I think this is the best course of action.

My memory says that sometimes C-c C-c doesn't work and C-c C-x is necessary, but I haven't been able to reproduce it. So, until students can help me out here, nevermind on that part.

I had not thought before about how Proof General knew what constituted a whole tactic. With Notations and Ltac in all its glory, it does seem challenging to get things right 100% of the time. That said, a tiny improvement here would save a great deal of trouble... if there were a way to be confident that it wouldn't regress behaviors for others' proofs.

[cpitclaudel]

C-c C-c does break for me, and such a hint or message would be helpful.

It's difficult to give a hint reliably, because Proof General has no way to know (when speaking to the REPL) whether Coq is busy computing or whether it's waiting for more input.

I had not thought before about how Proof General knew what constituted a whole tactic. With Notations and Ltac in all its glory, it does seem challenging to get things right 100% of the time.

Yes, it's insane. The proper way is to let Coq do the parsing :)

[mgree]

While it seems risky to try to patch up the regex parser, a different parser might be able to diagnose when to give the hint. One such policy might be: when a multi-character command doesn't end in .[:space:]*.

Alternatively, a tiny hint appearing in *response* or minibuffer or in a modeline somewhere after 1 second would be harmless. (Make the timer configurable, so setting it to nil turns off the behavior?) C-c C-c isn't a bad thing to be reminded of for a long running tactic anyway...

[cpitclaudel]

One such policy might be: when a multi-character command doesn't end in .[:space:]*.

We'd also want to rule the hint out for :{ as well as ..., I think.

Alternatively, a tiny hint appearing in *response* or minibuffer or in a modeline somewhere after 1 second would be harmless. (Make the timer configurable, so setting it to nil turns off the behavior?) C-c C-c isn't a bad thing to be reminded of for a long running tactic anyway...

Not a bad idea at all :) I won't have time to work on it but I'd be happy to review the code

[hendriktews]

Michael Greenberg <[email protected]> writes:

Alternatively, a tiny hint appearing in *response* or minibuffer or in a modeline somewhere after 1 second would be harmless. (Make the timer configurable, so setting it to nil turns off the behavior?) C-c C-c isn't a bad thing to be reminded of for a long running tactic anyway...

I suggest to use the minibuffer only (via message). Otherwise one would mess with the window layout, because the response buffer is not always visible. This is a Proof General hacker beginners task: - create a proof-shell internal variable for the timer - reset the timer on entry of proof-shell-exec-loop - set the timer after sending something to the proof assistant in proof-shell-exec-loop - display the message when the timer hits. - bonus: add a configuration variable to disable all that Whoever is interested, please pick it up - I am still busy with #352 and #439.

[mgree]

I was able to reproduce an Emacs freeze with a student today, with exactly the same example They were using Windows 10.

Using C-c C-c to interrupt the prover locked the Emacs entirely. Using C-c C-x worked.

EDIT: thinking about this more, I wonder if the issue is with the signal/process model on Windows. Dribs and drabs from old mailing list posts seem related to this issue, but nothing recent. Not sure when I'll have time to debug it, though.

[Matafou]

Hi,
given that neither emacs nor coqtop is in a loop during this freeze, I suspect indeed a problem with interrupt signals.
Can you give the repro please?

I agree with Hendrik: only coq can parse coq files correctly. In this particular case the error is due to the fact that { if just after an end of command is itself an end of command (because it starts a parenthesized script). Notice by the way that this is recursive: Proof. {{{{ is actually 5 different commands).

So it seems that in .{ the { is wrongly detected as an end of command whereas it is not since the . isn't.

I will try to fix this.
P.

[mgree]

To reproduce, enter the following into a coq-mode buffer named test.v on Windows:

Theorem thm : True.
Proof. assert True.{reflexivity.} apply H. Qed.

Put your cursor after } and hit C-c C-RET. Running C-c C-c will not work. After running C-c C-c, if I try C-c C-x, emacs hangs with "Retracting buffer test.v...". On my computer, Emacs eventually manages to stop Coq and control is returned to Emacs after, say, 30s; on a students' (less powerful) computer, the hourglass appeared and he killed Emacs before we could wait it out.

I'm sorry this isn't the best quality repro possible... 😕

[Matafou]

Thanks.
On my linux C-c C-c works immediately, so I guess this is a bug in coq for windows.

[mgree]

I should add that it works immediately on macOS, too---I suspect it's a platform-dependent SIGINT issue.

[Matafou]

I submitted a fix. It makes thing a bit more robust, but not perfect.