lean-client-python icon indicating copy to clipboard operation
lean-client-python copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Document Lean server interface

Open jasonrute opened this issue 4 years ago • 3 comments

This relates to Issue #8 (a more comprehensive trio example), but is a little different. In short, I'd like to document all the requests in commands.py. This will provide a form of documentation of the Lean server interface, probably the best so far. I think I'll be able to incorporate it into the PR for Issue #6, but just in case, I've made it a separate issue.

jasonrute avatar Jun 07 '20 13:06 jasonrute

What kind of documentation are you thinking of? Comments in the .py, or a separate .md file?

jcommelin avatar Jun 08 '20 09:06 jcommelin

I was thinking as doc strings in the commands.py file. That way if you are in an IDE which supports doc strings, it can tell you want to expect from a command. I'd be open to other ideas. (Like Patrick, I agree that really this should be fully documented somewhere else, since other applications also need to use the server.)

jasonrute avatar Jun 08 '20 13:06 jasonrute

@EdAyers added documentation in https://github.com/leanprover-community/lean/pull/443.

bryangingechen avatar Aug 20 '20 15:08 bryangingechen