Support Repositories with Inner Lakefile

Open andrewmw94 opened this issue 1 year ago • 1 comments

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

Apr 04 '24 15:04 andrewmw94

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

Apr 04 '24 21:04 yangky11