Fix test-lean failure when LEAN project directory exists but is incomplete (#629)

Author: Copilot

CHANGELOG.md

@@ -1,5 +1,11 @@
 ## [Unreleased]
 
+### Bugfixes
+
+* Fix `test-lean` failure when LEAN project directory exists but is incomplete
+
+## v25.12.1
+
 ### Enhancements
 
 * Integrate `libcurl` for HTTP requests, replacing external `curl`/`wget` tools

src/form/lean.cpp

@@ -367,6 +367,12 @@ bool LeanFormula::initializeLeanProject() {
     return true;
   }
 
+  // If directory exists but lakefile doesn't, clean up incomplete initialization
+  if (isDir(projectDir)) {
+    Log::get().info("Removing incomplete LEAN project at " + projectDir);
+    rmDirRecursive(projectDir);
+  }
+
   Log::get().info("Initializing LEAN project at " + projectDir);
 
   // Use lake to create a new Lean project with Mathlib dependency