Could you trace a single lean file without using github?

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.

https://leandojo.org

MIT License

532 stars 77 forks source link

Closed UltimatePea closed 9 months ago

UltimatePea commented 9 months ago

I see currently Leandojo requires a github repo, is it possible to trace a single file without its dependency locally?

Essentially, I am looking for something that could talk to lean for a single theorem (without any dependency) without much overhead. Thanks!

yangky11 commented 9 months ago

There are related discussions (https://github.com/lean-dojo/LeanDojo/discussions/78), but currently we do not support this function.

UltimatePea commented 9 months ago

Thank you!