PG goes into infinite loop with 100% CPU usage

[megacz]

To reproduce: download the attachment. Then type:

emacs -nw pg_bug3.v

Pick your nose while admiring the cromulent proof general splash screen.

Type "C-c ." to turn on electric terminator.

Move to the end of the file. Delete the existing period and re-type it.

Type a new period.

Watch your computer furiously increase the entropy level in the room.

FWIW, executing "coqc pg_bug3.v" reports an error, so this script clearly is not valid. However, the fact that PG goes into a 100% CPU usage situation is probably not the best reaction.

[David Aspinall]

This is indeed ugly, but it isn't PG's fault.

Instead of testing with coqc, try the interactive interpreter that PG runs, coqtop. You'll see that it goes into an infinite loop printing "Syntax error: Bad token".

You can switch to the *coq* buffer and hit C-c C-c there to interrupt, the script buffer C-c C-c function will refuse to do this unless it expects the prover to be busy. I'm uploading a tiny patch (for personal use) that relaxes this a bit but really this infinite loop is pretty much destined to bring Emacs to its knees.

Please report to the Coq team. Biased recommendation: try PG's Unicode Tokens instead of these unsafe Unicode characters.

[David Aspinall]

Patch to make C-c C-c in script buffers always cause a process interrupt

[megacz]

Hrm, I don't see anything about "unsafe" in the Unicode specification... what does it mean for a Unicode character to be unsafe?

Thanks for the patch. You sure you don't want to commit it? One of the most frustrating things in the world is when proof general won't let me interrupt Coq for one reason or another; it would seem to be wise to err on the side of sending the interrupt whenever the user asks for it, regardless of whether or not proof general thinks it's necessary...