search

leanprover-community / lean-client-python

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

Add testing framework #3

Closed jasonrute closed 4 years ago

jasonrute commented 4 years ago

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 commented 4 years ago

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

PatrickMassot commented 4 years ago

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.

jasonrute commented 4 years ago

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

jasonrute commented 4 years ago

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 commented 4 years ago

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

jasonrute commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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.)