Statement splitting incorrect in the presence of some notation

[RalfJung]

The following file compiles fine with Coq, but PG fails to step through it:

Definition ndot (n1 n2 : nat) := n1 + n2.
Infix ".:." := ndot (at level 19, left associativity).

Lemma name N x : (N .:. x) = (x .:. N).
Proof. Admitted.

[cpitclaudel]

Hi Ralf,

I don't think there's anything we can do about this with the current architecture; Coq doesn't expose parsing primitives to us, so we can only guess where sentences start and end.

Feel free to reopen if you feel that there's something we could do in this particular case; in general a good way to work around these problems is to use a symbol without dots; possibly a Unicode symbol (you can input them with company-match, with company-coq, or with the TeX input method in Emacs)

[RalfJung]

Closing the bug kind of makes it feel like you don't even accept that this is a deficiency. if you want to keep this bug separate from those that you think you can solve, GitHub has this handy "tag" feature :)

Considering the implementation... I'm not exactly sure what happens right now. Something is sent to Coq, and then everything freezes. Is it Coq that freezes? Or is it just giving an unexpected error back to PG, to which PG react badly? The latter could be improved.

Finally, of course, Coq does provide an interface better suited for IDEs than coqtop...

[cpitclaudel]

Closing the bug kind of makes it feel like you don't even accept that this is a deficiency. if you want to keep this bug separate from those that you think you can solve, GitHub has this handy "tag" feature :)

Don't read too much in a single bit of information :) It's definitely an issue, and there are many ways to run into it; notations are one; unmatched delimiters are another. I've added a help-wanted tag and reopened.

Considering the implementation... I'm not exactly sure what happens right now. Something is sent to Coq, and then everything freezes. Is it Coq that freezes? Or is it just giving an unexpected error back to PG, to which PG react badly? The latter could be improved.

PG sends stuff to Coq, and waits for an answer. Since what PG sent is not a full sentence, Coq waits for more input.

Finally, of course, Coq does provide an interface better suited for IDEs than coqtop...

Indeed; and if you follow the coq-club and coqdev mailing lists, I'm sure you've heard about my recent efforts in that direction :) Unfortunately the new API is not backwards compatible, isn't officially documented, and is still in flux. Of course, any help transitioning to that API is welcome.

[RalfJung]

Don't read too much in a single bit of information :) It's definitely an issue, and there are many ways to run into it; notations are one; unmatched delimiters are another. I've added a help-wanted tag and reopened.

Thanks!
This (maybe?) should also reduce the likelihood that this is reported as a duplicate, and/or gets lost.

So, the freeze is because Coq is waiting for PG to send more input, and PG is waiting for Coq to reply to the input it sent? Ouch.

Is there some "immediate" reaction that Coq always shows to input, even if that input happens to be a diverging tactic application?

[cpitclaudel]

Is there some "immediate" reaction that Coq always shows to input, even if that input happens to be a diverging tactic application?

Unfortunately not :/

[Matafou]

Note that coqide does not like your notation either... It fails more
gracefully though.

Let us say that this is a limitation of the current protocol used by PG: PG
is supposed to send exactly one complete command at a time, this is a
strong constraint on which the whole PG architecture is based. If it sends
an incomplete command (or more than one) it loses synchronization with the
prover (or get stuck). The splitting of a buffer into a list of complete
commands is made by pg in a syntactic way: mainly by detecting dots
followed by a space. Coqide does something similar.

The right way to do this would be to ask Coq itself to perform the
splitting of the buffer. Maybe once we switch to the xml protocol...

P.

2016-02-23 18:57 GMT+01:00 Clément Pit--Claudel notifications@github.com:

Is there some "immediate" reaction that Coq always shows to input, even if
that input happens to be a diverging tactic application?

Unfortunately not :/

—
Reply to this email directly or view it on GitHub
#58 (comment).

[ejgallego]

Just to mention than the following is not fully accurate anymore:

I don't think there's anything we can do about this with the current architecture; Coq doesn't expose parsing primitives to us, so we can only guess where sentences start and end.

Quite reasonable mechanisms are exposed now, even tho our current internal prototypes are based on full-buffer parsing or LSP.

[cpitclaudel]

Right, of course.
In the OP's case it's even simpler, too, because just sending a delimited query makes it possible for Coq to return the syntax error immediately.

[ejgallego]

We can make the good old coqtop take delimited queries easily, something such as --expect-0eol could be added if you folks would use it.