search

lean-dojo / LeanDojo

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

[WIP] Support cedar-lean #152

Open andrewmw94 opened 3 months ago

andrewmw94 commented 3 months ago

Changes to support lake projects that aren't at the root of a github repo. Applicable to projects like https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean

This is WIP and not ready to merge (e.g., we'd need to revert baef645)

andrewmw94 commented 3 months ago

Sorry for my poor python code. Any suggestions to make it more idiomatic are appreciated.

yangky11 commented 3 months ago

Thanks! I'm converting it to a PR draft, but please let me know when it's ready.