EOF error when additional_imports = ['Mathlib']

[wclsn]

Description What happened? I try to add additional imports ('Mathlib') for a dojo env since it will give everything so that we do not need to import other mathlib modules, but it raises an EOF error. Detailed Steps to Reproduce the Behavior

from lean_dojo import Dojo, Theorem, LeanGitRepo
if __name__ == "__main__":
    repo = LeanGitRepo(
        "https://github.com/leanprover-community/mathlib4",
        "3c307701fa7e9acbdc0680d7f3b9c9fed9081740"
    ) 

    host_wd = os.getcwd()
    print("initialization begin")
    theorem = Theorem(repo, Path("Mathlib/Algebra/Algebra/Basic.lean"), "algebraMap.coe_zero")
    dojo, state_0 = Dojo(theorem, additional_imports=['Mathlib']).__enter__()

Logs in Debug Mode Traceback (most recent call last): File "/home//miniforge3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 233, in enter res = json.loads(self._read_next_line()[0]) File "/home/miniforge3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 527, in _read_next_line raise EOFError EOFError

During handling of the above exception, another exception occurred:

Traceback (most recent call last): File "/home/lean4math/test/test_dojo.py", line 18, in dojo, state_0 = Dojo(theorem, additional_imports=['Mathlib']).enter() File "/home/miniforge3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 265, in enter raise ex File "/home/miniforge3/envs/leandojo/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 240, in enter raise DojoInitError("EOF") lean_dojo.interaction.dojo.DojoInitError: EOF

Platform Information

• OS: Ubuntu 20.04
• LeanDojo Version 1.7.1
• python 3.10.13

[wclsn]

I also attempted to assign additional imports to a list of string with a length of 10, which ultimately resulted in triggering an EOF error. I tested it with leandojo 1.8.2, but unfortunately, the issue persists.

[yangky11]

Trying to import Mathlib in a file within mathlib will lead to errors due to circular imports. This happens w/ or w/o LeanDojo, e.g., when you manually add import Mathlib to Mathlib/Algebra/Algebra/Basic.lean in VS Code.

[wclsn]

Thank you for your reply. Since I am relatively new to Lean, I have another question. How can I add additional imports to ensure that my theorem can access as many other theorems as possible without encountering any "unknown" issues?

Whatever, this issue will be closed.

[yangky11]

You can create a new repo and import mathlib (or any other repos) in your repo.

[wclsn]

Thank you!