Skip to content

Commit

Permalink
minor edits to get_traced_repo_path
Browse files Browse the repository at this point in the history
  • Loading branch information
yangky11 committed Aug 5, 2024
1 parent 515d361 commit 897c6f1
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/lean_dojo/data_extraction/trace.py
Original file line number Diff line number Diff line change
Expand Up @@ -204,16 +204,16 @@ def get_traced_repo_path(repo: LeanGitRepo, build_deps: bool = True) -> Path:
Returns:
Path: The path of the traced repo in the cache, e.g. :file:`/home/kaiyu/.cache/lean_dojo/leanprover-community-mathlib-2196ab363eb097c008d4497125e0dde23fb36db2`
"""
path = cache.get(repo.format_dirname / repo.name)
rel_cache_dir = repo.format_dirname / repo.name
path = cache.get(rel_cache_dir)
if path is None:
logger.info(f"Tracing {repo}")
with working_directory() as tmp_dir:
logger.debug(f"Working in the temporary directory {tmp_dir}")
_trace(repo, build_deps)
traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name, build_deps)
traced_repo.save_to_disk()
src_dir = tmp_dir / repo.name
rel_cache_dir = Path(repo.format_dirname) / repo.name
traced_repo = TracedRepo.from_traced_files(src_dir, build_deps)
traced_repo.save_to_disk()
path = cache.store(src_dir, rel_cache_dir)
else:
logger.debug("The traced repo is available in the cache.")
Expand Down

0 comments on commit 897c6f1

Please sign in to comment.