LeanDojo: ModuleNotFoundError: No module named 'loguru'

Description Hey guys, I tried tracing a theorem from the following repository - lean-dojo-mew, and commit number 12fec4d9f39ac9a41c6c1f058efab3ec41c028af, and I got the following error message:

2023-08-22 16:04:56.513 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-08-22 16:04:56.801 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:131 - Tracing LeanGitRepo(url='https://github.com/rah4927/lean4-example', commit='529eed015655c59d6f44649800e871f50964d216')
Traceback (most recent call last):
  File "build_lean4_repo.py", line 12, in <module>
    from loguru import logger
ModuleNotFoundError: No module named 'loguru'
---------------------------------------------------------------------------
CalledProcessError                        Traceback (most recent call last)
Cell In[50], line 1
----> 1 with Dojo(theorem) as (dojo, init_state):
      2     print(init_state)

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py:283, in Dojo.__enter__(self)
    281 os.chdir(self.origin_dir)
    282 shutil.rmtree(self.tmp_dir)
--> 283 raise ex

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py:203, in Dojo.__enter__(self)
    200 os.chdir(self.tmp_dir)
    202 # Copy and `cd` into the repo.
--> 203 traced_repo_path = get_traced_repo_path(self.repo)
    204 shutil.copytree(
    205     traced_repo_path,
    206     self.repo.name,
    207     ignore=ignore_patterns("*.dep_paths", "*.ast.json", "*.trace.xml"),
    208 )
    209 os.chdir(self.repo.name)

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py:134, in get_traced_repo_path(repo)
    132 with working_directory() as tmp_dir:
    133     logger.debug(f"Working in the temporary directory {tmp_dir}")
--> 134     _trace(repo)
    135     traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name)
    136     traced_repo.save_to_disk()

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py:66, in _trace(repo)
     64 else:
     65     assert repo.uses_lean4
---> 66     _trace_lean4(repo)

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py:104, in _trace_lean4(repo)
     98 container = get_container()
     99 mts = {
    100     Path.cwd() / repo.name: f"/workspace/{repo.name}",
    101     LEAN4_BUILD_SCRIPT_PATH: f"/workspace/{LEAN4_BUILD_SCRIPT_PATH.name}",
    102     LEAN4_DATA_EXTRACTOR_PATH: f"/workspace/{repo.name}/{LEAN4_DATA_EXTRACTOR_PATH.name}",
    103 }
--> 104 container.run(
    105     f"python3 build_lean4_repo.py {repo.name}",
    106     create_mounts(mts),
    107     {"NUM_PROCS": NUM_PROCS},
    108     as_current_user=True,
    109     work_dir="/workspace",
    110 )

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/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 ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/utils.py:116, in execute(cmd, capture_output)
    114         logger.info(ex.stdout.decode())
    115         logger.error(ex.stderr.decode())
--> 116     raise ex
    117 if not capture_output:
    118     return None

File ~/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/utils.py:111, in execute(cmd, capture_output)
    101 """Execute the shell command ``cmd`` and optionally return its output.
    102 
    103 Args:
   (...)
    108     Optional[Tuple[str, str]]: The command's output, including stdout and stderr (None if ``capture_output == False``).
    109 """
    110 try:
--> 111     res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
    112 except subprocess.CalledProcessError as ex:
    113     if capture_output:

File ~/.pyenv/versions/3.9.16/lib/python3.9/subprocess.py:528, in run(input, capture_output, timeout, check, *popenargs, **kwargs)
    526     retcode = process.poll()
    527     if check and retcode:
--> 528         raise CalledProcessError(retcode, process.args,
    529                                  output=stdout, stderr=stderr)
    530 return CompletedProcess(process.args, retcode, stdout, stderr)

CalledProcessError: Command 'NUM_PROCS=32 python3 build_lean4_repo.py lean4-example' returned non-zero exit status 1.

Detailed Steps to Reproduce the Behavior

1. First, I installed the latest lean-dojo package by downloading the git repository and running pip install .
2. All the dependencies are installed (including loguru)
3. Then, I ran the following code in a jupyter notebook

import os
os.environ['CONTAINER'] = 'native'
os.environ['VERBOSE'] = '1'

from lean_dojo import *
os.environ['VERBOSE']
repo = LeanGitRepo("https://github.com/rah4927/lean-dojo-mew/", "12fec4d9f39ac9a41c6c1f058efab3ec41c028af")
theorem = Theorem(repo, "MiniF2F/Example.lean", "amc12a_2019_p21")

with Dojo(theorem) as (dojo, init_state):
    print(init_state)

Logs in Debug Mode

2023-08-22 16:26:36.756 | WARNING  | lean_dojo.interaction.dojo:__init__:172 - Using Lean 4 without a hard timeout may hang indefinitely.
2023-08-22 16:26:36.757 | DEBUG    | lean_dojo.interaction.dojo:__enter__:192 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/rah4927/lean-dojo-mew/', commit='12fec4d9f39ac9a41c6c1f058efab3ec41c028af'), file_path=PosixPath('MiniF2F/Example.lean'), full_name='amc12a_2019_p21')
2023-08-22 16:26:37.048 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:131 - Tracing LeanGitRepo(url='https://github.com/rah4927/lean-dojo-mew/', commit='12fec4d9f39ac9a41c6c1f058efab3ec41c028af')
2023-08-22 16:26:37.049 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:133 - Working in the temporary directory /tmp/tmpcgh6yp06
2023-08-22 16:26:37.434 | DEBUG    | lean_dojo.data_extraction.lean:clone_and_checkout:436 - Cloning LeanGitRepo(url='https://github.com/rah4927/lean-dojo-mew/', commit='12fec4d9f39ac9a41c6c1f058efab3ec41c028af')
2023-08-22 16:26:37.755 | INFO     | lean_dojo.utils:execute:114 - 
2023-08-22 16:26:37.755 | ERROR    | lean_dojo.utils:execute:115 - fatal: Not a git repository (or any parent up to mount point /tmp)
Stopping at filesystem boundary (GIT_DISCOVERY_ACROSS_FILESYSTEM not set).

Traceback (most recent call last):
  File "/lilac/data/peer/rsaha/misc./dojo.py", line 9, in <module>
    with Dojo(theorem) as (dojo, init_state):
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 283, in __enter__
    raise ex
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/interaction/dojo.py", line 203, in __enter__
    traced_repo_path = get_traced_repo_path(self.repo)
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py", line 134, in get_traced_repo_path
    _trace(repo)
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py", line 66, in _trace
    _trace_lean4(repo)
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/trace.py", line 95, in _trace_lean4
    repo.clone_and_checkout()
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/data_extraction/lean.py", line 439, in clone_and_checkout
    execute(
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/utils.py", line 116, in execute
    raise ex
  File "/home/sahar1/.pyenv/versions/lean-dojo-benchmark/lib/python3.9/site-packages/lean_dojo/utils.py", line 111, in execute
    res = subprocess.run(cmd, shell=True, capture_output=capture_output, check=True)
  File "/home/sahar1/.pyenv/versions/3.9.16/lib/python3.9/subprocess.py", line 528, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command 'git checkout 12fec4d9f39ac9a41c6c1f058efab3ec41c028af && git submodule update --recursive' returned non-zero exit status 128.

Platform Information

• System

Architecture:          x86_64
CPU op-mode(s):        32-bit, 64-bit
Byte Order:            Little Endian
CPU(s):                8
On-line CPU(s) list:   0-7
Thread(s) per core:    1
Core(s) per socket:    2
Socket(s):             4
NUMA node(s):          1
Vendor ID:             GenuineIntel
CPU family:            6
Model:                 85
Model name:            Intel(R) Xeon(R) Gold 6242R CPU @ 3.10GHz
Stepping:              7
CPU MHz:               3099.999
BogoMIPS:              6199.99
Hypervisor vendor:     VMware
Virtualization type:   full
L1d cache:             32K
L1i cache:             32K
L2 cache:              1024K
L3 cache:              36608K
NUMA node0 CPU(s):     0-7

• OS:

NAME="CentOS Linux"
VERSION="7 (Core)"
ID="centos"
ID_LIKE="rhel fedora"
VERSION_ID="7"
PRETTY_NAME="CentOS Linux 7 (Core)"
ANSI_COLOR="0;31"
CPE_NAME="cpe:/o:centos:centos:7"
HOME_URL="https://www.centos.org/"
BUG_REPORT_URL="https://bugs.centos.org/"

CENTOS_MANTISBT_PROJECT="CentOS-7"
CENTOS_MANTISBT_PROJECT_VERSION="7"
REDHAT_SUPPORT_PRODUCT="centos"
REDHAT_SUPPORT_PRODUCT_VERSION="7"

• Browser (running the notebook on chrome)
• LeanDojo Version - 1.2.1

Any help is apppreciated, thank you!