minor fix

src/lean_dojo/data_extraction/ExtractData.lean

@@ -359,8 +359,7 @@ private def visitTermInfo (ti : TermInfo) (env : Environment) : TraceM Unit := d
     }
 
 
-private def visitInfo (ctx : ContextInfo)
-(i : Info) (parent : InfoTree) (env : Environment) : TraceM Unit := do
+private def visitInfo (ctx : ContextInfo) (i : Info) (parent : InfoTree) (env : Environment) : TraceM Unit := do
   match i with
   | .ofTacticInfo ti => visitTacticInfo ctx ti parent
   | .ofTermInfo ti => visitTermInfo ti env
@@ -502,10 +501,8 @@ def processAllFiles (noDeps : Bool) : IO Unit := do
     for path in ← System.FilePath.walkDir cwd do
       if ← shouldProcess path noDeps then
         println! path
-        let mut args := #["env", "lean", "--run", "ExtractData.lean"]
-        args := args.push path.toString
         let t ← IO.asTask $ IO.Process.run
-          {cmd := "lake", args := args}
+          {cmd := "lake", args := #["env", "lean", "--run", "ExtractData.lean", path.toString]}
         tasks := tasks.push (t, path)
 
     for (t, path) in tasks do

src/lean_dojo/data_extraction/build_lean4_repo.py

@@ -129,9 +129,6 @@ def check_files(packages_path: str, no_deps: bool) -> None:
     missing_deps = {p.with_suffix(".dep_paths") for p in oleans - deps}
     if len(missing_jsons) > 0 or len(missing_deps) > 0:
         for p in missing_jsons.union(missing_deps):
-            import pdb
-
-            pdb.set_trace()
             logger.warning(f"Missing {p}")
 
 
@@ -157,7 +154,6 @@ def is_new_version(v: str) -> bool:
 def main() -> None:
     parser = argparse.ArgumentParser()
     parser.add_argument("repo_name")
-    parser.add_argument("--low-memory-mode", action="store_true")
     parser.add_argument("--no-deps", action="store_true")
     args = parser.parse_args()
 
@@ -192,8 +188,6 @@ def main() -> None:
     logger.info(f"Tracing {repo_name}")
     with launch_progressbar(dirs_to_monitor):
         cmd = f"lake env lean --threads {num_procs} --run ExtractData.lean"
-        if args.low_memory_mode:
-            cmd += " noPremises"
         if args.no_deps:
             cmd += " noDeps"
         logger.debug(cmd)

src/lean_dojo/data_extraction/cache.py

@@ -36,8 +36,7 @@ def _split_git_url(url: str) -> Tuple[str, str]:
 
 def _format_dirname(url: str, commit: str) -> str:
     user_name, repo_name = _split_git_url(url)
-    dirname = f"{user_name}-{repo_name}-{commit}"
-    return dirname
+    return f"{user_name}-{repo_name}-{commit}"
 
 
 _CACHE_CORRPUTION_MSG = "The cache may have been corrputed!"