ProofGeneral stalls/loops on ...

[coquser]

Goal True.

...

Evaluating this script (the "..." is literal) will cause PG to loop forever/stall while it waits for Coq to respond.

[coquser]

Similarly with

Goal True.
  idtac; ...

However,

Goal True.
Proof with easy.
  idtac...
Defined.

correctly goes through and solves the goal.

[coquser]

The following patch fixes it for me. It's not too pretty, though.

--- coq-indent.el.~11.24.~	2015-01-27 04:27:09.000000000 -0500
+++ coq-indent.el	2015-04-27 15:04:47.537983825 -0400
@@ -326,6 +326,13 @@
                             (goto-char (match-beginning 1))
                             (not (coq-empty-command-p)))
                         nil)
+                      (and (string-equal (match-string 1) ".")
+                           (save-excursion
+                             (goto-char (match-beginning 1))
+                             (skip-chars-backward ".")
+                             (skip-chars-backward " \t\n")
+                             (left-char)
+                             (looking-at-p "[^a-zA-Z_][ \t\n]*\\.\\.\\.")))
                       (and
                        (goto-char foundend)
                        (proof-buffer-syntactic-context))))

The real problem is in the definition of coq-period-end-command, which considers ... to be a sentence terminator in all cases (it is only when preceded by at least on alphabetic character (and possibly whitespace):

(defconst coq-period-end-command
  "\\(?2:[^.]\\|\\=\\|\\.\\.\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\'\\)")

This could be a coq error though. Are there examples of ... as a command starter?

-- cpitcla

[courtieu]

Hi,

Indeed this is a strang coq-8.4 behavior that seems fixed in v8.5.

v8.4 seem to be waiting for more input, and only after seeing a "." does he detect that ... is misplaced.

Maybe not worth fixing? Feel free to reopen if you feel the need. P.