yifan123
commented
2 weeks ago 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.leanThe 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
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)