Is there any spec for Lean server protocol?

Stream: new members

[Grigoriy Prokhrov]

I try to find it in the community documentation and via google but found nothing. The lean --server gives only stdin cursor with naked json messages. Maybe exists some python3 module to communicate with server which is unknown to me. Anyway any reasonable material would be helpful. Thanks in advance.

[Mario Carneiro]

No, the only spec is in the parsing code in the lean-vscode plugin

[Grigoriy Prokhrov]

@Mario Carneiro Thank you!

[Bryan Gin-ge Chen]

There's no formal "spec" but there is now some basic documentation here.

[Julian Berman]

@Grigoriy Prokhrov https://github.com/leanprover-community/lean-client-python/

[Grigoriy Prokhrov]

@Bryan Gin-ge Chen @Julian Berman thank you!