build_lean4_repo.py exit with error

[OctoberFox11]

Description
I'm an amateur and I've spent days starting lean_dojo :(
My error occurs when trying to run lean_dojo with a specific Lean4 repository. The process fails with a CalledProcessError when attempting to execute the lake env lean --threads 4 --run ExtractData.lean command.

Detailed Steps to Reproduce the Behavior

Use the following code to reproduce the error:

import os
from lean_dojo import *
import subprocess

# Set environment variable VERBOSE to 1
os.environ['VERBOSE'] = '1'

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

try:
    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)
except subprocess.CalledProcessError as e:
    print("Command failed with exit status", e.returncode)
    print("Command output:", e.output.decode())
    print("Command stderr:", e.stderr.decode())
    print("Current working directory:", os.getcwd())
except Exception as e:
    print("An unexpected error occurred:", str(e))
    print("Current working directory:", os.getcwd())

3. Observe the error during the execution.

Logs in Debug Mode
Command failed with exit status 1
Command output: [0/1] Building Lean4Example

Command stderr:

2024-06-22 00:05:49.396 | INFO     | __main__:main:165 - Building lean4-example
2024-06-22 00:05:51.908 | INFO     | __main__:main:188 - Tracing lean4-example
2024-06-22 00:05:51.929 | DEBUG    | __main__:main:193 - lake env lean --threads 4 --run ExtractData.lean
  0%|          | 0/721 [00:05<?, ?it/s]Traceback (most recent call last):
  File "/tmp/tmpokt8c1we/workspace/build_lean4_repo.py", line 200, in <module>
    main()
  File "/tmp/tmpokt8c1we/workspace/build_lean4_repo.py", line 194, in main
    run_cmd(cmd, capture_output=True)
  File "/tmp/tmpokt8c1we/workspace/build_lean4_repo.py", line 29, in run_cmd
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/usr/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'lake env lean --threads 4 --run ExtractData.lean' returned non-zero exit status 1.

Platform Information

• Windows WSL
• Python 3.10.12
• Lean 4.6.0-rc1
• Elan 3.1.1
• Lake version 5.0.0-5cc0c3f
• LeanDojo Version 1.8.2

[realharryhero]

I had the same issue, but with lake build, and not lake env lean --threads 4 --run ExtractData.lean. I solved it by making sure all the lean files in the directory did not have any errors in them.

(edit: never mind sorry)

[yangky11]

It's because fd14c4c8b29cc74a082e5ae6f64c2fb25b28e15e is too old, and Lean has made quite a few breaking changes since this commit.

You can simply change it to 7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f. I'll also updating LeanDojo's documentation to reflect this.

[yangky11]

Feel free to re-open if the issue still persists.