LeanDojo: yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a/lean-example is not a Git repo.

Description What happened? 按照官网教程，安装了leandojo ， 在测试的时候，报错如下信息。请帮忙看看。 做过以下尝试：Extracting Data from Lean 4 ， 也是相同问题。

---------------------------------------------------------t.py 内容-------------------------------------------------------------- [root@localhost lean-dojo-demo]# cat t.py from lean_dojo import LeanGitRepo, trace

repo = LeanGitRepo(“https://github.com/yangky11/lean-example”, “5a0360e49946815cb53132638ccdd46fb1859e2a”) trace(repo, dst_dir=“traced_lean-example”)

---------------------------------------------------------报错信息--------------------------------------------------------------

[root@localhost lean-dojo-demo]# python t.py 2023-07-21 10:54:50.099 | INFO | lean_dojo.data_extraction.cache:get:72 - Downloading the traced repo from the remote cache. Set the environment variable DISABLE_REMOTE_CACHE if you want to trace the repo locally. –2023-07-21 10:54:50-- https://lean-dojo.s3.amazonaws.com/yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a.tar.gz Resolving lean-dojo.s3.amazonaws.com (lean-dojo.s3.amazonaws.com)… 52.92.165.81, 52.92.229.105, 52.218.182.99, … Connecting to lean-dojo.s3.amazonaws.com (lean-dojo.s3.amazonaws.com)|52.92.165.81|:443… connected. HTTP request sent, awaiting response… 200 OK Length: 184449705 (176M) [application/x-gzip] Saving to: ‘/root/.cache/lean_dojo/yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a.tar.gz’

100%[=================================================================================================================================>] 184,449,705 20.5MB/s in 9.7s

2023-07-21 10:55:00 (18.1 MB/s) - ‘/root/.cache/lean_dojo/yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a.tar.gz’ saved [184449705/184449705]

2023-07-21 10:55:20.405 | INFO | lean_dojo.data_extraction.trace:trace:164 - Loading the traced repo from /root/.cache/lean_dojo/yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a/lean-example Traceback (most recent call last): File “/root/lean-dojo-demo/t.py”, line 4, in <module> trace(repo, dst_dir=“traced_lean-example”) File “/usr/local/python3/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py”, line 165, in trace traced_repo = TracedRepo.load_from_disk(cached_path) File “/usr/local/python3/lib/python3.9/site-packages/lean_dojo/data_extraction/traced_data.py”, line 1269, in load_from_disk raise RuntimeError(f"{root_dir} is not a Git repo.") RuntimeError: /root/.cache/lean_dojo/yangky11-lean-example-5a0360e49946815cb53132638ccdd46fb1859e2a/lean-example is not a Git repo.

Detailed Steps to Reproduce the Behavior

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

Platform Information

• OS: [e.g. centos7.9]
• wget 1.14
• docker 24
• python 3.9
• git [e.g. 2.39.1]
• LeanDojo Version [e.g. 1.1.0]