Lean Dojo

Stream: general

[Mohamamd Awheeo]

I want to use leanDojo to interact with lean programmatically. The code snippet in the documentation is provided bellow. Is there a way to trace a lean file from my local device not from a git repo
image.png

[Eric Wieser]

Git repos can exist on your local device too, I assume the API works with those just fine

[Jason Rute]

@Kaiyu Yang

[Kaiyu Yang]

Currently the way LeanDojo handles Git repos is quite ad-hoc and does not support local repos. Adding such support should not be difficult, though it is currently not our first priority (PRs are welcome). Does your use case make it very difficult to upload the repo to Github (e.g., you need to make frequent changes to a local repo)?

BTW, for questions specific to LeanDojo, you're welcome to ask in our repo: https://github.com/lean-dojo/LeanDojo#questions-and-bugs