a potential bug in container.py

[OakYU]

Description When I was running the lean4 example, I met an error in the function _unmount_files under container.py. The error is "Directory not empty". I tried to print the directory and found there exists .lake. It seems that the mechanism of moving and deleting files belonging to the dst folder in function _unmount_files is somewhere not robust. To solve this issue, I simply modify shutil.rmtree(dst) into shutil.rmtree(dst, ignore_errors=True) in line 144. But I'm not sure whether this solution is safe.

Detailed Steps to Reproduce the Behavior

My code:

from lean_dojo import LeanGitRepo
repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "3f8c5eb303a225cdef609498b8d87262e5ef344b")

from lean_dojo import Theorem, Dojo, ProofFinished
theorem = Theorem(repo, "Lean4Example.lean", "foo")
with Dojo(theorem) as (dojo, init_state):
    print(init_state)
    result = dojo.run_tac(init_state, "rfl")
    assert isinstance(result, ProofFinished)
    print(result)

Logs in Debug Mode You can also see my print here, i.e. dst="/mntnfs/med_data5/yufei/.cache/tmp/tmp62wukmc1/lean4-example/workspace/lean4-example" and os.listdir(dst) -> ['.lake']

2024-06-05 13:06:47.688 | WARNING  | lean_dojo.interaction.dojo:__init__:152 - Using Lean 4 without a hard timeout may hang indefinitely.
2024-06-05 13:06:47.688 | DEBUG    | lean_dojo.interaction.dojo:__enter__:164 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='3f8c5eb303a225cdef609498b8d87262e5ef344b'), file_path=PosixPath('Lean4Example.lean'), full_name='foo')
2024-06-05 13:06:47.692 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:87 - The traced repo is available in the cache.
2024-06-05 13:06:55.182 | DEBUG    | lean_dojo.interaction.dojo:_modify_file:356 - Modifying Lean4Example.lean
2024-06-05 13:06:55.186 | DEBUG    | lean_dojo.interaction.dojo:__enter__:195 - Launching the proof using <class 'lean_dojo.container.NativeContainer'>
2024-06-05 13:07:04.303 | DEBUG    | lean_dojo.container:run:189 - lake build Lean4Repl
2024-06-05 13:07:26.145 | DEBUG    | lean_dojo.container:run_interactive:219 - lake env lean --threads=1 --memory=32768 Lean4Example.lean
2024-06-05 13:07:26.789 | DEBUG    | lean_dojo.interaction.dojo:_read_next_line:530 - REPL> {"tacticState": "a : Nat\n⊢ a + 1 = Nat.succ a", "sid": 0, "error": null}
TacticState(pp='a : Nat\n⊢ a + 1 = Nat.succ a', id=0, message=None)
2024-06-05 13:07:26.790 | DEBUG    | lean_dojo.interaction.dojo:_submit_request:491 - {"sid": 0, "cmd": "rfl"}
2024-06-05 13:07:26.792 | DEBUG    | lean_dojo.interaction.dojo:_read_next_line:530 - REPL> {"tacticState": "no goals", "sid": 1, "error": null}
ProofFinished(tactic_state_id=1, message='')
2024-06-05 13:07:26.792 | DEBUG    | lean_dojo.interaction.dojo:_cleanup:289 - Cleaning up.
2024-06-05 13:07:26.792 | DEBUG    | lean_dojo.interaction.dojo:_cleanup_container:299 - Cleaning up the container.
/mntnfs/med_data5/yufei/.cache/tmp/tmp62wukmc1/lean4-example/workspace/lean4-example
['.lake']
2024-06-05 13:07:36.638 | DEBUG    | lean_dojo.interaction.dojo:_cleanup_tmp_dir:319 - Cleaning up the temporary directory.
Traceback (most recent call last):
  File "/mntnfs/med_data5/yufei/lean/LeanDojo/src/lean_dojo/container.py", line 145, in _unmount_files
    shutil.rmtree(dst)
  File "/mntnfs/med_data5/yufei/anaconda3/envs/lean/lib/python3.9/shutil.py", line 734, in rmtree
    _rmtree_safe_fd(fd, path, onerror)
  File "/mntnfs/med_data5/yufei/anaconda3/envs/lean/lib/python3.9/shutil.py", line 667, in _rmtree_safe_fd
    _rmtree_safe_fd(dirfd, fullname, onerror)
  File "/mntnfs/med_data5/yufei/anaconda3/envs/lean/lib/python3.9/shutil.py", line 667, in _rmtree_safe_fd
    _rmtree_safe_fd(dirfd, fullname, onerror)
  File "/mntnfs/med_data5/yufei/anaconda3/envs/lean/lib/python3.9/shutil.py", line 673, in _rmtree_safe_fd
    onerror(os.rmdir, fullname, sys.exc_info())
  File "/mntnfs/med_data5/yufei/anaconda3/envs/lean/lib/python3.9/shutil.py", line 671, in _rmtree_safe_fd
    os.rmdir(entry.name, dir_fd=topfd)
OSError: [Errno 39] Directory not empty: 'lib'

Platform Information

• OS: linux
• python 3.9.18
• LeanDojo Version 1.9.0
• elan 3.1.1 (71ddc6633 2024-02-22)
• Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

[yangky11]

Sorry for the late response. I'll be able to take a look probably next week.

[yangky11]

Hi,

I ran the code but was unable to reproduce the error. Nevertheless, adding ignore_errors=True should be fine.