/bin/sh: 1: lake: not found

[mnluzimu]

When I run python scripts/trace_repos.py, this error always occures. I find it hard to locate the "lake" mentioned here.

2023-09-26 14:27:14.437 | INFO     | __main__:main:12 - Namespace(data_path='data')
2023-09-26 14:27:43.887 | INFO     | __main__:main:26 - Repos to trace: {LeanGitRepo(url='https://github.com/leanprover/std4', commit='dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8'), LeanGitRepo(url='https://github.com/JLimperg/aesop', commit='d13a9666e6f430b940ef8d092f1219e964b52a09')}
2023-09-26 14:27:44.708 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:131 - Tracing LeanGitRepo(url='https://github.com/leanprover/std4', commit='dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8')
2023-09-26 14:27:48.106 | INFO     | __main__:main:121 - Building std4
/bin/sh: 1: lake: not found
Traceback (most recent call last):
  File "/tmp/tmp0xhcp848/workspace/build_lean4_repo.py", line 165, in <module>
    main()
  File "/tmp/tmp0xhcp848/workspace/build_lean4_repo.py", line 147, in main
    run_cmd("lake build")
  File "/tmp/tmp0xhcp848/workspace/build_lean4_repo.py", line 27, in run_cmd
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/mnt/cache/luzimu/ReProver/reproverenv/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake build' returned non-zero exit status 127.

I an rather amateur and would really appreciate it if you guys could give me some suggestions as to why this error occured and how to solve it.

[yangky11]

Hi,

Please set the environment variableVERBOSE=1 and include the logs here.

[mnluzimu]

the logs are as below:

2023-09-27 10:42:19.807 | DEBUG    | lean_dojo.constants:<module>:70 - Using GitHub without authentication. Don't be surprised if you hit the API rate limit.
2023-09-27 10:42:21.031 | INFO     | __main__:main:12 - Namespace(data_path='data')
2023-09-27 10:42:44.973 | INFO     | __main__:main:26 - Repos to trace: {LeanGitRepo(url='https://github.com/JLimperg/aesop', commit='d13a9666e6f430b940ef8d092f1219e964b52a09'), LeanGitRepo(url='https://github.com/leanprover/std4', commit='dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8'), LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='355541ae7a2455222f179dcf7f074aa2c45eb8aa')}
2023-09-27 10:42:44.973 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:131 - Tracing LeanGitRepo(url='https://github.com/JLimperg/aesop', commit='d13a9666e6f430b940ef8d092f1219e964b52a09')
2023-09-27 10:42:44.974 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:133 - Working in the temporary directory /tmp/tmpm9enmhba
2023-09-27 10:42:45.807 | DEBUG    | lean_dojo.data_extraction.lean:clone_and_checkout:441 - Cloning LeanGitRepo(url='https://github.com/JLimperg/aesop', commit='d13a9666e6f430b940ef8d092f1219e964b52a09')
2023-09-27 10:42:48.000 | DEBUG    | lean_dojo.data_extraction.trace:_trace_lean4:97 - Tracing LeanGitRepo(url='https://github.com/JLimperg/aesop', commit='d13a9666e6f430b940ef8d092f1219e964b52a09')
2023-09-27 10:42:48.041 | DEBUG    | lean_dojo.container:run:183 - NUM_PROCS=12 python3 build_lean4_repo.py aesop
2023-09-27 10:42:48.140 | INFO     | __main__:main:121 - Building aesop
/bin/sh: 1: lake: not found
Traceback (most recent call last):
  File "/tmp/tmpm9enmhba/workspace/build_lean4_repo.py", line 165, in <module>
    main()
  File "/tmp/tmpm9enmhba/workspace/build_lean4_repo.py", line 147, in main
    run_cmd("lake build")
  File "/tmp/tmpm9enmhba/workspace/build_lean4_repo.py", line 27, in run_cmd
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake build' returned non-zero exit status 127.
Traceback (most recent call last):
  File "/home/SENSETIME/luzimu/theorm/ReProver/scripts/trace_repos.py", line 33, in <module>
    main()
  File "/home/SENSETIME/luzimu/theorm/ReProver/scripts/trace_repos.py", line 29, in main
    trace(repo)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 162, in trace
    cached_path = get_traced_repo_path(repo)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 134, in get_traced_repo_path
    _trace(repo)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 66, in _trace
    _trace_lean4(repo)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 104, in _trace_lean4
    container.run(
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/container.py", line 193, in run
    execute(cmd, capture_output=capture_output)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/utils.py", line 117, in execute
    raise ex
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/site-packages/lean_dojo/utils.py", line 112, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/home/SENSETIME/luzimu/theorm/ReProver/reproverenv/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'NUM_PROCS=12 python3 build_lean4_repo.py aesop' returned non-zero exit status 1.

[yangky11]

From the logs, it looks like LeanDojo is running outside Docker. Did you set the environment variable CONTAINER?

[yangky11]

If you want to run outside Docker, you'll have to install elan: https://github.com/leanprover/elan

[mnluzimu]

The problems have been solved. Thank you very much!