problem in 'demo-lean.ipynb'

[yuchen814]

Description

I executed it successfully before, but recently I ran it again and there was an error.

When I executed "traced_repo = trace(repo)" in 'demo-lean.ipynb' I had an error.

GitCommandError                           Traceback (most recent call last)
Cell In[4], [line 2](vscode-notebook-cell:?execution_count=4&line=2)
      [1](vscode-notebook-cell:?execution_count=4&line=1) # A few minutes if the traced repo is in the cache; many hours otherwise.
----> [2](vscode-notebook-cell:?execution_count=4&line=2) traced_repo = trace(repo)

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:247, in trace(repo, dst_dir, build_deps)
    [242](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:242)     dst_dir = Path(dst_dir)
    [243](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:243)     assert (
    [244](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:244)         not dst_dir.exists()
    [245](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:245)     ), f"The destination directory {dst_dir} already exists."
--> [247](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:247) cached_path = get_traced_repo_path(repo, build_deps)
    [248](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:248) logger.info(f"Loading the traced repo from {cached_path}")
    [249](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:249) traced_repo = TracedRepo.load_from_disk(cached_path, build_deps)

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:213, in get_traced_repo_path(repo, build_deps)
    [211](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:211) with working_directory() as tmp_dir:
    [212](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:212)     logger.debug(f"Working in the temporary directory {tmp_dir}")
--> [213](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:213)     _trace(repo, build_deps)
    [214](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:214)     src_dir = tmp_dir / repo.name
    [215](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:215)     traced_repo = TracedRepo.from_traced_files(src_dir, build_deps)

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:130, in _trace(repo, build_deps)
    [128](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:128) # Trace `repo` in the current working directory.
    [129](https://file+.vscode-resource.vscode-cdn.net/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:129) assert not repo.is_lean4, "Cannot trace Lean 4 itself."
...
error: 5515 bytes of body are still expected
fetch-pack: unexpected disconnect while reading sideband packet
fatal: early EOF
fatal: fetch-pack: invalid index-pack output
'

Platform Information

• OS: [macOS]

[yangky11]

I wasn't able to reproduce the problem. Have you tried the latest version (2.2.0 or the current main branch)?

[yuchen814]

I have solved this problem, thanks for your help!