search

leanprover-community / lean-client-python

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

Freezes if you sync an unchanged file #2

Open jasonrute opened 4 years ago

jasonrute commented 4 years ago

If you sync the same file again (with no changes) the response is of the form 

{"message":"file unchanged","response":"ok","seq_num":3}

It will not send an additional current tasks response, so full_sync is left waiting forever. I'm having a bit of trouble following your code to fix it. You are throwing away the message field (not sure why) and so I don't have access to it to check for this case.

PatrickMassot commented 4 years ago

I don't know where I am "throwing away the message field", but feel free to fix. The current implementation was really an experimental proof of concept. I think this is a better basis for building a robust client than previous attempts, but this is only a basis.

jasonrute commented 4 years ago

This is addressed by PR #5.