I'm currently trying to use this repo for the BFS-Prover-V2 planner. The BFS-Prover-V2 repo comes with lean-dojo==2.1.3 and I tried tracing this repo with that version yesterday but got an error. Unfortunately, I don't have the logs saved. Today I tried upgrading to lean-dojo==4.20.0 (in hopes that a later version of lean-dojo has fixed the issue) and tracing this repo with the following script:
✔ [2/3] Built Lean4Repl
Build completed successfully.
2025-11-01 20:43:13,566 INFO worker.py:1908 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265
0%| | 4/4421 [00:00<05:19, 13.85it/s]
Traceback (most recent call last):
File "/home/anon/BFS-Prover-V2/trace-test.py", line 6, in <module>
trace(repo, build_deps=True)
File "/home/anon/BFS-Prover-V2/venv/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/anon/BFS-Prover-V2/venv/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/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 1127, in from_traced_files
traced_files = list(
^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/tqdm/std.py", line 1181, in __iter__
for obj in iterable:
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 170, in get_generator
yield self.get_next_unordered()
^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 370, in get_next_unordered
return ray.get(future)
^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/_private/auto_init_hook.py", line 22, in auto_init_wrapper
return fn(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/_private/client_mode_hook.py", line 104, in wrapper
return func(*args, **kwargs)
^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 2849, in get
values, debugger_breakpoint = worker.get_objects(object_refs, timeout=timeout)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 937, in get_objects
raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(AssertionError): ray::_TracedRepoHelper.parse_traced_file() (pid=448781, ip=10.128.0.2, actor_id=6d38afb3876f34c83ab6671f01000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x7f658f317190>)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 993, in parse_traced_file
return TracedFile.from_traced_file(self.root_dir, path, self.repo)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 535, in from_traced_file
return cls._from_lean4_traced_file(root_dir, json_path, repo)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 555, in _from_lean4_traced_file
ast = FileNode.from_data(data, lean_file)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/anon/BFS-Prover-V2/venv/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/anon/BFS-Prover-V2/venv/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/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 1480, in from_data
assert len(children) == 2
^^^^^^^^^^^^^^^^^^
AssertionError
I've attached the full log from running the trace-test.py script.
I'm currently trying to use this repo for the BFS-Prover-V2 planner. The BFS-Prover-V2 repo comes with lean-dojo==2.1.3 and I tried tracing this repo with that version yesterday but got an error. Unfortunately, I don't have the logs saved. Today I tried upgrading to lean-dojo==4.20.0 (in hopes that a later version of lean-dojo has fixed the issue) and tracing this repo with the following script:
When I ran it, I got the following error:
I've attached the full log from running the trace-test.py script.
trace-test-log-yangky11-miniF2F-lean4.txt
Additional Info:
elan 4.1.2 (58e8d545e 2025-05-26)
Lake version 5.0.0-c375e19 (Lean version 4.10.0)
Python 3.11.2
EDIT:
typo: should be lean-dojo==4.20.0 not 4.2.0