lean_dojo_repl not working

[durant42040]

Description
The error occurred when running Dojo.enter(), it crashes at res = json.loads(self._read_next_line()[0]). After debugging for a while, the issue seems to stem from the loop function in Lean4Repl.lean. I've provided a example below. It seems to be parsing an empty string when there is no input, which causes it to crash. What is the expected behavior?

Detailed Steps to Reproduce the Behavior
Following the logic of Dojo.enter(), here's a minimal example that reproduces the error.
https://github.com/durant42040/lean4-example/tree/repl
run lake env lean --run Lean4Example.lean

Logs in Debug Mode

lean4-example % lake env lean --run Lean4Example.lean
Lean4Example.lean:5:2: error: [fatal] failed to parse JSON offset 0: unexpected end of input
REPL> {"tacticState": "a b c : Nat\n⊢ a * (b + c) = a * b + a * c", "sid": 0, "error": null}

2025-07-23 16:13:50.942 | INFO     | leanlibrary.lean_agent.prover.proof_search:prove_sorry_theorems:582 - Found 6 sorry theorems to prove
Processing theorems from durant42040/lean4-example: 100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 6/6 [00:00<00:00, 34615.99theorem/s]
2025-07-23 16:13:50.942 | INFO     | leanlibrary.lean_agent.prover.proof_search:search_unordered:534 - Not distributed
2025-07-23 16:13:50.942 | INFO     | leanlibrary.lean_agent.prover.proof_search:search:112 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/durant42040/lean4-example', commit='a372e27e6488fb31dd0ba89c2c4c5e49f825ac18'), file_path=PosixPath('Lean4Example.lean'), full_name='add_mul')
2025-07-23 16:13:50.942 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:__enter__:248 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/durant42040/lean4-example', commit='a372e27e6488fb31dd0ba89c2c4c5e49f825ac18'), file_path=PosixPath('Lean4Example.lean'), full_name='add_mul')
2025-07-23 16:13:50.944 | DEBUG    | leanlibrary.lean_dojo.data_extraction.trace:get_traced_repo_path:247 - The traced repo is available in the cache.
2025-07-23 16:13:51.104 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:__enter__:264 - traced_repo_path, /work/10710/rhsiang/LeanLibrary/raid/.cache/lean_dojo/durant42040-lean4-example-a372e27e6488fb31dd0ba89c2c4c5e49f825ac18/lean4-example
2025-07-23 16:13:51.105 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_modify_file:350 - Modifying `Lean4Example.lean` into `/work/10710/rhsiang/LeanLibrary/raid/.cache/lean_dojo/durant42040-lean4-example-a372e27e6488fb31dd0ba89c2c4c5e49f825ac18/lean4-example/Lean4Examplew2xp57w3.lean`
2025-07-23 16:13:51.107 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:__enter__:271 - modified_path Lean4Examplew2xp57w3.lean
2025-07-23 16:13:51.127 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:510 - Waiting for next line from process 2569976
2025-07-23 16:13:55.210 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:512 - Got expect index: 0
2025-07-23 16:13:55.210 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:513 - proc.before: Lean4Examplew2xp57w3.lean:41:8: warning: declaration uses 'sorry'
2025-07-23 16:13:55.210 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:520 - Appending message: Lean4Examplew2xp57w3.lean:41:8: warning: declaration uses 'sorry'
2025-07-23 16:13:55.210 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:510 - Waiting for next line from process 2569976
2025-07-23 16:13:55.227 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:512 - Got expect index: 0
2025-07-23 16:13:55.227 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:513 - proc.before: Lean4Examplew2xp57w3.lean:46:2: error: [fatal] failed to parse JSON offset 0: unexpected end of input line:
2025-07-23 16:13:55.227 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:520 - Appending message: Lean4Examplew2xp57w3.lean:46:2: error: [fatal] failed to parse JSON offset 0: unexpected end of input line:
2025-07-23 16:13:55.227 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:510 - Waiting for next line from process 2569976
2025-07-23 16:13:55.241 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:512 - Got expect index: 1
2025-07-23 16:13:55.241 | DEBUG    | leanlibrary.lean_dojo.interaction.dojo:_read_next_line:513 - proc.before:
Traceback (most recent call last):
  File "<frozen runpy>", line 198, in _run_module_as_main
  File "<frozen runpy>", line 88, in _run_code
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/__main__.py", line 9, in <module>
    main()
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/lean_agent.py", line 229, in main
    agent.prove()
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/lean_agent.py", line 167, in prove
    prover.prove_sorry_theorems(
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/prover/proof_search.py", line 629, in prove_sorry_theorems
    self._process_theorem_batch(theorem_batch, positions_batch, repo, database)
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/prover/proof_search.py", line 650, in _process_theorem_batch
    results = self.search_unordered(
              ^^^^^^^^^^^^^^^^^^^^^^
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/prover/proof_search.py", line 535, in search_unordered
    return [
           ^
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/prover/proof_search.py", line 536, in <listcomp>
    self.prover.search(repo, thm, pos)
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_agent/prover/proof_search.py", line 126, in search
    with Dojo(thm, self.timeout, additional_imports=imps) as (
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_dojo/interaction/dojo.py", line 290, in __enter__
    raise ex
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_dojo/interaction/dojo.py", line 279, in __enter__
    res = json.loads(self._read_next_line()[0])
                     ^^^^^^^^^^^^^^^^^^^^^^
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_dojo/interaction/dojo.py", line 524, in _read_next_line
    self._check_alive()
  File "/work/10710/rhsiang/LeanLibrary/leanlibrary/lean_dojo/interaction/dojo.py", line 493, in _check_alive
    raise DojoCrashError(f"Unexpected exit code: {exit_code}")

Platform Information

• OS: MacOS, Linux
• Lean: v4.21.0

[yangky11]

will take a look when I have a chance (hopefully next week)

[yangky11]

I believe this is related to #211 and will not be solved anytime soon.