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

shubhramishra07 commented 8 months ago

Description I tried setting up LeanDojo (and running the demo-lean4.ipynb file) in vscode, and ran into the error in the header. I also tried running it in Jupyter Notebook, and got the same error. Is there an installation I'm missing?

Detailed Steps to Reproduce the Behavior I ran the following commands: conda create -n "lean4test" python=3.10 conda activate lean4test jupyter notebook I set the GitHub Access Token locally within the notebook, and then ran the cells. I ran into an issue in the first cell under the "Interact through Tactics" section. The line causing the error: dojo, state_0 = Dojo(theorem).enter()

Logs in Debug Mode

`023-12-04 21:30:48.768 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-12-04 21:32:06.550 | INFO     | lean_dojo.utils:execute:115 - 
2023-12-04 21:32:06.553 | ERROR    | lean_dojo.utils:execute:116 - error: unknown target `Lean4Repl`

---------------------------------------------------------------------------
CalledProcessError                        Traceback (most recent call last)
Cell In[28], line 5
      2 theorem = Theorem(repo, "Mathlib/LinearAlgebra/Basic.lean", "pi_eq_sum_univ")
      4 # For some theorems, it might take a few minutes.
----> 5 dojo, state_0 = Dojo(theorem).__enter__()

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py:293, in Dojo.__enter__(self)
    291 os.chdir(self.origin_dir)
    292 shutil.rmtree(self.tmp_dir)
--> 293 raise ex

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py:237, in Dojo.__enter__(self)
    235     cmd = f"./build/release/stage1/bin/lean {self.file_path}"
    236 else:
--> 237     self.container.run(
    238         "lake build Lean4Repl",
    239         mts,
    240         as_current_user=True,
    241         capture_output=True,
    242         work_dir=f"/workspace/{self.repo.name}",
    243         cpu_limit=None,
    244         memory_limit=None,
    245         envs={},
    246     )
    247     cmd = f"lake env lean {self.file_path}"
    249 self.proc = self.container.run_interactive(
    250     cmd,
    251     mts,
   (...)
    256     envs={},
    257 )

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/container.py:193, in NativeContainer.run(self, command, mounts, envs, as_current_user, capture_output, cpu_limit, memory_limit, work_dir)
    190         work_dir = Path.cwd() / work_dir.relative_to(work_dir.root)
    192 with working_directory(work_dir):
--> 193     execute(cmd, capture_output=capture_output)
    195 self._unmount_files(mounts)

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/utils.py:117, in execute(cmd, capture_output)
    115         logger.info(ex.stdout.decode())
    116         logger.error(ex.stderr.decode())
--> 117     raise ex
    118 if not capture_output:
    119     return None

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/site-packages/lean_dojo/utils.py:112, in execute(cmd, capture_output)
    102 """Execute the shell command ``cmd`` and optionally return its output.
    103 
    104 Args:
   (...)
    109     Optional[Tuple[str, str]]: The command's output, including stdout and stderr (None if ``capture_output == False``).
    110 """
    111 try:
--> 112     res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
    113 except subprocess.CalledProcessError as ex:
    114     if capture_output:

File /Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/subprocess.py:524, in run(input, capture_output, timeout, check, *popenargs, **kwargs)
    522     retcode = process.poll()
    523     if check and retcode:
--> 524         raise CalledProcessError(retcode, process.args,
    525                                  output=stdout, stderr=stderr)
    526 return CompletedProcess(process.args, retcode, stdout, stderr)

CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1.`

Platform Information

OS: macOS
Browser Safari
LeanDojo Version 1.4.0

shubhramishra07 commented 8 months ago

I also tried it with LeanDojo versions 1.2.6, 1.3.0, and 1.4.2. Let me know if some other version might be better for this. Thank you!