fix LakeMain.lean

lean-dojo · Oct 6, 2024 · ab13370 · ab13370
1 parent fed54c2
commit ab13370
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git 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
@@ -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")