Zulip Chat Archive

Stream: new members

Topic: Is there any spec for Lean server protocol?


view this post on Zulip Grigoriy Prokhrov (Mar 28 2021 at 10:57):

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.

view this post on Zulip Mario Carneiro (Mar 28 2021 at 10:59):

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

view this post on Zulip Grigoriy Prokhrov (Mar 28 2021 at 11:03):

@Mario Carneiro Thank you!

view this post on Zulip Bryan Gin-ge Chen (Mar 28 2021 at 12:58):

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

view this post on Zulip Julian Berman (Mar 28 2021 at 14:18):

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

view this post on Zulip Grigoriy Prokhrov (Mar 28 2021 at 15:30):

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


Last updated: May 06 2021 at 21:09 UTC