server api

Stream: Machine Learning for Theorem Proving

[Daniel Selsam]

Does anyone have working code interacting with Lean 4 server with JSON only? Ideally from Python, with some way of discovering what features are supported by the server. :pray:

[Junyan Xu]

https://github.com/zhangir-azerbayev/repl probably? from this thread
For more features maybe take a look at https://github.com/leanprover/vscode-lean4

[Jason Rute]

In another thread (I’d have to look it up), someone suggested just finding a Python client for LSP servers in general. That would help with implementation (assuming such clients exist), but not discoverability.

[Scott Morrison]

@Zhangir Azerbayev, it would be nice to merge your PR for the python wrapper for the REPL back into the main repository. Are you still interested in doing that? There are some questions on your PR still from a while back.

[Zhangir Azerbayev]

Scott Morrison said:

Zhangir Azerbayev, it would be nice to merge your PR for the python wrapper for the REPL back into the main repository. Are you still interested in doing that? There are some questions on your PR still from a while back.

My bad, I had completely forgotten about this PR. I'll start implementing your suggestions right now.

[Jason Rute]

Does the REPL use the LSP server?

[Adam Topaz]

As far as I understand it uses essentially docs4#Lean.Elab.IO.processCommands directly

[Jason Rute]

Also, while we do have a client for the Lean 3 server, I don't know if it was a good idea. It isn't up-to-date with all the server features. For example, it doesn't handle widgets if I recall. Really the main advantage of that project is that is serves as an example of how to interact with Lean 3 via the language server, and a bad one at that since there is only or two examples. (I can trash talk it since I wrote a large amount of the code on top of a proof of concept by Patrick who again was just using it as an example of how to talk to the server from Python. I planned to add better documentation and examples, but never got around to it.)

[Jason Rute]

For Lean 4, I think a more useful thing would be good documentation for the Lean LSP server. (However, sometimes one wants more specialty use cases like a machine learning REPL and then it might make sense to build those out into tools for end users.)

[Daniel Selsam]

Jason Rute said:

In another thread (I’d have to look it up), someone suggested just finding a Python client for LSP servers in general. That would help with implementation (assuming such clients exist), but not discoverability.

Thanks! Yes, I think this is what I actually want. Leo pointed me to https://github.com/leanprover/lean4/blob/master/src/Lean/Server/FileWorker/RequestHandling.lean#L610-L622 for the API, with only the last two being Lean specific. I guess it is easy to just write/find a generic LSP client.

[Julian Berman]

I've used the server side pieces of pygls (a Python LSP implementation) pretty successfully.-- it does have a client as well (which I don't recall ever using). It uses asyncio unfortunately but otherwise is pretty reasonable (especially if you don't have strong opinions about Async IO Python frameworks). But I suspect it'd still be nice to have a thin layer on top of it, because even though LSP is standardized you still have to know a bit about which methods to call and what to send them, etc. -- it's slightly too low level for "hey send over this lean code and get back some state" I think.

[Julian Berman]

https://pypi.org/project/sansio-lsp-client/ is a better design probably, but seemed abandoned -- I made a note to some day poke at it, but not sure if it functions at this point.