search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
490 stars 88 forks source link

Statement splitting incorrect in the presence of some notation #58

Open RalfJung opened 8 years ago

RalfJung commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 commented 8 years ago

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 https://github.com/ProofGeneral/PG/issues/58#issuecomment-187818365.

ejgallego commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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.