Error when running python scripts/trace_repos.py

[j991222]

I encountered an error when running python scripts/trace_repos.py(CONTAINER="native"). The error message is as follows:

2023-10-01 12:31:32.387 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:503 - Querying the commit hash for https://github.com/leanprover/doc-gen4 "main"
2023-10-01 12:31:36.338 | DEBUG    | lean_dojo.utils:read_url:238 - Requset to https://github.com/leanprover/lean4-nightly/releases/tag/v4.1.0 failed. Retrying...
Traceback (most recent call last):
  File "/home/username/extractdata/extract.py", line 7, in <module>
    trace(repo)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 164, in trace
    traced_repo = TracedRepo.load_from_disk(cached_path)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1481, in load_from_disk
    dependencies = repo.get_dependencies(root_dir)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 461, in get_dependencies
    return self._get_lean4_dependencies(path)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 524, in _get_lean4_dependencies
    for name, repo in self._parse_lakefile_dependencies(lakefile):
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 507, in _parse_lakefile_dependencies
    deps.append((m["name"], LeanGitRepo(url, commit)))
  File "<string>", line 5, in __init__
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 400, in __post_init__
    lean_version = get_lean4_commit_from_config(config)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 297, in get_lean4_commit_from_config
    html = read_url(url)
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/utils.py", line 236, in read_url
    raise ex
  File "/home/username/.conda/envs/myenv/lib/python3.10/site-packages/lean_dojo/utils.py", line 232, in read_url
    with urllib.request.urlopen(url) as f:
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 216, in urlopen
    return opener.open(url, data, timeout)
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 525, in open
    response = meth(req, response)
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 634, in http_response
    response = self.parent.error(
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 563, in error
    return self._call_chain(*args)
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 496, in _call_chain
    result = func(*args)
  File "/home/username/.conda/envs/myenv/lib/python3.10/urllib/request.py", line 643, in http_error_default
    raise HTTPError(req.full_url, code, msg, hdrs, fp)
urllib.error.HTTPError: HTTP Error 404: Not Found

[yangky11]

What is the version of LeanDojo you're using? Upgrading to the latest version (v1.2.5) may solve the problem.

[j991222]

I updated to v1.2.5 and it worked. Thanks!