From ab133703ebf2da9a6d7e49a2c5a68c0e5793dffe Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Sun, 6 Oct 2024 20:46:57 +0000 Subject: [PATCH] fix LakeMain.lean --- src/lean_dojo/data_extraction/traced_data.py | 4 ---- src/lean_dojo/utils.py | 2 ++ 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/lean_dojo/data_extraction/traced_data.py b/src/lean_dojo/data_extraction/traced_data.py index c7fa9b5..380f00e 100644 --- a/src/lean_dojo/data_extraction/traced_data.py +++ b/src/lean_dojo/data_extraction/traced_data.py @@ -546,10 +546,6 @@ def _from_lean4_traced_file( data["module_paths"] = [] deps_path = json_path.with_suffix("").with_suffix("").with_suffix(".dep_paths") - if not deps_path.exists(): - import pdb - - pdb.set_trace() for line in deps_path.open(): line = line.strip() diff --git a/src/lean_dojo/utils.py b/src/lean_dojo/utils.py index 57f6240..87723a9 100644 --- a/src/lean_dojo/utils.py +++ b/src/lean_dojo/utils.py @@ -272,6 +272,8 @@ def to_lean_path(root_dir: Path, path: Path) -> Path: assert root_dir.name != "lean4" if path == LEAN4_PACKAGES_DIR / "lean4/lib/lean/Lake.lean": return LEAN4_PACKAGES_DIR / "lean4/src/lean/lake/Lake.lean" + elif path == LEAN4_PACKAGES_DIR / "lean4/lib/lean/LakeMain.lean": + return LEAN4_PACKAGES_DIR / "lean4/src/lean/lake/LakeMain.lean" elif path.is_relative_to(LEAN4_PACKAGES_DIR / "lean4/lib/lean/Lake"): # E.g., "lake-packages/lean4/lib/lean/Lake/Util/List.lean" p = path.relative_to(LEAN4_PACKAGES_DIR / "lean4/lib/lean/Lake")