Implement Language Server Protocol for painless editor integration

[artagnon]

The proposal is to have a new IDE mode for fstar fstar.exe --lsp implementing the Language Server Protocol. This has the primary benefit of getting editor plugins for free in any editor that implements LSP. For a prime example of a simple LSP client, see clangd-vscode. For a prime example of an editor extension that does a lot of work because coqtop does not implement LSP, see vscoq.

Our implementation of fstar.exe --lsp would be an augmentation of the LSP, since LSP doesn't support proof push/pop/state. See also: how Isabelle augments LSP.

Finally, LSP would push F* into supporting smarter editing features; things that are currently absent in fstar.exe --ide.

(Catalin: this was originally discussed on Slack)

[cpitclaudel]

This has the primary benefit of getting editor plugins for free in any editor that implements LSP.

As I mentioned on Slack, I don't think that is completely accurate: what you get for free is features that F shares with other languages, like jumping to a definition, or completion. But most of the effort required to add F support to a new IDE, in my experience, is the state management that comes from distinguishing between processed, unprocessed, and in-processing regions.

What LSP does do for you is track continuations, which would be nice on the Emacs side (in a typescript or javascript IDE, I'd expect async support to reduce the significance of this).

Another advantage of LSP is that it's less scary ; it might help draw contributors.

Finally, LSP would push F* into supporting smarter editing features; things that are currently absent in fstar.exe --ide.

We could open separate issues for these, since most of the effort (all, assuming an LSP backend ^^) will be implementing support for these features in F* proper. Do you have a list in mind?

[artagnon]

Finally, LSP would push F* into supporting smarter editing features; things that are currently absent in fstar.exe --ide.

We could open separate issues for these, since most of the effort (all, assuming an LSP backend ^^) will be implementing support for these features in F* proper. Do you have a list in mind?

I found the clangd list to be quite descriptive. The ones that apply to us, in my opinion, are:

• [ ] Formatting
• [X] Completion
• [ ] Diagnostics
• [ ] Fix-its
• [X] Go to Definition
• [ ] Signature Help
• [ ] Document Highlights
• [ ] Rename
• [ ] Source hover
• [ ] Find References
• [ ] Document Symbols
• [ ] Workspace Symbols
• [ ] Code Lens (?)
• [ ] Code Folding (?)

[cpitclaudel]

Relevant discussion on the Coq gitter: https://gitter.im/coq/coq?at=5cd9a7256fd7c11cd8b00644

[catalin-hritcu]

Relevant discussion on the Coq gitter ...

It seems that Emilio made LSP support in Coq depend on some big refactorings that got pushed to 8.11. Not sure how that is relevant to us though.

Update: More details about the status of vscoq here: https://github.com/siegebell/vscoq/issues/167

[artagnon]

I did significant research on LSP implementations in neovim, spacemacs, and vscode. I also read through fstar-mode.el.

The main proposal is to offload much of the complexity onto F* and lsp client implementations available in the editors. This would eliminate the code that fstar-mode.el uses to interface with company and company-help for (at the very least) fstar-subp-company-candidates, fstar-doc, and fstar-jump-to-definition functions: we'd get all those for free (along with suitable keybindings) with the lsp spacemacs layer. We'd also get the opportunity to simplify proof-state tracking and interfacing with proof-general by making smarter LSP-extension APIs like Isabelle does. I think we can also remove the spinner and tracking of busy-state, since LSP allows reordering responses as long as it doesn't break correctness — we can easily issue a $/cancelRequest to elegantly cancel a request, and avoid killing fstar.exe --lsp.

Yes, this is a lot of work on the F* side, but I think it will pay off once we get to the point of supporting multiple editors, and significantly shrinking fstar-mode.el. I've been rapidly hacking away at the problem, and #1742 is (almost) ready to merge, with #1744 in the pipeline.

[cpitclaudel]

Sounds great! A few points in response:

This would eliminate the code that fstar-mode.el uses to interface with company and company-help for (at the very least) fstar-subp-company-candidates

Beware that some of that code called from there is code for pretty-printing completions, in particular snippets. I don't think that code would go away.

, fstar-doc, and fstar-jump-to-definition functions: we'd get all those for free

Is there support for company-quickhelp in the Emacs LSP implementation?

(along with suitable keybindings) with the lsp spacemacs layer.

Is there a reason you focus on spacemacs instead of Emacs? Does spacemacs have anything lsp-wise that Emacs proper doesn't?

We'd also get the opportunity to simplify proof-state tracking and interfacing with proof-general by making smarter LSP-extension APIs like Isabelle does.

I'm puzzled, why is proof-general

I think we can also remove the spinner and tracking of busy-state, since LSP allows reordering responses as long as it doesn't break correctness

That sounds good, as long as we make F* parallel enough to handle queries while it's running a proof. Otherwise, I think exposing busy status is useful, since otherwise you can get confusing results like a 'jump to definition' jumping long past the time when you made the request.

Btw, there's logic like this in fstar-mode: if you initiate a jump to definition and then move the point before the response comes, it will ignore the response and not jump. How can you achieve this behavior in LSP?

— we can easily issue a $/cancelRequest to elegantly cancel a request, and avoid killing fstar.exe --lsp.

That sounds good (but currently we don't have to kill fstar --ide either; we send a sigint to the process to interrupt the currently-running query)

[artagnon]

, fstar-doc, and fstar-jump-to-definition functions: we'd get all those for free

Is there support for company-quickhelp in the Emacs LSP implementation?

We'd get that with either textDocument/hover or textDocument/codeLens, I think.

(along with suitable keybindings) with the lsp spacemacs layer.

Is there a reason you focus on spacemacs instead of Emacs? Does spacemacs have anything lsp-wise that Emacs proper doesn't?

spacemacs is simply Emacs with a nice ~/.emacs.d — better defaults, package management, and keybindings. Overall, it's much easier to get started with. Users can get lsp-mode for emacs too, albeit with a little more configuration.

We'd also get the opportunity to simplify proof-state tracking and interfacing with proof-general by making smarter LSP-extension APIs like Isabelle does.

I'm puzzled, why is proof-general

I assumed that fstar-mode would want to interface with proof-general in the future. No worries if this isn't the case.

I think we can also remove the spinner and tracking of busy-state, since LSP allows reordering responses as long as it doesn't break correctness

That sounds good, as long as we make F* parallel enough to handle queries while it's running a proof. Otherwise, I think exposing busy status is useful, since otherwise you can get confusing results like a 'jump to definition' jumping long past the time when you made the request.

Right; like I said: "without breaking correctness".

Btw, there's logic like this in fstar-mode: if you initiate a jump to definition and then move the point before the response comes, it will ignore the response and not jump. How can you achieve this behavior in LSP?

Either $/cancelRequest or simply ignoring the response, I would assume.

I have a question of my own: what's required for run_symbol_lookup to work? I'm assuming the tcenv needs to be initialized first — is vfs-add sufficient for this, or should I push the entire buffer with lax typechecking in order to get jump-to-definition to work at textDocument/didOpen?

[artagnon]

I'm having a problem with the spec of vfs-add/push. I'm sending the following query to fstar.exe --ide FooBar.fst, but I have no idea how to tell push to use Test.fst that I created on the virtual filesystem — it fails because FooBar.fst doesn't exist on the disk. The spec clearly states that the contents I send through vfs-add may correspond to a non-existent file; that's all great, but if push doesn't use the VFS, what's the point of having the VFS?

{"query-id":"1","query":"vfs-add","args":{"filename":"Test.fst","contents":"module Test\n\nlet rec fib n =\n  if n <= 1 then 1 else fib (n - 1) + fib (n - 2)\n"}}
{"query-id":"2","query":"push","args":{"kind":"lax","code":"module Test\n\nlet rec fib n =\n  if n <= 1 then 1 else fib (n - 1) + fib (n - 2)\n","line":1,"column":0}}
{"query-id":"3","query":"autocomplete","args":{"partial-symbol":"fi"}}

[cpitclaudel]

When you call fstar --ide, the file name you pass it what F* considers to be the 'current file'. When you do your first push, fstar reads that file, and its dependencies.

With you vfs-add, you told F about a file called Test.fst. But when you did your first add, F attempted to read FooBar.fst, and didn't find it.

So either you need to do a vfs-add for FooBar.fst, or you need to start fstar --ide with Test.fst.

that's all great, but if push doesn't use the VFS, what's the point of having the VFS?

Please, please, can we keep the tone a bit more friendly than this? My code is probably full of bugs, but let's not be too quick to assume that the features I took the time to document are pointless.

[artagnon]

When you call fstar --ide, the file name you pass it what F* considers to be the 'current file'. When you do your first push, fstar reads that file, and its dependencies.

With you vfs-add, you told F about a file called Test.fst. But when you did your first add, F attempted to read FooBar.fst, and didn't find it.

So either you need to do a vfs-add for FooBar.fst, or you need to start fstar --ide with Test.fst.

Got it, thanks! In the LSP implementation, I plan to not pass in a file and do everything with vfs-add.

that's all great, but if push doesn't use the VFS, what's the point of having the VFS?

Please, please, can we keep the tone a bit more friendly than this? My code is probably full of bugs, but let's not be too quick to assume that the features I took the time to document are pointless.

My sincere apologies 😰 — I will double-check my writing style for micro-aggressions before posting.

I wasn't assuming that it was pointless — my assumption was that someone added it for some reason at some point, and I hadn't figured out what that reason was: passing in a file to fstar.exe --ide seems to be a special case, as I know now. I will update the spec on the wiki with this clarification.

Please assume good faith always. I'm fully appreciative of your efforts on --ide!

[cpitclaudel]

passing in a file to fstar.exe --ide seems to be a special case

I don't understand this part :/ I don't think it's a special case. It's just that F* (either in --ide mode or in normal mode) expects a 'main file' that you're currently working on.

[artagnon]

I'm confused about a meta-issue: when editing multiple buffers, do you start different instances of fstar.exe --ide, one per buffer? Thinking about it some more, I think LSP works the same way: there's a different LSP server started in each buffer, since the overhead of keeping state of different buffers is an unnecessary complexity.

Now I'm confused about vfs-add again: is it used when the user creates different downstream dependencies of the "main file" that she does not flush to disk, and changes to the "main file" not yet flushed to disk? We can't type-check those not-yet-flushed changes, since push only works on the "main file" on the filesystem, right?

[cpitclaudel]

We start a separate instance of F per buffer, with one twist: if you jump to definition, we tie the buffer that we jump to to the original one, and share the F process (and long as you don't push code there). This allows you to do chains of jump-to-definition without repeatedly starting a new server.

vfs-add is useful because of the way dependencies are tracked in F*:

• All dependencies are loaded before starting to verify anything (that is, the dependencies of your entire file are loaded at once, before starting to process the current file)
• If you use FStar.SomeModule.someIdentifier anywhere in a file, then `FStar.SomeModule is a dependency of your file.

Because of this, F needs to see all of the current file before it can start processing any of it (worse: the whole file has to syntax-check, and before we did the --ide rewrite it would crash if your file had even a syntax mistake). So the first thing F does when you do your first push is it reads your entire file, all of its dependencies, etc — from disk.

This is a problem when you're modifying the file. Maybe you don't want to save it to disk just yet (maybe you opened a scratch buffer; maybe you're not sure about the changes yet; etc). So vfs-add tells F*: hey, when you read this whole file to check its dependencies, use this virtual file, not the actual contents on disk.

HTH

[catalin-hritcu]

There are 2 PRs for this ready to be reviewed and merged: #1742 and #1744