lean-client-python
lean-client-python copied to clipboard
leanprover-community
Python talking to the Lean theorem prover
Could this lean client be use to write an IPython kernel that supports Lean?
Here are some examples I'd like to add to the trio server: * A version of our current example, but with all the lines annotated so the user understands what...
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...
As for the `commands.py`, I think it suffers from the following possible problem. `parse_response` is trying (with limited success) to figure out what type a response is from the JSON...
The newest version of the lean server now has widgets. Our current code breaks. I think the refactor proposed in #6 (or just adding to the PR #5) could make...
Now that we have a testing framework, #3, we should turn on continuous integration. Any objections?
As we talked about in https://github.com/leanprover-community/lean-client-python/pull/3, commands.py needs unit tests. In particular, it's easy to mess up both converting to and from the correct JSON. (This is even more important...
If you sync the same file again (with no changes) the response is of the form ```json {"message":"file unchanged","response":"ok","seq_num":3} ``` It will not send an additional current tasks response, so...
While we could add methods like `state` for every possible use case, we don't need to since we can directly use the `send` method and the corresponding Request object. I'd...
Sometimes the file_info messages don't have line and column. Sometimes a sync will get a "file unchanged" message or an error message. I wrote tests to cover these and fixed...
Metadata
Owner
Metadata
Python talking to the Lean theorem prover