Error in tracing local repo

[AquiloZh]

I wanna trace a local stand-alone lean project for some test while tracing process always stopped at last few file and went wrong

>>> from lean_dojo import *
>>> repo = LeanGitRepo.from_path('leanProj')
>>> trace_repo = trace(repo)
2025-06-06 20:53:19.644 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:210 - Tracing LeanGitRepo(url='/home/aquilo/minimo/leanProj', commit='fbf3f1fb178d3adee1ca8cfdaf2e931e9666c92a')
Build completed successfully.
100%|███████████████████████████████████████████████████████████████████████████▊| 1516/1521 [1:12:54<27:33, 330.61s/it]2025-06-06 23:07:50.615 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj/Basic.ast.json
2025-06-06 23:07:50.646 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj/Basic.dep_paths
2025-06-06 23:07:50.646 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj/Group.ast.json
2025-06-06 23:07:50.647 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/Main.ast.json
2025-06-06 23:07:50.647 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj.ast.json
2025-06-06 23:07:50.647 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj/Group.dep_paths
2025-06-06 23:07:50.648 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/LeanProj.dep_paths
2025-06-06 23:07:50.649 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpo8yf3q4h/leanProj/.lake/build/ir/lean/Main.dep_paths
Build completed successfully.
2025-06-06 23:08:00,339 INFO worker.py:1879 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265
  0%|                                                                                          | 0/1517 [00:01<?, ?it/s]Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 247, in trace
    cached_path = get_traced_repo_path(repo, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 215, in get_traced_repo_path
    traced_repo = TracedRepo.from_traced_files(src_dir, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 1125, in from_traced_files
    traced_files = list(
                   ^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/tqdm/std.py", line 1181, in __iter__
    for obj in iterable:
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 170, in get_generator
    yield self.get_next_unordered()
          ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 370, in get_next_unordered
    return ray.get(future)
           ^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/_private/auto_init_hook.py", line 21, in auto_init_wrapper
    return fn(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/_private/worker.py", line 2822, in get
    values, debugger_breakpoint = worker.get_objects(object_refs, timeout=timeout)
                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/ray/_private/worker.py", line 930, in get_objects
    raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(AssertionError): ray::_TracedRepoHelper.parse_traced_file() (pid=313088, ip=172.22.205.162, actor_id=39434d0b0b84d2475d12a54e01000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x7c7e605eeed0>)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 991, in parse_traced_file
    return TracedFile.from_traced_file(self.root_dir, path, self.repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 536, in from_traced_file
    return cls._from_lean4_traced_file(root_dir, json_path, repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 556, in _from_lean4_traced_file
    ast = FileNode.from_data(data, lean_file)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 253, in from_data    node = Node.from_data(node_data, lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 1360, in from_data
    children = _parse_children(node_data, lean_file)
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 267, in _parse_children
    node = Node.from_data(d["node"], lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 601, in from_data    children = _parse_children(node_data, lean_file)
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 267, in _parse_children
    node = Node.from_data(d["node"], lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/aquilo/minimo/myenv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 1401, in from_data
    assert isinstance(children[0], AtomNode) and children[0].val == "import"
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
AssertionError

[yangky11]

Hi, I'm happy to take a look if you can provide an example with public repos (rather than local repos).

[AquiloZh]

https://github.com/AquiloZh/DojoTest/
take a while on tracing the publice one, still have simillar issue. get stuck on last few step.

[yangky11]

It was likely due to Lean v4.20.0. I fixed in the the current main branch. Please try it out and let me know if the error still persists.

[AquiloZh]

Seems the promblem is solve, now the error is caused by oom instead. Is there a general solution on oom?

[yangky11]

I don't think there is a easy way to get rid of OOM errors. How much RAM were you using?

[AquiloZh]

16GB

[yangky11]

That might not be enough. Tracing a large repo like mathlib requires 64–128GB. Since the repo only needs to be traced once, you could try tracing it on a machine with larger RAM and copy the cache files into your machine.