-
Notifications
You must be signed in to change notification settings - Fork 232
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Separate data and control in the interactive protocol #981
Conversation
Testing this should be easy: I already updated fstar-mode, and this PR includes an updated OCaml snapshot (the a commit in this PR that sets the version number to 42 is there to make it easy for fstar-mode to detect when it needs to use the new JSON-based protocol; we should of course change this number before merging) |
GitHub has a nifty feature that lets you review a range of commit, btw; this should make it east to exclude the snapshot and #955. |
2897943
to
3420b45
Compare
Rebased on latest master (there was one conflict: 6946f10). |
3420b45
to
f8d822b
Compare
f8d822b
to
3d64f03
Compare
I can't be bothered to debug the obscure Windows-only OCaml issue.
bee004d
to
f226ab6
Compare
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.
c48c5bf
to
caf9323
Compare
@nikswamy Ok, I think this is ready for merging. It includes #955, so no need to merge that separately. Following our discussion:
I'll open a separate PR soon with new features based on this protocol. |
5fc26cd
to
31e67fe
Compare
Rebased and fixed conflicts. |
testing it on my branch now. will merge into master soon |
Apart from using JSON messages, the new protocol is essentially the same as the
old one. Significant differences:
etc) now cause F* to print a reasonably helpful diagnostic message.
contains the id of the corresponding query.
for consistency (all query names are now verbs).
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).
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.
“pop” any more — instead, the pop happens automatically.
Fixes #361, #366, and #828. This PR includes #955, so that one should be debated and merged first. I also added a small test suite for the new interactive protocol.