search

leanprover-community / lean-client-python

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

Fix await bug in kill #13

Closed jasonrute closed 4 years ago

jasonrute commented 4 years ago

This fixes issues with the kill method in the trio server:

async def kill(self):
         """Kill the Lean process."""
        await self.process.kill()

self.process.kill() is not await-able:

TypeError: object NoneType can't be used in 'await' expression

So I removed that await. Now there is no reason for it to be async, so I removed that as well.

Last, I added server.kill() to the trio example. I think it is a good habit to kill processes after you start them. Here it doesn't matter since you are exiting the application (and exiting trio which I also imagine would kill it), however, it is good to have. Also it acts as a sort of (weak) test that the bug is fixed.

jasonrute commented 4 years ago

This doesn't depend on any other PRs and can be merged right away.