gistfile1.txt

artagnon   [May 6th at 9:38 AM]
I wish `fstar.exe --ide` implemented the Language Server Protocol; it would be really easy to do editor integration then: https://microsoft.github.io/language-server-protocol/ (edited)

19 replies

artagnon   [2 days ago]
The editor plugin for clangd is as simple as this: https://github.com/llvm-mirror/clang-tools-extra/blob/master/clangd/clients/clangd-vscode/src/extension.ts


catalin   [2 days ago]
@artagnon Does the Language Server Protocol support interactive proofs? And in case you missed it, here is a description of the protocol that @cpitclaudel, who knows a lot about IDEs for interactive proofs (in particular he maintains Company-Coq and ProofGeneral), developed for F*: https://github.com/FStarLang/FStar/wiki/Editor-support-for-F%2A#adding-support-for-new-ides (edited)


artagnon   [2 days ago]
@catalin That’s a good question, whose answer I’ve briefly investigated: see https://github.com/siegebell/vscoq/tree/master/server/src where siegebell essentially implements an LSP server on top of `coqtop`.


artagnon   [2 days ago]
Yes, I’ve seen that page, and fstar-mode for Emacs is quite complex — I’ve briefly looked at the source. If we want to support more editors, I figured that we need to make the editor support more painless.


artagnon   [2 days ago]
Isabelle’s VSCode integration is also achieved through LSP, albeit with a few extensions: https://github.com/seL4/isabelle/tree/master/src/Tools/VSCode/extension#isabelle-prover-ide-support


cpitclaudel   [1 day ago]
I think opening an issue in the fstar repo would be good.  I'm not an expert in LSP, and I think it has progressed since I wrote fstar-mode, but I can give a few reasons why I didn't go that way:
- The F* side was going to be much more complex (IIUC, you haad to diff new and old versions of the document to find out what had changed to be able to fit this into F*'s stack-oriented interaction)
- Multiple extensions would be needed to support goals and having a 'processing' status for each individual code fragment.
- LSP didn't have support for asynchronous messages from the server, which we use a lot in F* (for goals, and for module-loading messages)


cpitclaudel   [1 day ago]
I'd also be careful about mistaking the complexity of fstar-mode with the complexity of the protocol that it uses (there's a lot of code in fstar-mode because it does a lot, but the protocol part is fairly small)


cpitclaudel   [1 day ago]
Also, which IDE are you targetting? If VSCode, I already wrote a client in TypeScript for F* IDE protocol; could you reuse that? (edited)


artagnon   [1 day ago]
@cpitclaudel I think it does support async messages now. Whatever isn’t supported can be augmented, like in the Isabelle extension. Yes, I know the current F* protocol is very simple, and that LSP is more complex, but the complexity will be offloaded onto munging JSON on the F* side (pretty mundane), and all LSP clients can reap the benefits by being extremely simple. Can you link me to the TypeScript you wrote? I’ll open an issue, but I was thinking I should write it myself, in order to familiarize myself with the subset of F# that F* is implemented in. (edited)


cpitclaudel   [1 day ago]
I think it may be worth a try. My hunch is that you'll end up rebuilding the current F* protocol as extensions to LSP (I don't think LSP will remove the one hard bit, which is state tracking on the client side)


cpitclaudel   [1 day ago]
See https://github.com/cpitclaudel/fstar.js/tree/master/lib


cpitclaudel   [1 day ago]
In particular https://github.com/cpitclaudel/fstar.js/blob/master/lib/fstar.driver.ts


cpitclaudel   [1 day ago]
And the demo at https://people.csail.mit.edu/cpitcla/fstar.js/stlc.html


artagnon   [1 day ago]
I *think* Isabelle communicates state in its protocol: can you have a quick look at https://github.com/seL4/isabelle/blob/master/src/Tools/VSCode/extension/src/state_panel.ts and let me know if this is really the case?


artagnon   [1 day ago]
IIUC, the current F* protocol doesn’t implement many of the LSP features — adding an LSP client may push the protocol in the direction of providing those additional editor features.


artagnon   [1 day ago]
@cpitclaudel fstar.driver.ts isn’t terribly interesting: it simply launches `fstar.exe --ide` and does some fs-level book-keeping which can be done in many fewer lines of code using the vscode API. I’m also looking at https://github.com/cpitclaudel/fstar.js/blob/master/lib/fstar.ide.client.ts — from a quick read, it looks like push/pop are the main “features”; we’d basically get the baseline LSP features for free in the editor plugin (see clangd above), and augmentations would require a little bit of additional code (see Isabelle above)


artagnon   [1 day ago]
I’ve opened a new issue for this: https://github.com/FStarLang/FStar/issues/1736


cpitclaudel   [1 day ago]
>  can you have a quick look at https://github.com/seL4/isabelle/blob/master/src/Tools/VSCode/extension/src/state_panel.ts and let me know if this is really the case?

Sorry, no: I don't know anything about Isabelle.  All I meant that you need to have logic in the client that updates the appearance of each individual fragment of F* code as it is processed.

> fstar.driver.ts isn’t terribly interesting

I'm sure you didn't mean it that way, but this sounds agressive.  Can we keep this discussion friendly?

> see clangd above

This volume of code seems on par with what we need currently to support completion and jumps.  I'm not saying switching to LSP would make our worse (It might help, or it might not; I don't know).  All I'm saying is that there non-trivial UI work to make F* work in a new IDE, and in my experience the protocol isn't the most painful part of it (nor is it very big: switching from the old REPL protocol to the new JSON one didn't affect much of the Emacs client code, and these parts are the only ones that would be affected by a switch to LSP). (edited)


artagnon   [1 day ago]
> I’m sure you didn’t mean it that way, but this sounds a agressive.  Can we keep this discussion friendly?
Sorry! I definitely didn’t :sweat:
> This volume of code seems on par with what we need currently to support completion and jumps
Ah, this is good to know.
> there non-trivial UI work to make F* work in a new IDE, and in my experience the protocol isn’t the most painful part of it
Got it. I’m a little worried about book-keeping from the volume of code that vscoq ships — perhaps this worry is unfounded because `coqtop` is especially uncooperative; I don’t know; but you’ve urged me to dig a bit more before diving into LSP :smile: (edited)