Skip to content
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

Handle fragmented messages from F* by storing fragments in a buffer #19

Merged
merged 2 commits into from
Dec 20, 2023

Conversation

klinvill
Copy link
Contributor

Resolves #18.

Messages from F* larger than 8192 bytes seem to get fragmented into multiple messages when read by the language server. This typically results in invalid JSON messages when this fragmentation occurs. This PR supports re-assembly of fragmented messages under the assumptions that:

  • fragmented messages will always be delivered sequentially and in-order
  • messages that are not valid JSON are always fragmented messages

I'm opening this as a draft PR since I'd like to add unit tests for my changes, but am running into some difficulties that might be best addressed by refactoring (e.g. loading the server module that contains the handlers currently requires a connection for the server).

Several assumptions are made in this implementation including that
fragmented messages will always be delivered sequentially.
The function really checks if a message from the F* executable is valid,
rather than a message from the IDE. This renaming captures that meaning.
@nikswamy
Copy link
Contributor

Thanks Kirby! This looks great.

If there's a way to add a unit-testing framework that would be amazing and useful beyond the scope of this PR. Unfortunately, at the moment, my testing is limited to trying out the extension for a bit and seeing if it works for a bit ... clearly inadequate.

I'll try your PR out to see if it works well for me. If it does, I'd be open to merging it, while perhaps separately we try to figure out what a unit test framework for this extension would look like.

@klinvill
Copy link
Contributor Author

Ok sounds good! I've been working on some potential refactoring that I think should make it easier to unit test (and mock out the I/O bits), but it's turning into quite the overhaul. At this point that probably belongs in a separate PR.

@klinvill klinvill marked this pull request as ready for review December 16, 2023 19:50
@nikswamy
Copy link
Contributor

Thanks Kirby. Finally got around to testing this. It works well for me ... merging.

@nikswamy nikswamy merged commit d0c9ae2 into FStarLang:main Dec 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants