Error when trying to load theorem through leandojo

[script-jpg]

I'm not sure if this repo has leandojo in mind during its creation but I got this issue when trying to use this repo with leandojo.
Here is my script:

(venv) anon@instance-20251031-173928:~/BFS-Prover-V2$ cat trace-test.py 
from lean_dojo import *
import os

url = 'https://github.com/rahul3613/miniF2F-lean4/'
commit = 'HEAD'
repo = LeanGitRepo(url, commit)
trace(repo, build_deps=False)
theorem = Theorem(repo, "formal/test.lean", "mathd_algebra_478")
with Dojo(theorem) as (dojo, init_state):
     print(init_state)

Here is the traceback:

(venv) anon@instance-20251031-173928:~/BFS-Prover-V2$ python trace-test.py 
2025-11-01 19:02:18.254 | INFO     | lean_dojo.data_extraction.trace:trace:248 - Loading the traced repo from /home/anon/BFS-Prover-V2/cache/lean_dojo/rahul3613-miniF2F-lean4-d2e847c98dee1acf5355f5de2ab71f3fcd24849a/miniF2F-lean4
2025-11-01 19:02:20,028 INFO worker.py:1908 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████| 757/757 [00:24<00:00, 31.37it/s]
Following Github server redirection from /repos/leanprover/std4 to /repositories/529900532
2025-11-01 19:02:49.090 | WARNING  | lean_dojo.data_extraction.lean:__post_init__:579 - LeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: v4.0.0
Traceback (most recent call last):
  File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py", line 163, in __enter__
    traced_file = self._locate_traced_file(traced_repo_path)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py", line 213, in _locate_traced_file
    return TracedFile.from_traced_file(traced_repo_path, json_path, self.repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 530, in from_traced_file
    raise FileNotFoundError(f"{json_path} does not exist")
FileNotFoundError: /home/anon/BFS-Prover-V2/cache/lean_dojo/rahul3613-miniF2F-lean4-d2e847c98dee1acf5355f5de2ab71f3fcd24849a/miniF2F-lean4/.lake/build/ir/formal/test.ast.json does not exist

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/anon/BFS-Prover-V2/trace-test.py", line 9, in <module>
    with Dojo(theorem) as (dojo, init_state):
  File "/home/anon/BFS-Prover-V2/venv/lib/python3.11/site-packages/lean_dojo/interaction/dojo.py", line 165, in __enter__
    raise DojoInitError(
lean_dojo.interaction.dojo.DojoInitError: Cannot find the *.ast.json file for Theorem(repo=LeanGitRepo(url='https://github.com/rahul3613/miniF2F-lean4', commit='d2e847c98dee1acf5355f5de2ab71f3fcd24849a'), file_path=PosixPath('formal/test.lean'), full_name='mathd_algebra_478') in /home/anon/BFS-Prover-V2/cache/lean_dojo/rahul3613-miniF2F-lean4-d2e847c98dee1acf5355f5de2ab71f3fcd24849a/miniF2F-lean4.