search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Is there a similar client impletation for Lean 4? #25

Open LAWArthur opened 1 month ago

LAWArthur commented 1 month ago

I'm trying to work on a project with Lean 4, which requires communicating to lean4 process (maybe via LSP) and stands alone from vscode or web or React.

However, the current clients I've found in the project are somehow highly nested with those platforms and I've struggled but failed to pick them out.

So I'd like to ask if you have any suggestion of how to implement one like this in Lean 4 or instruction of extracting one from existing project?

jasonrute commented 1 month ago

This project isn't much more than a thin python wrapper around the Lean 3 JSON-based language server. The most important thing it does is properly handle the async communication via the trio library. (It also makes the API into some data classes, but that isn't necessary, nor is it perfect since, for example, the widgets API is not properly supported.)

Lean 4 has a similar JSON-based language server. It wouldn't be hard for you to modify this code (forgetting about the tests and data classes) to use that language server. (The Lean 4 language server is also an LSP server, so you may even be able to find an LSP Python client.)

Moreover, I'm not sure of your use case, but note that there are many ways to interact with Lean 4 from Python. The language server is just one way. You can also use Lean metaprogramming (the fastest way) or just call Lean from the command line (the simplest way). It might be worth having a discussion about your aims at leanprover.zulipchat.com