Proper protocol for communicating with F* process in interactive mode #828
Comments
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
The current protocol mixes control and data (and some control commands are valid source syntax!).
Nasty example (updated from #361) that typechecks from the command-line assuming
False, but fails to typecheck in interactive mode.See also #341
The text was updated successfully, but these errors were encountered: