You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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):
moduleTestlett=nat//^ textDocument/definition
The text was updated successfully, but these errors were encountered:
As suggested by @gebner in #20 (comment):
Another suggestion, that may need to be its own issue in the future, was:
The text was updated successfully, but these errors were encountered: