Stream: new members
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.
Mario Carneiro (Mar 28 2021 at 10:59):
No, the only spec is in the parsing code in the lean-vscode plugin
Grigoriy Prokhrov (Mar 28 2021 at 11:03):
@Mario Carneiro Thank you!
Bryan Gin-ge Chen (Mar 28 2021 at 12:58):
There's no formal "spec" but there is now some basic documentation here.
Julian Berman (Mar 28 2021 at 14:18):
@Grigoriy Prokhrov https://github.com/leanprover-community/lean-client-python/
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