Address non-happy paths

leanprover-community / lean-client-python

Python talking to the Lean theorem prover

Apache License 2.0

39 stars 6 forks source link

Address non-happy paths #5

Open jasonrute opened 4 years ago

jasonrute commented 4 years ago

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 the Trio code.

I didn't fix or address the qt code. In particular, I made a change to the commands.py file (added a SyncResponse type (which has a message field). This might break something in the qt_server.

(This PR builds on my previous two.)

PatrickMassot commented 4 years ago

Let's wait until #3 stabilizes then. Also I don't think we should merge this without checking the Qt code. Hopefully commands.py should be very stable and that won't happen to often. Otherwise we may need to split this repo into three packages. I'll check the Qt code once #3 and #4 land.

jasonrute commented 4 years ago

I agree we should check Qt code before merging. I just haven't got around to running it yet.