PG accepts garbage though Coq said "illegal begin of vernac"

[Matt McCutchen]

If I type the following complete garbage and press "C-c C-RET" at the end of the line, Proof General accepts it, even though I see in the *coq* buffer that Coq has said "illegal begin of vernac":

Check nat.&!&*\:,.:<*&^!)@)$.

I'm guessing that Proof General doesn't recognize the first period as a command separator and there's a miscommunication between Coq and Proof General regarding how much of the text was processed.

I'm using GNU Emacs 23.1.1 and Proof General 3.7.1, though I checked that the problem still exists in the latest Proof General from CVS.

[David Aspinall]

Many thanks for the report. Script management for Coq is still somewhat broken in current CVS, I'll try to have a look at this problem too when fixing it.

[David Aspinall]

Fixed: proof-script-command-end-regexp now allows any non-alphabetic character after a period to terminate a command. Hopefully correct.

[Erik Martin-Dorel]

Hello,

I reopen this ticket since I have just noticed that this Regexp change prevents from processing SSReflect libraries, because it breaks the parsing of all Coq notations that contain a period followed by a non-alphabetic character (for example, p .[ x ] do not work any more).

In fact I would virtually say that this report has more to do with a feature than a bug, all the more so as it is also reproducible within CoqIDE.

Thus we should definitely accept that ProofGeneral accepts such inputs.

Kind regards, Erik Martin-Dorel.

[David Aspinall]

Aha. I had worried about this, many thanks for pointing out. Have reverted the change in coq.el 10.51 now.

Considering this as invalid --- or at least, it's a detail we won't get perfectly right unless we change the interaction protocol or provide PG with a way to track the precise command end syntax.

[Robin Green]

In Coq trunk, I believe periods are not treated as end-of-command unless they are immediately followed by whitespace or end-of-line. (And therefore, multiple consecutive periods cannot be end-of-command - they must be something else, like a notation.) So that should be a simple way for Proof General to disambiguate periods as end-of-command from other uses of periods.

[David Aspinall]

Thanks for the note. Moved against 4.2.

[coquser]

I haven't tested the behavior of CVS proof general, but ... can also end tactic commands.

[Erik Martin-Dorel]

I have just test the behavior of CVS ProofGeneral and the "..." syntax seems to work smoothly.

However, as pointed out in #435, there is currently an issue with the parsing of some SSReflect notations such as "n.+1" (and "n.-1").

To reproduce the bug, you can for instance process the following Coq code:

Notation succn := Datatypes.S (only parsing).
Notation "n .+1" := (succn n) (at level 2, left associativity,
  format "n .+1") : nat_scope.
Check 5.+1.
Check 7.+1.

which leads to the following output in the *coq* buffer.

Welcome to Coq 8.3pl3 (December 2011)

(... snip ...)

<prompt>Coq < 10 || 0 < </prompt>Notation succn := Datatypes.S (only parsing).

<prompt>Coq < 11 || 0 < </prompt>Notation "n .+1" := (succn n) (at level 2, left associativity,   format "n .+1") : nat_scope.

<prompt>Coq < 12 || 0 < </prompt>Check 5.+
5
     : nat

<prompt>Coq < 13 || 0 < </prompt>1.
Syntax error: illegal begin of vernac.

<prompt>Coq < 13 || 0 < </prompt>

Kind regards,

Erik Martin-Dorel

[courtieu]

This has been solved a long time ago. I tested the Notations above and it works. I close the bug.