subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1. #99

parsifal-chx · 2023-11-29T07:40:49Z

parsifal-chx
Nov 29, 2023

Hi! I'm encountering a challenging issue while running a program that interacts with Lean. My operating environment includes Ubuntu 20.04, Python 3.10, and Lean 4.2. Below are my code and a screenshot of the debug process.

debug:

Answered by yangky11

Dec 14, 2023

@parsifal-chx @ohyeat It should be fixed in #108. Could you please try and let me know if the error still persists?

View full answer

yangky11 · 2023-11-29T21:27:14Z

yangky11
Nov 29, 2023
Maintainer

Hi,

Can you upgrade to the latest version (v1.4.1) and try again? Please also post the code in a way that I can directly copy (not just a screenshot). Thanks.

0 replies

parsifal-chx · 2023-11-30T02:07:14Z

parsifal-chx
Nov 30, 2023
Author

Thanks for the response, This is a very simple demo. Following your advice, I upgraded the version, but the problem still persists.

from lean_dojo import *

repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "a61b40b90afba0ee5a3357665a86f7d0bb57461d")
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")

with Dojo(theorem) as (dojo, init_state):
    print(init_state)
    result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, ←add_assoc]")
    assert isinstance(result, ProofFinished)
    print(result)

error

2023-11-30 11:16:46.961 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-11-30 11:16:52.968 | INFO     | lean_dojo.utils:execute:113 - 
2023-11-30 11:16:52.968 | ERROR    | lean_dojo.utils:execute:114 - error: unknown target `Lean4Repl`

Traceback (most recent call last):
  File "/home/rise/learn/leanDojo/interact.py", line 6, in <module>
    with Dojo(theorem) as (dojo, init_state):
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 293, in __enter__
    raise ex
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 237, in __enter__
    self.container.run(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/container.py", line 193, in run
    execute(cmd, capture_output=capture_output)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/utils.py", line 115, in execute
    raise ex
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/utils.py", line 110, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1.

0 replies

yangky11 · 2023-11-30T03:43:03Z

yangky11
Nov 30, 2023
Maintainer

I was not able to reproduce the error. Can you run in debug mode (with the environment variable VERBOSE=1) and paste the output here? Here is mine:

(lean-dojo) kaiyu@tensorlab-DGX:~/LeanDojo$ VERBOSE=1 python tmp.py 
2023-11-29 19:41:35.623 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
2023-11-29 19:41:40.018 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-11-29 19:41:40.019 | DEBUG    | lean_dojo.interaction.dojo:__enter__:192 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='a61b40b90afba0ee5a3357665a86f7d0bb57461d'), file_path=PosixPath('Lean4Example.lean'), full_name='hello_world')
2023-11-29 19:41:40.020 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:158 - The traced repo is available in the cache.
2023-11-29 19:41:41.899 | DEBUG    | lean_dojo.interaction.dojo:_modify_file:413 - Modifying Lean4Example.lean
2023-11-29 19:41:41.900 | DEBUG    | lean_dojo.interaction.dojo:__enter__:230 - Launching the proof using <class 'lean_dojo.container.NativeContainer'>
2023-11-29 19:41:42.677 | DEBUG    | lean_dojo.container:run:183 - lake build Lean4Repl
2023-11-29 19:41:48.185 | WARNING  | lean_dojo.container:run_interactive:209 - Disregarding `cpu_limit = 1 since NativeContainer does not support CPU limit.`
2023-11-29 19:41:48.186 | WARNING  | lean_dojo.container:run_interactive:213 - Disregarding `memory_limit = 16g` since NativeContainer does not support memory limit.
2023-11-29 19:41:48.981 | DEBUG    | lean_dojo.container:run_interactive:221 - lake env lean Lean4Example.lean
2023-11-29 19:41:49.276 | DEBUG    | lean_dojo.interaction.dojo:_read_next_line:605 - REPL> {"tacticState": "a b c : Nat\n⊢ a + b + c = a + c + b", "sid": 0, "error": null}
TacticState(pp='a b c : Nat\n⊢ a + b + c = a + c + b', id=0, message=None)
2023-11-29 19:41:49.277 | DEBUG    | lean_dojo.interaction.dojo:_submit_request:562 - Request: {"sid": 0, "cmd": "rw [add_assoc, add_comm b, ←add_assoc]"}
2023-11-29 19:41:49.284 | DEBUG    | lean_dojo.interaction.dojo:_read_next_line:605 - REPL> {"tacticState": "no goals", "sid": 1, "error": null}
ProofFinished(tactic_state_id=1, message='')
2023-11-29 19:41:49.284 | DEBUG    | lean_dojo.interaction.dojo:_submit_request:562 - Request: exit
2023-11-29 19:41:49.302 | DEBUG    | lean_dojo.interaction.dojo:_read_next_line:605 - 
2023-11-29 19:41:49.302 | DEBUG    | lean_dojo.interaction.dojo:_cleanup:339 - Cleaning up.
2023-11-29 19:41:49.302 | DEBUG    | lean_dojo.interaction.dojo:_cleanup_container:349 - Cleaning up the container.
2023-11-29 19:41:50.382 | DEBUG    | lean_dojo.interaction.dojo:_cleanup_tmp_dir:365 - Cleaning up the temporary directory.

1 reply

parsifal-chx Nov 30, 2023
Author

Thanks for your patient guidance.

(chx-py3.10) rise@rise-Alienware-Aurora-R7:~/learn/leanDojo$ VERBOSE=1 python interact.py 
2023-11-30 15:14:34.112 | DEBUG    | lean_dojo.constants:<module>:68 - Using GitHub personal access token for authentication
2023-11-30 15:14:44.314 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-11-30 15:14:44.314 | DEBUG    | lean_dojo.interaction.dojo:__enter__:192 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='a61b40b90afba0ee5a3357665a86f7d0bb57461d'), file_path=PosixPath('Lean4Example.lean'), full_name='hello_world')
2023-11-30 15:14:44.316 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:158 - The traced repo is available in the cache.
2023-11-30 15:14:50.087 | DEBUG    | lean_dojo.interaction.dojo:_modify_file:413 - Modifying Lean4Example.lean
2023-11-30 15:14:50.089 | DEBUG    | lean_dojo.interaction.dojo:__enter__:230 - Launching the proof using <class 'lean_dojo.container.NativeContainer'>
2023-11-30 15:14:50.791 | DEBUG    | lean_dojo.container:run:183 - lake build Lean4Repl
2023-11-30 15:14:50.910 | INFO     | lean_dojo.utils:execute:113 - 
2023-11-30 15:14:50.910 | ERROR    | lean_dojo.utils:execute:114 - error: unknown target `Lean4Repl`

Traceback (most recent call last):
  File "/home/rise/learn/leanDojo/interact.py", line 6, in <module>
    with Dojo(theorem) as (dojo, init_state):
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 293, in __enter__
    raise ex
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 237, in __enter__
    self.container.run(
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/container.py", line 193, in run
    execute(cmd, capture_output=capture_output)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/utils.py", line 115, in execute
    raise ex
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/site-packages/lean_dojo/utils.py", line 110, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/home/rise/anaconda3/envs/chx-py3.10/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1.

parsifal-chx · 2023-11-30T08:17:57Z

parsifal-chx
Nov 30, 2023
Author

I've observed a phenomenon while using PyCharm in debug mode and setting breakpoints. Before executing the self.container.run() function.

if I go to the temp/rempc3zd7tco/lean-example folder and run the lake build lean4repl command, then continue executing the self.container.run() function.

it runs successfully.

However, the error reoccurs in subsequent runs.

11 replies

yangky11 Dec 13, 2023
Maintainer

@parsifal-chx Do you still get error: unknown target Lean4Repl when running lake build Lean4Repl in /tmp/tmpxxxx/lean4-example/workspace/lean4-example? If so, can you please show me the lakefile.lean in that directory?

parsifal-chx Dec 14, 2023
Author

Yes, the problem still exists.
https://github.com/parsifal-chx/lean4-example
It contains two folders and The folder with s in the file names can execute the lake build Lean4Repl command

ohyeat Dec 14, 2023

Got the same problem when I was trying demo-lean4.ipynb where the target repo is mathlib4. It's really weird that running lake build Lean4Repl in /tmp/tmpxxxx/mathlib4/ is OK while running the command in /tmp/tmpxxxx/mathlib4/workspace/mathlib4/ returns error: unknown target Lean4Repl . I've compared the contents of Lean4Repl.lean and lakefile.lean from the two dirs respectively, and found no difference.

yangky11 Dec 14, 2023
Maintainer

@parsifal-chx @ohyeat It should be fixed in #108. Could you please try and let me know if the error still persists?

Answer selected by parsifal-chx

ohyeat Dec 14, 2023

@yangky11 My problem is solved, thanks!

parsifal-chx Dec 14, 2023
Author

@yangky11 The problem has been solved, thank you!

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1. #99

{{title}}

{{editor}}'s edit

{{editor}}'s edit

Replies: 4 comments 12 replies

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

{{title}}

{{title}}

{{title}}

{{title}}

{{title}}

{{editor}}'s edit

{{editor}}'s edit

{{title}}

{{title}}

Select a reply

subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1. #99

parsifal-chx Nov 29, 2023

Replies: 4 comments · 12 replies

yangky11 Nov 29, 2023 Maintainer

parsifal-chx Nov 30, 2023 Author

yangky11 Nov 30, 2023 Maintainer

parsifal-chx Nov 30, 2023 Author

parsifal-chx Nov 30, 2023 Author

yangky11 Dec 13, 2023 Maintainer

parsifal-chx Dec 14, 2023 Author

ohyeat Dec 14, 2023

yangky11 Dec 14, 2023 Maintainer

ohyeat Dec 14, 2023

parsifal-chx Dec 14, 2023 Author

parsifal-chx
Nov 29, 2023

Replies: 4 comments 12 replies

yangky11
Nov 29, 2023
Maintainer

parsifal-chx
Nov 30, 2023
Author

yangky11
Nov 30, 2023
Maintainer

parsifal-chx Nov 30, 2023
Author

parsifal-chx
Nov 30, 2023
Author

yangky11 Dec 13, 2023
Maintainer

parsifal-chx Dec 14, 2023
Author

yangky11 Dec 14, 2023
Maintainer

parsifal-chx Dec 14, 2023
Author