lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF

[njuyxw]

Description
I have found some tactics that cause the dojo environment to crash, reporting the following error: lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF

Detailed Steps to Reproduce the Behavior
Test sample: "MiniF2F/Test.lean","mathd_numbertheory_237"
Test tactic: "congr 1"

Test Code:
‘’‘
from lean_dojo import *
import lean_dojo
repo = LeanGitRepo(
"https://github.com/wzj423/lean-dojo-mew",
"1ef4e4cac9dd370b7be6d648ce135a06aa6fce5f",
)
th=Theorem(repo,"MiniF2F/Test.lean","mathd_numbertheory_237")
dojo, state_0 = Dojo(th,additional_imports=["Mathlib.Tactic"]).enter()
action="congr 1"
state_1 = dojo.run_tac(state_0, action)
print(state_1)
’‘’

Error Report:
2024-08-25 12:52:09.445 | DEBUG | lean_dojo.interaction.dojo:_submit_request:379 - {"sid": 0, "cmd": "congr 1"}
Traceback (most recent call last):
File "home/conda/envs/lean/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 418, in _read_next_line
index = self.proc.expect(["\n", f"{_REPL_PROMPT}.?\n"])
File "home/conda/envs/lean/lib/python3.9/site-packages/pexpect/spawnbase.py", line 354, in expect
return self.expect_list(compiled_pattern_list,
File "home/conda/envs/lean/lib/python3.9/site-packages/pexpect/spawnbase.py", line 383, in expect_list
return exp.expect_loop(timeout)
File "home/conda/envs/lean/lib/python3.9/site-packages/pexpect/expect.py", line 179, in expect_loop
return self.eof(e)
File "home/conda/envs/lean/lib/python3.9/site-packages/pexpect/expect.py", line 122, in eof
raise exc
pexpect.exceptions.EOF: End Of File (EOF). Exception style platform.
<pexpect.pty_spawn.spawn object at 0x7fc3b7c4feb0>
command: /home/.elan/bin/lake
args: [b'/home/.elan/bin/lake', b'env', b'lean', b'--threads=1', b'--memory=32768', b'MiniF2F/Test3kldb649.lean']
buffer (last 100 chars): ''
before (last 100 chars): ''
after: <class 'pexpect.exceptions.EOF'>
match: None
match_index: None
exitstatus: 1
flag_eof: True
pid: 990853
child_fd: 7
closed: False
timeout: 600
delimiter: <class 'pexpect.exceptions.EOF'>
logfile: None
logfile_read: None
logfile_send: None
maxread: 1
ignorecase: False
searchwindowsize: None
delaybeforesend: 0.05
delayafterclose: 0.1
delayafterterminate: 0.1
searcher: searcher_re:
0: re.compile('\n')
1: re.compile('REPL>.?\n')

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File home/conda/envs/lean/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 382, in _submit_request
res, msg = self._read_next_line()
File "home/conda/envs/lean/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 429, in _read_next_line
raise EOFError
EOFError

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "home/codes/leanRL/rerankATP/try.py", line 9, in
state_1 = dojo.run_tac(state_0, action)
File "home/conda/envs/lean/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 332, in run_tac
res = self._submit_request(req)
File "home/conda/envs/lean/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 384, in _submit_request
raise DojoCrashError("Unexpected EOF")
lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF

I explored the cause of DojoCrashError and found that:
lean reported a 'maximum recursion depth error' and instructed me to set the option maxRecDepth . However, I do not know how to increase the recursive depth of Lean in Dojo. The issue arises with many tactics generated by LLMs. When such errors occur, Dojo throws a CrashError, causing the BFS search to be interrupted. This limitation affects the overall performance of some LLMs. I hope you can help me with this.

Platform Information
Leandojo version: 2.1.2 [Different versions of leandojo have the same problem]
python version: 3.9.19
lean version: 4.7.0
lake version: 5.0.0-6fce8f7
elan version: 3.1.1 (71ddc6633 2024-02-22)

[yifan123]

You can run lake exe cache get to check if a specific toolchain is uninstalled or navigate to your code directory and run lake env lean --threads=1 --memory=32768 MiniF2F/Test.lean to see the output.

Here is my steps to solve a similar EOF error.

I encountered the same error when running the following mathlib example:

from lean_dojo import *
repo = LeanGitRepo("https://github.com/leanprover-community/mathlib4", "29dcec074de168ac2bf835a77ef68bbe069194c5")
theorem = Theorem(repo, "Mathlib/GroupTheory/PGroup.lean", "IsPGroup.powEquiv_symm_apply")
with Dojo(theorem) as (dojo, init_state):
  print(init_state)

The output is lean_dojo.interaction.dojo.DojoInitError: Unexpected EOF.

To resolve the error, I followed these steps:

Navigate to the directory:

cd .cache/lean_dojo/leanprover-community-mathlib4-29dcec074de168ac2bf835a77ef68bbe069194c5/mathlib4/
lake env lean --threads=1 --memory=32768 Mathlib/GroupTheory/PGroup.lean

The output indicated an error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

Running lake exe cache get confirmed the error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

However, when I checked ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1, the directory existed.

To fix this, I first removed the directory with rm -rf ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1 and then installed the toolchain using elan toolchain install leanprover/lean4:v4.10.0-rc1. This resolved the error.

[Thomas333333]

You can run lake exe cache get to check if a specific toolchain is uninstalled or navigate to your code directory and run lake env lean --threads=1 --memory=32768 MiniF2F/Test.lean to see the output.

Here is my steps to solve a similar EOF error.

I encountered the same error when running the following mathlib example:

from lean_dojo import *
repo = LeanGitRepo("https://github.com/leanprover-community/mathlib4", "29dcec074de168ac2bf835a77ef68bbe069194c5")
theorem = Theorem(repo, "Mathlib/GroupTheory/PGroup.lean", "IsPGroup.powEquiv_symm_apply")
with Dojo(theorem) as (dojo, init_state):
  print(init_state)

The output is lean_dojo.interaction.dojo.DojoInitError: Unexpected EOF.

To resolve the error, I followed these steps:

Navigate to the directory:

cd .cache/lean_dojo/leanprover-community-mathlib4-29dcec074de168ac2bf835a77ef68bbe069194c5/mathlib4/
lake env lean --threads=1 --memory=32768 Mathlib/GroupTheory/PGroup.lean

The output indicated an error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

Running lake exe cache get confirmed the error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

However, when I checked ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1, the directory existed.

To fix this, I first removed the directory with rm -rf ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1 and then installed the toolchain using elan toolchain install leanprover/lean4:v4.10.0-rc1. This resolved the error.

It works well to my problem.
In Lean-dojo/ReProver, when I use command python prover/evaluate.py --data-path data/leandojo_benchmark_4/random/ --gen_ckpt_path kaiyuy/leandojo-lean4-tacgen-byt5-small --split test --num-workers 15 --num-gpus 1. It shows similar warning of EOF:

�[36m(ProverActor pid=164235)�[0m 2024-09-10 20:03:01.923 | INFO     | prover.proof_search:search:83 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='29dcec074de168ac2bf835a77ef68bbe069194c5'), file_path=PosixPath('Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean'), full_name='Besicovitch.SatelliteConfig.exists_normalized_aux1')
�[36m(ProverActor pid=164244)�[0m 2024-09-10 20:03:01.910 | WARNING  | prover.proof_search:search:134 - Unexpected EOF

[saranpandian]

You can run lake exe cache get to check if a specific toolchain is uninstalled or navigate to your code directory and run lake env lean --threads=1 --memory=32768 MiniF2F/Test.lean to see the output.

Here is my steps to solve a similar EOF error.

I encountered the same error when running the following mathlib example:

from lean_dojo import *
repo = LeanGitRepo("https://github.com/leanprover-community/mathlib4", "29dcec074de168ac2bf835a77ef68bbe069194c5")
theorem = Theorem(repo, "Mathlib/GroupTheory/PGroup.lean", "IsPGroup.powEquiv_symm_apply")
with Dojo(theorem) as (dojo, init_state):
  print(init_state)

The output is lean_dojo.interaction.dojo.DojoInitError: Unexpected EOF.

To resolve the error, I followed these steps:

Navigate to the directory:

cd .cache/lean_dojo/leanprover-community-mathlib4-29dcec074de168ac2bf835a77ef68bbe069194c5/mathlib4/
lake env lean --threads=1 --memory=32768 Mathlib/GroupTheory/PGroup.lean

The output indicated an error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

Running lake exe cache get confirmed the error: the toolchain 'leanprover/lean4.10.0-rc1' was not installed.

However, when I checked ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1, the directory existed.

To fix this, I first removed the directory with rm -rf ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1 and then installed the toolchain using elan toolchain install leanprover/lean4:v4.10.0-rc1. This resolved the error.

This worked for me. Thanks a lot