trace depository error

[moyvbai]

I used LeanDojo to trace lean4 project(repo = LeanGitRepo(
"https://github.com/Moyvbai/lean4-example",
"9ed7ebe5ecd3903dc59a49995da6514f39f50bfc",
)),

but the following error occurred

{
	"name": "FileNotFoundError",
	"message": "/home2/shuming/Lean/Tmp/tmpbq4ytl3q/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json does not exist",
	"stack": "---------------------------------------------------------------------------
FileNotFoundError                         Traceback (most recent call last)
Cell In[5], line 2
      1 # A few minutes if the traced repo is in the cache; many hours otherwise.
----> 2 traced_repo = trace(repo)

File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:181, in trace(repo, dst_dir)
    176     dst_dir = Path(dst_dir)
    177     assert (
    178         not dst_dir.exists()
    179     ), f\"The destination directory {dst_dir} already exists.\"
--> 181 cached_path = get_traced_repo_path(repo)
    182 logger.info(f\"Loading the traced repo from {cached_path}\")
    183 traced_repo = TracedRepo.load_from_disk(cached_path)

File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py:154, in get_traced_repo_path(repo)
    152 logger.debug(f\"Working in the temporary directory {tmp_dir}\")
    153 _trace(repo)
--> 154 traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name)
    155 traced_repo.save_to_disk()
    156 path = cache.store(tmp_dir)

File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:1409, in TracedRepo.from_traced_files(cls, root_dir)
   1399         traced_files = list(
   1400             tqdm(
   1401                 pool.map_unordered(
   (...)
   1405             )
   1406         )
   1408 dependencies = repo.get_dependencies(root_dir)
-> 1409 traced_files_graph = _build_dependency_graph(traced_files, root_dir, repo)
   1410 traced_repo = cls(repo, dependencies, root_dir, traced_files_graph)
   1411 traced_repo._update_traced_files()

File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:1240, in _build_dependency_graph(seed_files, root_dir, repo)
   1238 if not G.has_node(dep_path_str):
   1239     json_path = to_json_path(root_dir, dep_path, repo)
-> 1240     tf_dep = TracedFile.from_traced_file(root_dir, json_path, repo)
   1241     G.add_node(dep_path_str, traced_file=tf_dep)
   1242     traced_files.append(tf_dep)

File ~/miniconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py:638, in TracedFile.from_traced_file(cls, root_dir, json_path, repo)
    636     json_path = root_dir / json_path
    637 if not json_path.exists():
--> 638     raise FileNotFoundError(f\"{json_path} does not exist\")
    639 assert json_path.suffixes == [
    640     \".ast\",
    641     \".json\",
    642 ], f\"{json_path} is not a *.ast.json file\"
    644 if repo.uses_lean3:

FileNotFoundError: /home2/shuming/Lean/Tmp/tmpbq4ytl3q/lean4-example/.lake/packages/mathlib/.lake/build/ir/Mathlib/Data/Real/Basic.ast.json does not exist"
}

However, when I remove the sum_choose_eq_Ico theorem in Lean4Example.lean, it works.

[yangky11]

Most likely, it can be solved by having more memory: #124. Is that an option for you? We're working on reducing the memory usage, but it's probably going to take some time.

[yangky11]

@moyvbai FYI, we made some progress in reducing the memory consumption in the most recent version (v1.7.0). You might want to upgrade and try again.

[moyvbai]

Thanks for your reply, I will use it and give feedback