leanprover-community / lean-client-python

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

`commands.py` needs unit tests #11

Open jasonrute opened 4 years ago

jasonrute commented 4 years ago

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 we go with more high level tests for the Lean server that don't depend on the specific JSON. If we do that, there is nothing currently testing our handling of the JSON correctly.) There is no reason to work on this until we complete #6 (or better it could be part of #6).