Emilio Jesús Gallego Arias (Oct 06 2023 at 18:37): Emilio Jesús Gallego Arias (Oct 06 2023 at 18:37):Moving the topic of @Hugo Herbelin here as not hijack the main meeting thread:
@Hugo Herbelin I agree that could be interesting to discuss, I'd like to add some short comments to your questions:
1) what an LSP for proof assistants looks like (e.g. can we specify precisely the kind of extension needed to support proof assistants)
The answer is: we don't know. There is the issue that Ram opened ( https://github.com/microsoft/language-server-protocol/issues/1414 ) which was useful but may be now updated, a lot of things going on, specially on the Lean side.
There have been some papers trying to propose a LSP + Proofs , but so far I'm not sure they will get tracktion. Also, I'm aware they were some meeting among Lean and Isabelle developers about improving the stadnard, but I understand that at time the upstream LSP developers were not interested in ITPs (famous last words). I bet now they realize about their error given how popular Lean got.
2) what a server for such LSP extension looks like (e.g. is its API fully specified by LSP or does it have to include other components)
As of today, all proof assistants need extra APIs to extend the LSP protocol, there are some comparisons floating around I think, but is usually well-documented.
How the server looks? There is no real consensus here. The main task of a LSP server is to provide the user the info it needs as fast as possible, there are many ways to do that. coq-lsp was strongly influenced by Dune and Isabelle's answers to these questions. I am looking forward to learn how Lean works in this aspect.
3) eventually to understand how LSP compares to other protocols (e.g. Jupyter if ever the question makes sense).
It makes sense, they short answer is that they are quite different!
Emilio Jesús Gallego Arias (Oct 06 2023 at 18:37):LSP now includes some "notebook" support, but that's indeed could be seen as a bad property of LSP, in the sense that the base model was no general enough to handle notebooks properly.
Hugo Herbelin (Oct 06 2023 at 18:42):And conversely, are there things that LSP supports and that Jupyter's model would not support well?
Emilio Jesús Gallego Arias (Oct 06 2023 at 18:55):It's been a while since I looked at the iPython protocol, so I'm unsure Hugo. Back in the day there were indeed less support for things like code formatting, etc... but I wouldn't be surprised if that's a thing of the past.
Last updated: Oct 13 2024 at 01:02 UTC