diff --git a/scripts/task.py b/scripts/task.py index 19a969e..3d5ffe8 100644 --- a/scripts/task.py +++ b/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,8 +90,17 @@ 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 @@ -96,6 +108,10 @@ def build_env(self) -> dict: 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", ""), ) diff --git a/scripts/test_putnam.yaml b/scripts/test_putnam.yaml new file mode 100644 index 0000000..9d11f69 --- /dev/null +++ b/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