How can we use Lean4 from Python?

Stream: lean4

[Daniel Donnelly]

https://github.com/leanprover-community/lean-client-python/issues/24

I've tried that for an example, and it fails.

[Eric Wieser]

(I posted some comments in the repo; the short answer is that there is no Lean Server Protocol any more, so I don't think we need our own client)

[Eric Wieser]

But someone here might be able to show you how to speak to the Language Server Protocol from Python.

[Daniel Donnelly]

@Eric Wieser Yes, that's what I need the closest related LSP documentation for Python/Lean4 comm. I'm not sure the architecture. Would man-in-the-middle be best? My end goal is to convert my commutative diagram data into Lean4 statements. I am aware of the CD widgets, but this is completely independent / a different approach from that. Found this article: https://medium.com/@malintha1996/understanding-the-language-server-protocol-5c0ba3ac83d2

[Eric Wieser]

Why don't you do it from within lean itself?

[Eric Wieser]

Lean can read in your data just like python, but it can construct Lean4 syntax accurately in a way that Python can't.

[Daniel Donnelly]

Eric Wieser said:

Lean can read in your data just like python, but it can construct Lean4 syntax accurately in a way that Python can't.

That sounds like the best laid plan for now. I will be learning some more Lean4 with my side project buddy.

[Daniel Donnelly]

@Eric Wieser who to ask how to rewrite designated insertion points of a .lean file, or would you just create a web routine that "grabs the objects"? In that case we should be sure that the diagram is pretty much edit locked I think...