lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
552 stars 83 forks source link

(Willing to PR) Support async Python #151

Closed fzyzcjy closed 5 months ago

fzyzcjy commented 6 months ago

Currently, LeanDojo provides synchronous API. However, it would be great to provide async python API in order to make downstream programming easier.

IMHO this may not be very hard to implement: The asyncio.subprocess.Process has quite similar APIs compared with the subprocess package LeanDojo is using.

I am willing to PR if this looks ok!

yangky11 commented 6 months ago

Hi,

Thank you for the suggestion and for offering to help. I'm OK with it as long as it does not break LeanDojo's existing API.