Separate data and control in REPL protocol #366
Labels
Comments
|
I think the current interaction protocol was a quick fix Nik implemented, but was never supposed to be the end of the story. We could of course try to incrementally improve it, but we could also look at the standard interaction protocols for proof assistants: in particular Proof General's (both the implemented one and the proposed replacement Proof Kit / PGIP http://proofgeneral.inf.ed.ac.uk/kit) and the more modern and less emacs specific PIDE (Prover IDE) framework which Isabelle and now Coq (http://www4.in.tum.de/~wenzelm/papers/coqpide.pdf) support. One more thing to look at: |
|
PGIP is mostly dead IIUC, and the current pG is just based on looking for prompts sent by a REPL. INRIA has been working on porting PG to Coq's custom XML-based async protocol. CoqPIE is just a UI on top of the regular REPL-based |
cpitclaudel
added a commit
that referenced
this issue
Apr 13, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 13, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 13, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 13, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 14, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 14, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 14, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 14, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 17, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 18, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 18, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 18, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
cpitclaudel
added a commit
that referenced
this issue
Apr 18, 2017
Apart from using JSON messages, the new protocol is essentially the same as the old one. Significant differences: - Instead of crashing, invalid requests (missing fields, unsupported queries, etc) now cause F* to print a reasonably helpful diagnostic message. - Each query now includes an editor-supplied query id, and each response contains the id of the corresponding query. - Some of the queries were renamed (info → lookup, completions → autocomplete) for consistency (all query names are now verbs). - Messages that F* used to print to stdout or stderr are now translated into proper JSON messages and labeled with a severity level (a review of these messages is needed to decide which of these should be turned into properly reported errors or warnings including range information). - F* now prints the protocol's version and a list of supported interactive features before starting the interactive loop. This lets the Emacs mode do dynamic capability detection instead of relying on version numbers. The same information is available through a new "describe-protocol" query. - A failed “push” doesn't require the editor to immediately send a corresponding “pop” any more — instead, the pop happens automatically. Fixes #361, #366, and #828.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
See #361 to see why combining the two is a bad idea and how it's done in Dafny.
The text was updated successfully, but these errors were encountered: