Add testing framework

[jasonrute]

I've added a testing framework for the trio server. Basically I've created a mock lean process in Trio which runs according to a (linear) script. I've included a test for the issue we already fixed where Lean stops waiting after we return a current_tasks response too early.

Also, to facilitate easier debugging, I've added another level of debugging called debug_bytes. This prints the lean messages as they are sent over the channel. Since parse_response in the trio server often crashes, this is a way to get at the message it is crashing on. Also, it is useful for creating the mock lean scripts in the tests.

Curious to get your thoughts Patrick.

[jasonrute]

Ok, prematurely PRed this, but it is all fixed now.

[PatrickMassot]

Nice! I don't have time to read it carefully tonight (it's 11pm here), but the description of the mock Lean process sounds like what I intended to do at some point. The style of the test script reminds me of Behavior Driven Development. You could have a look at pytest-bdd if you fancy that style.

[PatrickMassot]

Thanks Jason, this is indeed essential and was on my TODO list as well. I left comments aiming to simplify things a bit.

[jasonrute]

I switched to pytest. I'll wait for your thoughts on my thoughts before making other changes here.

[jasonrute]

Just so you know, I haven't forgot about this. I got caught up in some other projects and personal stuff and I have to go to work today, but I'll get back to this soon. Thanks for the changes!

[PatrickMassot]

There is no hurry at all, I have plenty to do while waiting.

[jasonrute]

Ok, I'm back at this. (It only took me a month.) I'll read through the code again and try to finish these PRs.

[jasonrute]

Ok, added some more fixes, but I need to still merge (or rebase) master. I tried it earlier and ran into some errors in the tests that need to be fixed.

[jasonrute]

Ok, I think we have addressed all the concerns. @PatrickMassot can I get an approval on this? (Also, note that I did a rebase, so if you are going to do anything with this branch, be aware. I don't think you had any outstanding edits to this branch, so I thought it was safe.)

[PatrickMassot]

Why do we need this explicit sleep (and the one below)?

[jasonrute]

That is a great question. I'm pretty sure it was necessary, but let me remember/investigate why and I'll add it as a comment to the code.

[jasonrute]

Ok, I've addressed this in this commit (a585707). In particular,

1. I moved the sleep command into the collect_stdin_messages to avoid duplicated code.
2. I clearly explained what three goals the sleep command (in conjunction with get_data_nowait()) are intended to accomplish.
3. I made the waiting time a parameter which could be changed. It might need to be extended if we are testing some complicated functionality which takes a while to compute.
4. I left the default of 0.01 seconds. In my tests, 0.001 seconds also allowed the tests to pass but 0.0001 was too fast. I thought 0.01 seconds was short enough to not make the tests take too long, but also gave an order of magnitude buffer to account for slow machines.

[PatrickMassot]

I still don't understand. The whole point of this async thing is to avoid guessing how long we should wait for answers from Lean. Why do we need any sleep? Is this only for tests, simulating some delay in answers, or is this going to be needed in actual uses of this lean-python client?

[jasonrute]

In short, it is only needed for tests because we don't want to wait forever for the Lean Python client to return information which it may never do.

Remember, this is "Mock Lean", so I'm simulating a fake Lean server process waiting for our Python client to send a request. A real Lean server would make a blocking call to read the data and wait as long as necessary. That could be accomplished via self.stdin.get_data() in collect_stdin_messages, but the problem is that I don't know if our client will send any requests and I could be left waiting forever. This is used to support LeanShouldGetRequest and LeanShouldNotGetRequest. Those test that either Lean receives a request (and it is a particular form) or that it doesn't receive a request, so I need the ability to stop waiting.

So what I'm doing here is waiting for our Python client for a little bit (enough time for our Python client to run and send a message if it is going to), and then checking if the message is sent in a non-blocking manner.

Another way I could possibly implement this is via a blocking call, self.stdin.get_data(), and then use a feature of Trio testing framework that has some way to stop execution of a blocked coroutine after a certain time. I think this might exist, however, I'd have to look into that more. It is not clear to me how to implement this.

[jasonrute]

So like I said, an alternative way to do this would be with cancellation and timeouts. I would still need to look into how to do this more. Would you prefer that approach?

[jasonrute]

I could do something like this inside collect_stdin_messages:

with trio.move_on_after(wait_time_seconds):
    try:
        data = await self.stdin.get_data()
    except Cancelled:
        return None
   
self.partial_message = raw_messages.pop()
self.messages.extend(self.parse_message(m) for m in raw_messages)

[jasonrute]

Ok, I just pushed a commit using the above snippet. I think hope it will clear up a lot of the confusion.

[PatrickMassot]

Yes, I think this expresses what's going on much more directly.