Fix git method & add more tests

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.

https://leandojo.org

MIT License

536 stars 80 forks source link

Closed RexWzh closed 1 month ago

RexWzh commented 1 month ago

[ ] Fix regex expression in check_git_version
[ ] Fix URL format in LeanGitRepo.commit_url | os.path.join gives invalid URL with \\ rather than / in windows
[ ] Use gitpython in clone_and_checkout
[ ] Add tests for LeanGitRepo

Overall, the changes are compatible with the original code and fix some of the errors on Windows.

One test failed due to a network problem.

Re-run the test.

yangky11 commented 1 month ago

Running tests

yangky11 commented 1 month ago

Thanks!

Will merge into main after the other PR is ready to merge