Support Repositories with Inner Lakefile

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.

https://leandojo.org

MIT License

478 stars 72 forks source link

Support Repositories with Inner Lakefile #153

Open andrewmw94 opened 3 months ago

andrewmw94 commented 3 months ago

Thanks for open sourcing this tool, it's great! I'd like to use it with projects such as https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean, which has a lake project in a subfolder instead of at the root. I forked LeanDojo and a work-in-progress PR here: https://github.com/lean-dojo/LeanDojo/pull/152.

To be more general, I think it would be great to support pointing this at any local lake project. I'm happy to contribute this if you agree it would be useful. My plan would be to

yangky11 commented 3 months ago

Sounds great to me. Please let me know if the PR is ready for review.