subprocess.CalledProcessError When I use leandojo to trace a custom lean repo.

[wclsn]

Description

What happened?

When I use leandojo(1.6.0) to trace my toy lean repo(only one basic.lean file) I have encountered below issue:

Traceback (most recent call last): File "/tmp/tmpfibkpeye/workspace/build_lean4_repo.py", line 198, in main() File "/tmp/tmpfibkpeye/workspace/build_lean4_repo.py", line 192, in main run_cmd(cmd, capture_output=True) File "/tmp/tmpfibkpeye/workspace/build_lean4_repo.py", line 28, in run_cmd res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/subprocess.py", line 526, in run raise CalledProcessError(retcode, process.args,

subprocess.CalledProcessError: Command 'lake env lean --threads 24 --run ExtractData.lean' returned non-zero exit status 1. Traceback (most recent call last):

File "/home/v-shaonanwu/lean4math/ast_demo/./trace.py", line 5, in lean_dojo.trace(repo, dst_dir="traced_demo") File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 192, in trace cached_path = get_traced_repo_path(repo, build_deps) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 159, in get_traced_repo_path _trace(repo, build_deps) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 67, in _trace _trace_lean4(repo, build_deps) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 134, in _trace_lean4 raise ex File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 122, in _trace_lean4 container.run( File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/container.py", line 193, in run execute(cmd, capture_output=capture_output) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/utils.py", line 116, in execute raise ex File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/site-packages/lean_dojo/utils.py", line 111, in execute res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True) File "/home/v-shaonanwu/miniforge3/envs/lean4/lib/python3.10/subprocess.py", line 526, in run raise CalledProcessError(retcode, process.args,

subprocess.CalledProcessError: Command 'NUM_PROCS=24 python3 build_lean4_repo.py lean_case_study' returned non-zero exit status 1

Detailed Steps to Reproduce the Behavior

leandojo version 1.6.0 leantoolchain : 4.6.0 rc1 python version 3.10.13

code block:

import lean_dojo from lean_dojo import LeanGitRepo

repo = LeanGitRepo("https://github.com/wclsn/lean_case_study", "3b795a67fb399df3662bd36ddb42b370aa1b3589") lean_dojo.trace(repo, dst_dir="traced_demo")

Platform Information

• OS: Ubuntu 20.04
• LeanDojo Version 1.6.0 and I tried 1.5.1 but it still does not work.

[wclsn]

I partly solve this question by degrading my project's Lean version to v4.3.0 rc2

[yangky11]

Could you please try the most recent version (v1.7.0) and see if the problem still persists? It works fine on my laptop.

[wclsn]

Could you please try the most recent version (v1.7.0) and see if the problem still persists? It works fine on my laptop.

Yes, I have tried the most recent version, and it did work. Thank you for your reply.