Refactor LSP Server to allow for mocking out I/O bits #20
Conversation
Allows for easier testing of the extension by mocking out the I/O bits, the connection and DocumentManager.
|
Note that I haven't included any tests in this PR yet. It's still a work in progress. I plan to first verify that I can import pieces of this for unit tests before I mark this ready for review. Since it's also such a large PR, I plan to try to use it for a day or two first to make sure I didn't break anything at a surface level. |
These tests use the jest framework and mock out dependencies. The jest types conflict with mocha types, however mocha isn't currently being used so I removed it as a dependency. Mocha cannot mock out dependencies so it's not a viable alternative here to jest.
|
I added some tests that I think demonstrate the value of this refactoring. The tests mock out the server, connection, and internally called functions that are irrelevant to the given test. Jest makes it easy to mock out everything in a module, so having separate files makes it easy to mock out server and connection objects separately. Furthermore, since connections and servers are only established in |
There was a problem hiding this comment.
Hi Kirby!
This refactoring is really great and goes in exactly the right direction. I am a bit lukewarm about the concrete test case though. I don't think the fragmentation code should exist in this form at all, and neither should the tests.
Do you have any plans for the F* vscode extension? We're also planning to add a couple new features. Happy to coordinate with you.
A good next step would be to make a class for the F* IDE process connection. This class could then contain a lot of the protocol handling that is now in the fstar_handlers.ts file. Another good change could be to turn DocumentState into a class and move all of the file-specific code there.
Gabriel
| code: text | ||
| } | ||
| }; | ||
| // TODO(klinvill): This interaction with the F* executable should be moved to the FStar class or file. |
There was a problem hiding this comment.
I have no idea why we don't send a request to the F* IDE process we already have. @nikswamy Is there a reason we need to spawn a fresh F* process here?
Either way, this should be async.
|
Hey Gabriel, thanks for the review and suggestions! I'm just getting around to these comments now after the holidays but will try to address them over the upcoming week.
I generally agree, but the fragmentation code is in there to resolve #18. It seems like this is occurring on the Javascript side. There's a NodeJS buffer property that might be able to increase the buffer size before messages get fragmented, but I'm not sure what a proper size for the buffer would be. However, I think potentially removing fragmentation should be the target of another PR (for which I can open an issue) and this PR should be focused on the refactoring. I could remove the test in that case. What do you think?
Not at this time, this refactoring was mostly just to enable me to test another PR I made introducing the fragmentation behavior (#19). I'm happy to help with further changes/refactoring though!
Yup, that sounds good to me and would fit in well with this PR. I'll take a stab. |
This change is meant to fix the bug Gabriel pointed out where the handlers could operate on stale configurations if they close over configuration settings. I instead opted here to refactor the handlers to not be factory functions unless they really need to (e.g. to close over the private buffer for `handleFStarResponseForDocument`). The other functions can simply take the server parameter as an argument when called. The server should be passed by reference so it is not expensive to pass it with each function call.
As a consequence message fragments should never be delivered out-of-order.
This change is made as per Gabriel's suggestion that the bind semantics are hairy (FStarLang#20 (comment)).
In addition to introducing the new FStarConnection class, this commit introduces a custom Result type as well as a couple of custom Error types that make it possible for the code that wraps the F* interactions to be fully decoupled from the LSP connection (e.g. errors are returned using Result and Error objects instead of sent over a ClientConnection). Additionally, this commit moves the message buffering logic to the FStarConnection class and exposes a 'message' event type on top of that buffering logic. Further refactoring is needed to get rid of fstar_handlers.ts entirely. Further refactoring should also likely be done to combine FStarConnection and FStar.
The key idea with this commit is that only the classes that wrap F* should worry about parsing messages from F*. Consumers of those messages (e.g. the LSP server) should be able to interact with those messages using a higher-level interface. In this case I decided to emit custom events for each message that was previously being parsed. This commit also introduces parsers and interface checkers for each of the possible F* messages. Most of these methods are not used and could be removed to reduce the codebase that needs to be maintained, but ideally there should be a clean way to parse the messages and tell what kind of message they are.
Oh I'm so sorry, I worded that remark a bit too strong. What I meant is that the fragmentation code should only look at newlines, and not worry about any reordering (since that won't happen). The part of the code that shouldn't exist is that part that tries to parse the request. As you've noticed, nodejs provides a relatively low-level interface with a maximum buffer size. (In other words, it looks very much like the good old |
| @@ -0,0 +1,9 @@ | |||
| /// Basic Result type similar to Rust | |||
| export type Result<T, E extends Error> = Ok<T> | E; | |||
There was a problem hiding this comment.
It's really uncommon to use a result type in javascript, and it lacks the syntactic sugar (i.e., postfix ?) that makes them ergonomic to use in Rust. I'd rather go with good old-fashioned exceptions instead.
There was a problem hiding this comment.
There's a few reasons I thought a result type was important to introduce:
- I needed a way to decouple the alerts that are sent to the LSP client from errors that occur when communicating with F*. Previously all the F* communication bits had to take the LSP client connection so they could send alert messages when errors occurred.
- The Result type makes the kinds of errors that can be returned explicit in the type annotation (with
Errorbeing a catchall). This is useful because the F* handlers only send alerts on some error messages (e.g. not if an alert has already been sent as a result of a previous F* error). The explicit error types make it clear what specific kinds of errors a function may return. To my knowledge, it's not possible to annotate (outside of comments) what exceptions can be thrown, making it more implicit than if we used an explicit result type.
Given those reasons, do you think it's still better to go with exceptions instead?
There was a problem hiding this comment.
I needed a way to decouple the alerts that are sent to the LSP client from errors that occur when communicating with F*. Previously all the F* communication bits had to take the LSP client connection so they could send alert messages when errors occurred.
IMHO the proper way to decouple this is to add an processDied: Event<{exitCode: number}> on FStarConnection.
AFAICT the only thing we can do about a dead F* process is to inform the user. So there's no reason to have separate error handling code in every request handler. We should just throw an exception (and thus abort).
This is useful because the F* handlers only send alerts on some error messages [...]
Is there any other case where this happens right now except for "process died"?
Given those reasons, do you think it's still better to go with exceptions instead?
For unrecoverable errors like "process died," I think we should definitely go with exceptions.
In other cases, I think it's better to use an ADT. Like in the responses returned by F*, which can be either success or failure. But there I'd just pass the typed JSON value around:
type IdeResponse<T, E> =
{ kind: 'response', 'query-id': string, response: T, status: 'success' } |
{ kind: 'response', 'query-id': string, response: E, status: 'failure' }There was a problem hiding this comment.
AFAICT the only thing we can do about a dead F* process is to inform the user. So there's no reason to have separate error handling code in every request handler.
Yeah that makes sense to me. You could try to run a new F* process as well, but this would still be something that should be handled at a process level rather than at a request level.
This is useful because the F* handlers only send alerts on some error messages [...]
Is there any other case where this happens right now except for "process died"?
I believe this only happens for "process died". There's also special behavior around ignoring validation queries if F* doesn't support full buffer queries, but this seems like one-off behavior that may not be relevant anymore and could just be rolled into an exception/error.
| const textDoc = documents.get(textDocumentPosition.textDocument.uri); | ||
| if (!textDoc) { return {contents: ""}; } | ||
| // The onHover handler is called when the user hovers over a symbol | ||
| // The interface requires us to return a Hover object *synchronously* |
There was a problem hiding this comment.
This comment is really wrong BTW. The LSP library is fully async. (I know you only moved it around, it was already there.)
| // - 'message:ide-auto-complete': emitted for each auto-complete message, | ||
| // emits the response as an `IdeAutoCompleteResponses` object. | ||
| private emitPerMessage(stream: Readable, msg: object) { | ||
| stream.emit('message', msg); |
There was a problem hiding this comment.
I didn't know you could send your own events on a Readable. It feels like a bit of a layering violation though.
FWIW, I would have used the typed Emitter/Event API from vscode-jsonrpc. (The vscode extension API has another copy of it called EventEmitter/Event.)
There was a problem hiding this comment.
It turns out that Streams in general are instances of Node's untyped EventEmitter.
That's nice that vscode exposes a typed version though! Do you use that API in the Lean extension?
There was a problem hiding this comment.
Yes, pretty heavily. See for example here: https://github.com/leanprover/vscode-lean4/blob/b3e8da84bc860ba4c2841f67cc29f5b0bfe94cba/vscode-lean4/src/leanclient.ts#L57-L92
Including yet another custom version of course: https://github.com/leanprover/vscode-lean4/blob/b3e8da84bc860ba4c2841f67cc29f5b0bfe94cba/lean4-infoview/src/infoview/event.ts
|
If we want to merge parts of this PR early, I think 4e9697e would be a great cut-off point. |
|
Just to throw an idea out there. I have just chatted a bit with Nik and we think it would be amazing to have tests at the LSP level. That is, write a small script that spawns the LSP server, passes some requests to it, and prints the responses to stdout. The output would be checked into git as That script could take an {"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///Test.fst","languageId":"fstar","version":1,"text":"module Test\nlet t = nat"}}}
{"jsonrpc":"2.0","id":1,"method":"textDocument/definition","params":{"textDocument":{"uri":"file:///Test.fst"},"position":{"line":1,"character":10}}}Another really cute trick is to generate these requests from comments in the file (which we've been doing in Lean): module Test
let t = nat
//^ textDocument/definition |
Yeah as I was working on refactoring out fstar_handlers I started realizing that it'll take a major refactor to do it right. I'll create a new PR (#22) for up through 4e9697e, I think that's probably the cleanest way to do this at this point. |
Definitely sounds like a good idea to me. I opened #26 to track this. |
This PR is a massive refactoring for the LSP server aimed at making testing easier. Specifically, the LSP server is factored out into a class that is constructed using a given client connection and document manager. This is essentially the dependency injection pattern, which should ideally make it easy to mock these components out for testing. Since we would need to potentially import the server without setting up a connection when testing, I've refactored the code that actually creates the client connection, document manager, and server out into
main.ts.Since this is a major refactor, I went ahead and tried to refactor out related components into smaller files, so the F* bits have been refactored out into their own file.