Comments (9)
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)
from pg.
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...
from pg.
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.
from pg.
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?
from pg.
Is there some "immediate" reaction that Coq always shows to input, even if that input happens to be a diverging tactic application?
Unfortunately not :/
from pg.
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 [email protected]:
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).
from pg.
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.
from pg.
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.
from pg.
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.
from pg.
Related Issues (20)
- `coq-accept-proof-using-suggestion 'always` incorrectly believes that `proof` is a proof directive HOT 4
- Hitting 'tab' to indent just throws an error HOT 6
- Broken link in Ch. 11 of User's Manual
- ProofGeneral does not handle "Proof term." directives HOT 11
- Feature request: sparate commands for jumping to current point with/without omitting proofs HOT 7
- *response* buffer only showing last output HOT 3
- Tons of warnings when using certain PG features HOT 11
- "Omit proof" on a Let in a section leads to warning HOT 14
- "Omit proofs" breaks other proofs because it also skips hints HOT 14
- whitelist for admissible commands inside proofs HOT 17
- PG incorrectly interprets `}.` as a single token, which results in incorrectly accepting files that coqc rejects
- test_wholefile.v incompatible with 8.17 HOT 1
- Scheme ... with is indented improperly HOT 1
- Merging the Abella fork of PG HOT 9
- Automatic indenting for Easycrypt HOT 1
- generic/pg-goals.el shouldn't be executable HOT 1
- confusing error on incorrect _CoqProject file
- Colors don't work in emacs-nox HOT 1
- Compile-before-require setting does not presist HOT 1
- `coq-insert-suggested-dependency` sometimes inserts unparsable statements
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from pg.