search

lean-dojo / LeanDojo

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

[Fix] Get first element of paginatedList #54

Closed josojo closed 1 year ago

josojo commented 1 year ago

If I am running the current code, I get the following error:

python scripts/evaluate_lean_4_interaction.py
2023-09-05 20:39:45.569 | DEBUG    | lean_dojo.constants:<module>:63 - Using GitHub without authentication. Don't be surprised if you hit the API rate limit.
2023-09-05 20:39:50.308 | INFO     | __main__:main:64 - Namespace()
Traceback (most recent call last):
  File "/Users/josojo/coding/ai/LeanDojo/scripts/evaluate_lean_4_interaction.py", line 128, in <module>
    main()
  File "/Users/josojo/coding/ai/LeanDojo/scripts/evaluate_lean_4_interaction.py", line 69, in main
    repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7d711f6da4584ecb7d4f057715e1f72ba175c910")
  File "<string>", line 5, in __init__
  File "/Users/josojo/coding/ai/LeanDojo/env/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 401, in __post_init__
    lean_version = get_lean4_commit_from_config(config)
  File "/Users/josojo/coding/ai/LeanDojo/env/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 285, in get_lean4_commit_from_config
    latest_tag = next(LEAN4_NIGHTLY_REPO.get_tags())
TypeError: 'PaginatedList' object is not an iterator

my python version is: 

python -V
Python 3.10.11

This issue should be happening on all script, but I used the one script from this repo:

https://github.com/josojo/LeanDojo/pull/1
yangky11 commented 1 year ago

Hi,

Thank you for the PR. FYI, this error has been fixed in https://github.com/lean-dojo/LeanDojo/pull/52. Please also see https://github.com/lean-dojo/LeanDojo/issues/51.