lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF #207

njuyxw · 2024-08-25T05:04:16Z

njuyxw
Aug 25, 2024

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)

Answered by yifan123

Aug 25, 2024

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 th…

View full answer

yifan123 · 2024-08-25T09:14:43Z

yifan123
Aug 25, 2024

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.

0 replies

Thomas333333 · 2024-09-10T13:00:12Z

Thomas333333
Sep 10, 2024

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

0 replies

saranpandian · 2024-09-15T18:32:24Z

saranpandian
Sep 15, 2024

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

0 replies

yangky11 · 2024-09-18T02:19:05Z

yangky11
Sep 18, 2024
Maintainer

Thanks @yifan123. I'm converting this issue to discussion so that other people can see.

0 replies

Xuekai-Zhu · 2024-12-09T13:08:46Z

Xuekai-Zhu
Dec 9, 2024

I found this doesn't work now. If you have time, please help me.
Thanks a lot !
when i run

rm -rf ~/.elan/update-hashes/leanprover--lean4---v4.10.0-rc1 
elan toolchain install leanprover/lean4:v4.10.0-rc1

Then,

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

output:

file 'Mathlib/Order/Boundednkwfj464.lean' not found

Finally, I still hit on EOF

Traceback (most recent call last):
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 412, in _read_next_line
    index = self.proc.expect(["\n", f"{_REPL_PROMPT}.*?\n"])
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pexpect/spawnbase.py", line 354, in expect
    return self.expect_list(compiled_pattern_list,
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pexpect/spawnbase.py", line 383, in expect_list
    return exp.expect_loop(timeout)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pexpect/expect.py", line 179, in expect_loop
    return self.eof(e)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/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 0x155495f6be20>
command: /home/zhuxuekai/.elan/bin/lake
args: [b'/home/zhuxuekai/.elan/bin/lake', b'env', b'lean', b'--threads=1', b'--memory=32768', b'Mathlib/Order/Boundednkwfj464.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: 1644546
child_fd: 113
closed: False
timeout: 60
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/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 182, in __enter__
    res = json.loads(self._read_next_line()[0])
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 423, in _read_next_line
    raise EOFError
EOFError

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/scratch2/nlp/zhuxuekai/reasoning_flow/baselines/gfn_ntp/proof_flow/scripts/gfn_tuning/train.py", line 54, in train
    trainer.fit(model=task, datamodule=data)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/trainer.py", line 538, in fit
    call._call_and_handle_interrupt(
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/call.py", line 47, in _call_and_handle_interrupt
    return trainer_fn(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/trainer.py", line 574, in _fit_impl
    self._run(model, ckpt_path=ckpt_path)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/trainer.py", line 981, in _run
    results = self._run_stage()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/trainer.py", line 1025, in _run_stage
    self.fit_loop.run()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/fit_loop.py", line 205, in run
    self.advance()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/fit_loop.py", line 363, in advance
    self.epoch_loop.run(self._data_fetcher)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/training_epoch_loop.py", line 140, in run
    self.advance(data_fetcher)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/training_epoch_loop.py", line 250, in advance
    batch_output = self.automatic_optimization.run(trainer.optimizers[0], batch_idx, kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/optimization/automatic.py", line 190, in run
    self._optimizer_step(batch_idx, closure)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/optimization/automatic.py", line 268, in _optimizer_step
    call._call_lightning_module_hook(
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/call.py", line 167, in _call_lightning_module_hook
    output = fn(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/core/module.py", line 1306, in optimizer_step
    optimizer.step(closure=optimizer_closure)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/core/optimizer.py", line 153, in step
    step_output = self._strategy.optimizer_step(self._optimizer, closure, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/strategies/strategy.py", line 238, in optimizer_step
    return self.precision_plugin.optimizer_step(optimizer, model=model, closure=closure, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/plugins/precision/precision.py", line 122, in optimizer_step
    return optimizer.step(closure=closure, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/torch/optim/optimizer.py", line 487, in wrapper
    out = func(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/torch/optim/optimizer.py", line 91, in _use_grad
    ret = func(self, *args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/torch/optim/adamw.py", line 197, in step
    loss = closure()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/plugins/precision/precision.py", line 108, in _wrap_closure
    closure_result = closure()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/optimization/automatic.py", line 144, in __call__
    self._result = self.closure(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/torch/utils/_contextlib.py", line 116, in decorate_context
    return func(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/optimization/automatic.py", line 129, in closure
    step_output = self._step_fn()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/loops/optimization/automatic.py", line 317, in _training_step
    training_step_output = call._call_strategy_hook(trainer, "training_step", *kwargs.values())
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/trainer/call.py", line 319, in _call_strategy_hook
    output = fn(*args, **kwargs)
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/pytorch_lightning/strategies/strategy.py", line 390, in training_step
    return self.lightning_module.training_step(*args, **kwargs)
  File "/scratch2/nlp/zhuxuekai/reasoning_flow/baselines/gfn_ntp/proof_flow/src/gfn_tuning/ntp.py", line 474, in training_step
    dojo, initial_state = self.dojo_cache.get(theorem)
  File "/scratch2/nlp/zhuxuekai/reasoning_flow/baselines/gfn_ntp/proof_flow/src/lean_env_cache.py", line 45, in get
    dojo, initial_state = dojo.__enter__()
  File "/home/zhuxuekai/miniconda3/envs/reasoning/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 189, in __enter__
    raise DojoInitError("Unexpected EOF")
lean_dojo.interaction.dojo.DojoInitError: Unexpected EOF

1 reply

yangky11 Dec 13, 2024
Maintainer

Do you have a minimal example that I can try to run?

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF #207

{{title}}

Replies: 5 comments 1 reply

{{title}}

{{title}}

{{title}}

{{title}}

{{title}}

{{title}}

Select a reply

lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF #207

njuyxw Aug 25, 2024

Replies: 5 comments · 1 reply

yifan123 Aug 25, 2024

Thomas333333 Sep 10, 2024

saranpandian Sep 15, 2024

yangky11 Sep 18, 2024 Maintainer

Xuekai-Zhu Dec 9, 2024

yangky11 Dec 13, 2024 Maintainer

njuyxw
Aug 25, 2024

Replies: 5 comments 1 reply

yifan123
Aug 25, 2024

Thomas333333
Sep 10, 2024

saranpandian
Sep 15, 2024

yangky11
Sep 18, 2024
Maintainer

Xuekai-Zhu
Dec 9, 2024

yangky11 Dec 13, 2024
Maintainer