-
Notifications
You must be signed in to change notification settings - Fork 10
Description
As suggested by @gebner in #20 (comment):
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 .out.expected files and CI would compare whether the output matches (similar to what we already have for the built-in IDE protocol: https://github.com/FStarLang/FStar/tree/master/tests/ide/emacs). This approach could cover a lot more code than unit tests, in particular we could also test the interaction with an actual F* process.
That script could take an .in file with one LSP request per line:
{"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 suggestion, that may need to be its own issue in the future, was:
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