search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Document Lean server interface #15

Open jasonrute opened 4 years ago

jasonrute commented 4 years ago

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.

jcommelin commented 4 years ago

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

jasonrute commented 4 years ago

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.)

bryangingechen commented 4 years ago

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