Merge branch 'lean-dojo:main' into main

src/lean_dojo/data_extraction/lean.py

@@ -431,7 +431,10 @@ def get_lean4_version_from_config(toolchain: str) -> str:
     """Return the required Lean version given a ``lean-toolchain`` config."""
     m = _LEAN4_VERSION_REGEX.fullmatch(toolchain.strip())
     assert m is not None, "Invalid config."
-    return m["version"]
+    v = m["version"]
+    if not v.startswith("v") and v[0].isnumeric():
+        v = "v" + v
+    return v
 
 
 def get_lean4_commit_from_config(config_dict: Dict[str, Any]) -> str:
@@ -440,10 +443,7 @@ def get_lean4_commit_from_config(config_dict: Dict[str, Any]) -> str:
     if LEAN4_REPO is None:
         LEAN4_REPO = GITHUB.get_repo("leanprover/lean4")
     assert "content" in config_dict, "config_dict must have a 'content' field"
-    config = config_dict["content"].strip()
-    prefix = "leanprover/lean4:"
-    assert config.startswith(prefix), f"Invalid Lean 4 version: {config}"
-    version = config[len(prefix) :]
+    version = get_lean4_version_from_config(config_dict["content"].strip())
     if version.startswith("nightly-"):
         global LEAN4_NIGHTLY_REPO
         if LEAN4_NIGHTLY_REPO is None:

src/lean_dojo/data_extraction/trace.py

@@ -158,7 +158,6 @@ def _trace(repo: LeanGitRepo, build_deps: bool) -> None:
             cmd = f"lake env lean --threads {NUM_PROCS} --run ExtractData.lean"
             if not build_deps:
                 cmd += " noDeps"
-            logger.debug(cmd)
             execute(cmd, capture_output=True)
 
         check_files(packages_path, not build_deps)

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()

src/lean_dojo/interaction/Lean4Repl.lean

@@ -248,9 +248,9 @@ end TacticRepl
 
 
 private def loop (m : Type → Type) [Monad m] [MonadLift IO m] [MonadError m] (handler : Request → m Response) : m Unit := do
-  while true do
-    let line ← (← IO.getStdin).getLine
-    if line.trim == "exit" then
+ while true do
+    let line := (← (← IO.getStdin).getLine).trim
+    if line == "exit" then
       break
     match (Json.parse line) with
     | .error err => throwError s!"[fatal] failed to parse JSON {err}"

src/lean_dojo/interaction/dojo.py

@@ -392,7 +392,7 @@ def _check_alive(self) -> None:
         if exit_code == 137:
             raise DojoCrashError("OOM")
         else:
-            raise DojoCrashError(f"Unknown exit code: {exit_code}")
+            raise DojoCrashError(f"Unexpected exit code: {exit_code}")
 
     def _read_next_line(self) -> Tuple[str, str]:
         """Read the next line from `self.proc`.

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")