Failed trace because of lean4 dependency

[Adarsh321123]

Description I am trying to trace the PFR repo on commit 6a5082ee465f9e44cea479c7b741b3163162bb7e using LeanDojo version 2.0.3. However, I am running into the following error:

Failed to trace repo LeanGitRepo
(url='https://github.com/teorth/pfr', commit='6a5082ee465f9e44cea479c7b741b3163162bb7e') because of Inval
id tag or branch: `nightly-2024-06-05` for Repository(full_name="leanprover/lean4")

Detailed Steps to Reproduce the Behavior Run python -m pip install lean_dojo==2.0.3 and then run the following:

from lean_dojo import *

url = "https://github.com/teorth/pfr"
commit = "6a5082ee465f9e44cea479c7b741b3163162bb7e"
repo = LeanGitRepo(url, commit)
traced_repo = trace(repo)

Logs in Debug Mode Set the environment variable VERBOSE=1 and paste the logs here.

2024-08-10 12:19:46.579 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:489 - Querying the dep
endencies of LeanGitRepo(url='https://github.com/teorth/pfr', commit='6a5082ee465f9e44cea479c7b741b3163162b
b7e')
2024-08-10 12:19:47.936 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.6.0-rc1
2024-08-10 12:19:50.190 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.7.0
2024-08-10 12:19:51.117 | DEBUG    | lean_dojo.data_extraction.lean:url_to_repo:68 - url_to_repo("https://g
ithub.com/leanprover-community/import-graph.git") failed. Retrying...
2024-08-10 12:19:52.237 | DEBUG    | lean_dojo.data_extraction.lean:url_to_repo:68 - url_to_repo("https://g
ithub.com/leanprover-community/import-graph.git") failed. Retrying...
2024-08-10 12:19:55.468 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.10.0
2024-08-10 12:19:56.496 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for doc-gen4 main
2024-08-10 12:19:57.110 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.11.0-rc1
2024-08-10 12:19:57.748 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:489 - Querying the dep
endencies of LeanGitRepo(url='https://github.com/YaelDillies/LeanAPAP', commit='f47447e44d8e82ab214ed8c1b19
9329141fc5b1f')
2024-08-10 12:19:58.514 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.9.0-rc1
2024-08-10 12:19:59.550 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.10.0-rc1
2024-08-10 12:20:00.300 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.9.0
2024-08-10 12:20:01.788 | DEBUG    | lean_dojo.data_extraction.lean:url_to_repo:68 - url_to_repo("https://g
ithub.com/leanprover-community/mathlib4.git") failed. Retrying...
2024-08-10 12:20:02.906 | DEBUG    | lean_dojo.data_extraction.lean:url_to_repo:68 - url_to_repo("https://g
ithub.com/leanprover-community/mathlib4.git") failed. Retrying...
2024-08-10 12:20:06.158 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:489 - Querying the dep
endencies of LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3dd071bc2260b3cf9a
71863d0dee1242fec41522')
2024-08-10 12:20:07.392 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:489 - Querying the dep
endencies of LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='6d8e3118ab526f8dfcabcbdf9f05
dc34e5c423a8')
2024-08-10 12:20:08.444 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 v4.10.0-rc2
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2024-08-10 12:20:10.306 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 nightly-2024-06-05
2024-08-10 12:20:11.583 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for md4lean main
2024-08-10 12:20:11.781 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for BibtexQuery master
2024-08-10 12:20:12.177 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4-unicode-basic main
2024-08-10 12:20:12.897 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4-cli nightly
2024-08-10 12:20:13.077 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commi
t hash for lean4 nightly-2024-06-05
2024-08-10 12:20:14.314 | INFO     | generate_benchmark_lean4:main:346 - Failed to trace repo LeanGitRepo(u
rl='https://github.com/teorth/pfr', commit='6a5082ee465f9e44cea479c7b741b3163162bb7e') because of Invalid t
ag or branch: `nightly-2024-06-05` for Repository(full_name="leanprover/lean4")

Platform Information

• OS: Ubuntu 20.04.6 LTS
• LeanDojo Version 2.0.3

[peter-peng-w]

Had the same error when tracing Mathlib4 commit a45ae63747140c1b2cbad9d46f518015c047047a using LeanDojo version 2.0.3, any suggestions?

[yangky11]

Maybe try the latest version and see if the error persists?

[peter-peng-w]

Using the latest version of Lean-Dojo (version 2.1.2) fixed this issue.