Zed integration

[ShalokShalom]

Hi there :)

I plan to use F* for one of my projects, and see that it has editor support for VSCode, Emacs and a couple of other editors.

I do intend to create a Zed integration, so I can use it there.

Is there something specific about the F* LSP server, that is undocumented, or can people who implemented it already into other editors, give me advice?

I like to see, how this journey is going to work out. 🙂

[nikswamy]

F* itself does not implement LSP. It implements a custom protocol enabled by the --ide flag. fstar-vscode-assistant wraps that IDE protocol with LSP in TypeScript/nodejs. I believe that implementation of LSP enables integration into things like Vim etc. Not sure how Zed works, but I would think that using fstar-vscode-assistant's LSP may be the shortest path to getting something working. @gebner should be able to give more advice/details.

[gebner]

Yes, fstar-vscode-assistant has an LSP server which is independent of the vscode extension. If you go to the binary releases, there's a selfcontained javascript file for the LSP server. (Be aware: there's a separate, completely unmaintained, LSP server built-in in F*. Stay away from that one.)

Here's an example of a neovim plugin for F* built using that LSP server (from the vscode extension): https://github.com/gebner/VimFStar

If you're looking to create a zed extension you should take a look at the protocol extension we've implemented. They're listed in this file: https://github.com/FStarLang/fstar-vscode-assistant/blob/main/lspserver/src/fstarLspExtensions.ts There are two that are effectively mandatory: 1) verify to position, which tells F* to actually verify the desired part of the file, and 2) status notification, which is how the LSP server tells you what parts of the file have already been verified (which can take seconds to minutes and you need to know whether the file verifies successfully or if F* just isn't finished yet; in the vscode extension we show that in a green bar on the side of the editor).

[nikswamy]

(Be aware: there's a separate, completely unmaintained, LSP server built-in in F*. Stay away from that one.)

FYI, there isn't one anymore. It was removed some months ago.