lean-dojo / LeanDojo

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

Extend function features to allow new repo types #190

Closed RexWzh closed 1 month ago

RexWzh commented 1 month ago

Main Changes

  1. Lean Version: Use string for lean_version instead of a commit hash. Postpone the initialization of the Lean4 repository.
  2. Cache: Update cache.get and cache.store for increased flexibility.
  3. Repository Type: Extend function capabilities to support new repository types, such as _to_commit_hash, normalize_url, get_latest_commit, and url_to_repo, each with tests to ensure reliability.

Progress

Implementation plan for the new feature:

RexWzh commented 1 month ago

Thank you @yangky11 , for your thorough review of most of the work.

The remaining tasks are straightforward after this PR merged.

Two notes to mention:

  1. The test case remote_example_url currently uses my cloned URL on gitee.com, which will not change, but can be replaced if needed.
  2. As git.Repo requires a directory, I plan to place them in .cache/lean_dojo/repos in the last PR.

For compatibility, the cache directory looks like:

❯ tree -L 2 lean_dojo
lean_dojo
├── leanprover-community-aesop-79fb157c6a5061190d169535f8e5cb007914a82e
├── leanprover-community-batteries-d2b1546c5fc05a06426e3f6ee1cb020e71be5592
├── repos
│   ├── rexzong-lean4-example-3f8c5eb303a225cdef609498b8d87262e5ef344b
│   └── testrepo-lean4-example-3f8c5eb303a225cdef609498b8d87262e5ef344b
├── yangky11-lean4-example-3f8c5eb303a225cdef609498b8d87262e5ef344b
└── yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f

11 directories, 0 files

Pytest result

image
RexWzh commented 1 month ago

merge to #179