Add isolate field for parallel MCP session support

scripts/task.py

@@ -47,6 +47,9 @@ class TaskMetadata:
     # Optional fields - Git integration
     git_commit: bool = False  # Whether to create git commits after each round
 
+    # Optional fields - Parallel execution
+    isolate: bool = False  # Enable MCP session isolation (sets LEAN_PROJECT_PATH)
+
     # Auto-generated fields
     created_at: datetime = field(default_factory=datetime.now)
     task_id: str = field(default="")  # Auto-generated unique ID
@@ -87,15 +90,28 @@ def get_check_path(self) -> Path:
         """Get the path to check for lean files."""
         return self.target_path
 
+    def _find_lean_project_root(self) -> Optional[Path]:
+        """Walk up from target_path to find the Lean project root (contains lean-toolchain)."""
+        search = self.target_path if self.target_path.is_dir() else self.target_path.parent
+        while search != search.parent:
+            if (search / "lean-toolchain").is_file():
+                return search
+            search = search.parent
+        return None
+
     def build_env(self) -> dict:
-        """Build environment variables (including MCP_LOG_DIR and MCP_LOG_NAME)."""
+        """Build environment variables (including MCP_LOG_DIR, MCP_LOG_NAME, LEAN_PROJECT_PATH)."""
         env = os.environ.copy()
         if self.mcp_log_dir:
             # Ensure directory exists
             Path(self.mcp_log_dir).mkdir(parents=True, exist_ok=True)
             env["MCP_LOG_DIR"] = str(self.mcp_log_dir)
         if self.mcp_log_name:
             env["MCP_LOG_NAME"] = self.mcp_log_name
+        if self.isolate:
+            project_root = self._find_lean_project_root()
+            if project_root:
+                env["LEAN_PROJECT_PATH"] = str(project_root)
         return env
 
     def to_dict(self) -> dict:
@@ -119,6 +135,7 @@ def to_dict(self) -> dict:
             "track_statements": self.track_statements,
             "on_statement_change": self.on_statement_change,
             "git_commit": self.git_commit,
+            "isolate": self.isolate,
             "created_at": self.created_at.isoformat(),
         }
 
@@ -150,6 +167,7 @@ def from_dict(cls, data: dict) -> "TaskMetadata":
             track_statements=data.get("track_statements", True),
             on_statement_change=data.get("on_statement_change", "warn"),
             git_commit=data.get("git_commit", False),
+            isolate=data.get("isolate", False),
             created_at=created_at,
             task_id=data.get("task_id", ""),
         )

scripts/test_putnam.yaml

@@ -0,0 +1,24 @@
+# Test config for parallel Putnam proving
+# Run with: python -m scripts.run_claude batch scripts/test_putnam.yaml --parallel --max-workers 2
+
+defaults:
+  task_type: file
+  prompt_file: /mnt/nvme1/zihao/numina/numina-lean-agent/prompts/prompt_complete_file.txt
+  cwd: /mnt/nvme1/zihao/numina
+  check_after_complete: true
+  allow_sorry: false
+  permission_mode: bypassPermissions
+  result_dir: /mnt/nvme1/zihao/numina/numina-lean-agent/results/test_putnam
+  mcp_log_dir: /mnt/nvme1/zihao/numina/numina-lean-agent/mcp_logs
+  track_statements: true
+  on_statement_change: warn
+  isolate: true
+
+tasks:
+  - target_path: /mnt/nvme1/zihao/numina/LiveProveBench/LiveProveBench/PutnamBench2025/putnam_2025_b1.lean
+    max_rounds: 15
+    mcp_log_name: putnam_2025_b1
+
+  - target_path: /mnt/nvme1/zihao/numina/LiveProveBench/LiveProveBench/PutnamBench2025/putnam_2025_a2.lean
+    max_rounds: 15
+    mcp_log_name: putnam_2025_a2