Failed to register worker 01000000ffffffffffffffffffffffffffffffffffffffffffffffff to Raylet. IOError: [RayletClient] Unable to register worker with raylet. No such file or directory

[parsifal-chx]

Hi! I'm encountering a challenging issue while running a program that traces repo. My current operating environment includes Ubuntu 20.04, Python 3.10, Lean 4.2, and Ray 2.8.0. Despite attempting to restart Ray using the command ray start --head, the issue persists. Below, I have provided my code and a screenshot of the error.

after ray start --head

[yangky11]

Hi,

Can you upgrade to the latest version (v1.4.1) and try again? Please also post the code in a way that I can directly copy (not just a screenshot). Thanks.

[parsifal-chx]

Thanks for the response, This is a very simple demo. Following your advice, I upgraded the version, but the problem still persists.

from lean_dojo import *
repo = LeanGitRepo(
    #  mathlib的地址
    "https://github.com/leanprover-community/mathlib4",
    # 一个具体的版本
    "3ce43c18f614b76e161f911b75a3e1ef641620ff",
)
repo.get_config("lean-toolchain")
# A few minutes if the traced repo is in the cache; many hours otherwise.
traced_repo = trace(repo)

error

/home/rise/anaconda3/envs/chx-py3.10/bin/python /home/rise/learn/leanDojo/extract.py 
2023-11-30 11:18:52.309 | INFO     | lean_dojo.data_extraction.trace:trace:182 - Loading the traced repo from /home/rise/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4
2023-11-30 11:18:53,092	INFO worker.py:1489 -- Connecting to existing Ray cluster at address: 198.18.0.1:6379...
[2023-11-30 11:18:53,096 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:54,098 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:55,099 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:56,100 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:57,102 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:58,103 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:18:59,105 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:19:00,106 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:19:01,107 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 11:19:02,109 W 108247 108247] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
2023-11-30 11:19:03,111	INFO worker.py:1638 -- Failed to connect to the default Ray cluster address at 198.18.0.1:6379. This is most likely due to a previous Ray instance that has since crashed. To reset the default address to connect to, run `ray stop` or restart Ray with `ray start`.
Traceback (most recent call last):
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/worker.py", line 1629, in init
    _global_node = ray._private.node.Node(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/node.py", line 254, in __init__
    node_info = ray._private.services.get_node_to_connect_for_driver(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/services.py", line 475, in get_node_to_connect_for_driver
    return global_state.get_node_to_connect_for_driver(node_ip_address)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/state.py", line 751, in get_node_to_connect_for_driver
    return self.global_state_accessor.get_node_to_connect_for_driver(
  File "python/ray/includes/global_state_accessor.pxi", line 218, in ray._raylet.GlobalStateAccessor.get_node_to_connect_for_driver
RuntimeError: b'GCS has started but no raylets have registered yet.'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/rise/learn/leanDojo/extract.py", line 10, in <module>
    traced_repo = trace(repo)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 183, in trace
    traced_repo = TracedRepo.load_from_disk(cached_path)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1481, in load_from_disk
    with ray_actor_pool(_TracedRepoHelper, root_dir, repo) as pool:
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/contextlib.py", line 135, in __enter__
    return next(self.gen)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/utils.py", line 72, in ray_actor_pool
    ray.init()
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/worker.py", line 1645, in init
    raise ConnectionError
ConnectionError

Process finished with exit code 1

[yangky11]

What will happen if you first run ray stop to stop the Ray server and then run the following commands in Python:

import ray
ray.init()

Is there any error?

BTW, if the problem is with Ray, a (slower) workaround is to disable Ray by setting the NUM_PROCS environment variable to 1.

[parsifal-chx]

Thanks for your patient guidance.

(base) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ conda activate chx-py3.10
(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ ray stop
Stopped all 5 Ray processes.
(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ python
Python 3.10.13 (main, Sep 11 2023, 13:44:35) [GCC 11.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import ray
>>> ray.init()
2023-11-30 16:07:35,973	INFO worker.py:1664 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
[2023-11-30 16:07:36,690 E 117019 117019] core_worker.cc:205: Failed to register worker 01000000ffffffffffffffffffffffffffffffffffffffffffffffff to Raylet. IOError: [RayletClient] Unable to register worker with raylet. No such file or directory

[parsifal-chx]

Additionally, I have attempted to restart Ray using the command ray start --head after executing ray stop, but this approach proved to be ineffective.

(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ ray stop
Stopped all 5 Ray processes.
(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ ray start --head
Usage stats collection is enabled. To disable this, add `--disable-usage-stats` to the command that starts the cluster, or run the following command: `ray disable-usage-stats` before starting the cluster. See https://docs.ray.io/en/master/cluster/usage-stats.html for more details.

Local node IP: 198.18.0.1

--------------------
Ray runtime started.
--------------------

Next steps
  To add another node to this Ray cluster, run
    ray start --address='198.18.0.1:6379'
  
  To connect to this Ray cluster:
    import ray
    ray.init()
  
  To submit a Ray job using the Ray Jobs CLI:
    RAY_ADDRESS='http://127.0.0.1:8265' ray job submit --working-dir . -- python my_script.py
  
  See https://docs.ray.io/en/latest/cluster/running-applications/job-submission/index.html 
  for more information on submitting Ray jobs to the Ray cluster.
  
  To terminate the Ray runtime, run
    ray stop
  
  To view the status of the cluster, use
    ray status
  
  To monitor and debug Ray, view the dashboard at 
    127.0.0.1:8265
  
  If connection to the dashboard fails, check your firewall settings and network configuration.
(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ python
Python 3.10.13 (main, Sep 11 2023, 13:44:35) [GCC 11.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import ray
>>> ray.init()
2023-11-30 16:27:27,260	INFO worker.py:1489 -- Connecting to existing Ray cluster at address: 198.18.0.1:6379...
[2023-11-30 16:27:27,266 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:28,267 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:29,269 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:30,271 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:31,272 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:32,274 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:33,275 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:34,277 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:35,279 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
[2023-11-30 16:27:36,280 W 117930 117930] global_state_accessor.cc:407: Some processes that the driver needs to connect to have not registered with GCS, so retrying. Have you run 'ray start' on this node?
2023-11-30 16:27:37,282	INFO worker.py:1638 -- Failed to connect to the default Ray cluster address at 198.18.0.1:6379. This is most likely due to a previous Ray instance that has since crashed. To reset the default address to connect to, run `ray stop` or restart Ray with `ray start`.
Traceback (most recent call last):
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/worker.py", line 1629, in init
    _global_node = ray._private.node.Node(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/node.py", line 254, in __init__
    node_info = ray._private.services.get_node_to_connect_for_driver(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/services.py", line 475, in get_node_to_connect_for_driver
    return global_state.get_node_to_connect_for_driver(node_ip_address)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/state.py", line 751, in get_node_to_connect_for_driver
    return self.global_state_accessor.get_node_to_connect_for_driver(
  File "python/ray/includes/global_state_accessor.pxi", line 218, in ray._raylet.GlobalStateAccessor.get_node_to_connect_for_driver
RuntimeError: b'GCS has started but no raylets have registered yet.'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/ray/_private/worker.py", line 1645, in init
    raise ConnectionError
ConnectionError

[yangky11]

If you cannot do

import ray
ray.init()

, the problem is specific to your particular system and Ray installation. There is nothing we can do on LeanDojo's side (other than you can set NUM_PROCS=1 to disable Ray). I'd suggest you ask in Ray's GitHub repo.

[parsifal-chx]

Okay, thanks for your patient guidance.

[parsifal-chx]

Sorry to bother you again, when I extract data through leandojo(The code is the same as above), I get an error every time: urllib.error.URLError: <urlopen error [Errno 104] Connection reset by peer>I access github by using clash for window in China, Is there any way you can prevent this?

(leandojo) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ VERBOSE=1 python extract.py 
2023-12-09 16:04:18.973 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
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
2023-12-09 16:04:29.970 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:158 - The traced repo is available in the cache.
2023-12-09 16:04:29.971 | INFO     | lean_dojo.data_extraction.trace:trace:182 - Loading the traced repo from /home/rise/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4
2023-12-09 16:04:30.903 | DEBUG    | lean_dojo.data_extraction.traced_data:load_from_disk:1463 - Loading 4462 traced XML files from /home/rise/.cache/lean_dojo/leanprover-community-mathlib4-3ce43c18f614b76e161f911b75a3e1ef641620ff/mathlib4 with 11 workers
2023-12-09 16:04:32,780	INFO worker.py:1664 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8265 
  0%|                                                  | 0/4462 [00:00<?, ?it/s](pid=186313) 2023-12-09 16:04:34.325 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
 13%|█████                                   | 562/4462 [01:37<13:59,  4.65it/s](_TracedRepoHelper pid=186320) 2023-12-09 16:06:10.840 | DEBUG    | lean_dojo.utils:read_url:208 - Request to https://raw.githubusercontent.com/leanprover-community/mathlib4/3ce43c18f614b76e161f911b75a3e1ef641620ff/lean-toolchain failed. Retrying...
(pid=186309) 2023-12-09 16:04:34.484 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication [repeated 10x across cluster] (Ray deduplicates logs by default. Set RAY_DEDUP_LOGS=0 to disable log deduplication, or see https://docs.ray.io/en/master/ray-observability/ray-logging.html#log-deduplication for more options.)
100%|███████████████████████████████████████| 4462/4462 [13:47<00:00,  5.39it/s]
2023-12-09 16:18:22.265 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='3ce43c18f614b76e161f911b75a3e1ef641620ff')
2023-12-09 16:18:29.111 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/doc-gen4 main
2023-12-09 16:18:38.827 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/std4 main
2023-12-09 16:18:48.045 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover-community/quote4 master
2023-12-09 16:18:57.460 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover-community/aesop master
2023-12-09 16:19:07.339 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/lean4-cli nightly
2023-12-09 16:19:14.700 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover-community/ProofWidgets4 v0.0.18
2023-12-09 16:19:22.963 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='53ecc225fea834acd7f32b9dc1aed880b79d70b9')
2023-12-09 16:19:30.948 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/xubaiw/CMark.lean main
2023-12-09 16:19:39.011 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/fgdorais/lean4-unicode-basic main
2023-12-09 16:19:48.553 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/mhuisi/lean4-cli nightly
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2023-12-09 16:19:58.053 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/hargonix/LeanInk doc-gen
2023-12-09 16:20:08.423 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77')
2023-12-09 16:20:15.074 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='dc62b29a26fcc3da545472ab8ad2c98ef3433634')
2023-12-09 16:20:23.850 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa')
2023-12-09 16:20:29.529 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1')
2023-12-09 16:20:38.426 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/std4', commit='b197bd218dbab248ad8899404334d41da04f5d13')
2023-12-09 16:20:47.783 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/doc-gen4 main
2023-12-09 16:20:50.286 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='53ecc225fea834acd7f32b9dc1aed880b79d70b9')
2023-12-09 16:20:56.797 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/xubaiw/CMark.lean main
2023-12-09 16:20:59.077 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/fgdorais/lean4-unicode-basic main
2023-12-09 16:21:01.364 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/mhuisi/lean4-cli nightly
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2023-12-09 16:21:04.993 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/hargonix/LeanInk doc-gen
2023-12-09 16:21:07.425 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77')
2023-12-09 16:21:13.912 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='dc62b29a26fcc3da545472ab8ad2c98ef3433634')
2023-12-09 16:21:21.335 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa')
2023-12-09 16:21:26.198 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1')
2023-12-09 16:21:35.445 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover-community/quote4', commit='ccba5d35d07a448fab14c0e391c8105df6e2564c')
2023-12-09 16:21:45.078 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover-community/aesop', commit='3141402ba5a5f0372d2378fd75a481bc79a74ecf')
2023-12-09 16:21:52.799 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/std4 main
2023-12-09 16:21:55.250 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/std4', commit='b197bd218dbab248ad8899404334d41da04f5d13')
2023-12-09 16:22:02.834 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/doc-gen4 main
2023-12-09 16:22:05.261 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='53ecc225fea834acd7f32b9dc1aed880b79d70b9')
2023-12-09 16:22:13.346 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/xubaiw/CMark.lean main
2023-12-09 16:22:15.833 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/fgdorais/lean4-unicode-basic main
2023-12-09 16:22:18.190 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/mhuisi/lean4-cli nightly
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2023-12-09 16:22:21.695 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/hargonix/LeanInk doc-gen
2023-12-09 16:22:24.127 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77')
2023-12-09 16:22:31.079 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='dc62b29a26fcc3da545472ab8ad2c98ef3433634')
2023-12-09 16:22:38.244 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa')
2023-12-09 16:22:43.042 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1')
2023-12-09 16:22:51.625 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa')
2023-12-09 16:22:56.764 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover-community/ProofWidgets4', commit='27715d1daf32b9657dc38cd52172d77b19bde4ba')
2023-12-09 16:23:03.530 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/std4 main
2023-12-09 16:23:06.086 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/std4', commit='b197bd218dbab248ad8899404334d41da04f5d13')
2023-12-09 16:23:13.559 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/leanprover/doc-gen4 main
2023-12-09 16:23:16.622 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/leanprover/doc-gen4', commit='53ecc225fea834acd7f32b9dc1aed880b79d70b9')
2023-12-09 16:23:23.817 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/xubaiw/CMark.lean main
2023-12-09 16:23:26.085 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/fgdorais/lean4-unicode-basic main
2023-12-09 16:23:28.379 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/mhuisi/lean4-cli nightly
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356
2023-12-09 16:23:31.671 | DEBUG    | lean_dojo.data_extraction.lean:_parse_lakefile_dependencies:573 - Querying the commit hash for https://github.com/hargonix/LeanInk doc-gen
2023-12-09 16:23:35.615 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77')
2023-12-09 16:23:41.812 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='dc62b29a26fcc3da545472ab8ad2c98ef3433634')
2023-12-09 16:23:48.529 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa')
2023-12-09 16:23:53.194 | DEBUG    | lean_dojo.data_extraction.lean:_get_lean4_dependencies:584 - Querying the dependencies of LeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1')
2023-12-09 16:50:16.499 | DEBUG    | lean_dojo.utils:read_url:208 - Request to https://raw.githubusercontent.com/leanprover-community/mathlib4/3ce43c18f614b76e161f911b75a3e1ef641620ff/lean-toolchain failed. Retrying...
2023-12-09 16:59:23.155 | DEBUG    | lean_dojo.utils:read_url:208 - Request to https://raw.githubusercontent.com/leanprover-community/mathlib4/3ce43c18f614b76e161f911b75a3e1ef641620ff/lean-toolchain failed. Retrying...
Traceback (most recent call last):
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 1348, in do_open
    h.request(req.get_method(), req.selector, req.data, headers,
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 1283, in request
    self._send_request(method, url, body, headers, encode_chunked)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 1329, in _send_request
    self.endheaders(body, encode_chunked=encode_chunked)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 1278, in endheaders
    self._send_output(message_body, encode_chunked=encode_chunked)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 1038, in _send_output
    self.send(msg)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 976, in send
    self.connect()
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/http/client.py", line 1455, in connect
    self.sock = self._context.wrap_socket(self.sock,
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/ssl.py", line 513, in wrap_socket
    return self.sslsocket_class._create(
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/ssl.py", line 1104, in _create
    self.do_handshake()
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/ssl.py", line 1375, in do_handshake
    self._sslobj.do_handshake()
ConnectionResetError: [Errno 104] Connection reset by peer

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/rise/learn/leanDojo/extract.py", line 15, in <module>
    traced_repo = trace(repo)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 183, in trace
    traced_repo = TracedRepo.load_from_disk(cached_path)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1492, in load_from_disk
    traced_files_graph = _build_dependency_graph(traced_files, root_dir, repo)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1236, in _build_dependency_graph
    for dep_module, dep_path in tf.get_direct_dependencies(repo):
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1031, in get_direct_dependencies
    packages_dir = repo.get_packages_dir()
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 493, in get_packages_dir
    toolchain = self.get_config("lean-toolchain")
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/data_extraction/lean.py", line 623, in get_config
    content = read_url(config_url)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/utils.py", line 206, in read_url
    raise ex
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/utils.py", line 202, in read_url
    with urllib.request.urlopen(url) as f:
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 216, in urlopen
    return opener.open(url, data, timeout)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 519, in open
    response = self._open(req, data)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 536, in _open
    result = self._call_chain(self.handle_open, protocol, protocol +
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 496, in _call_chain
    result = func(*args)
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 1391, in https_open
    return self.do_open(http.client.HTTPSConnection, req,
  File "/home/rise/anaconda3/envs/leandojo/lib/python3.10/urllib/request.py", line 1351, in do_open
    raise URLError(err)
urllib.error.URLError: <urlopen error [Errno 104] Connection reset by peer>

[yangky11]

I think it's probably related to the network environment in China. I can try to see if it's possible to reduce the number of requests LeanDojo makes to GitHub.

[yangky11]

@parsifal-chx How about the current version?

[parsifal-chx]

I updated the version #108 and the problem was solved ,thanks!