diff --git a/prompts/prompt_complete_file.txt b/prompts/prompt_complete_file.txt index 432f172..4496ed6 100644 --- a/prompts/prompt_complete_file.txt +++ b/prompts/prompt_complete_file.txt @@ -1,9 +1,9 @@ Complete the target Lean theorem file, making it sorry-free and ensuring it compiles without errors. -Use `python skills/cli/diagnostic.py FILE` to verify the file. Errors mean `"has_error": true` or severity `"error"` in the response. +Use `python skills/cli/lean_check.py FILE` to verify the file. Errors mean `"has_error": true` or severity `"error"` in the response. IMPORTANT: -- Verify the file again after each update using `python skills/cli/diagnostic.py`. +- Verify the file again after each update using `python skills/cli/lean_check.py`. - You may add helper lemmas, but do not create new axioms. Tips: @@ -21,4 +21,4 @@ where {reason} is: - LIMIT — if stopped due to limits or there are still sorries/errors - COMPLETE — only if the file is sorry-free AND compiles without errors -IMPORTANT: Use `python skills/cli/diagnostic.py` to verify, do not use `lake build`. +IMPORTANT: Use `python skills/cli/lean_check.py` to verify, do not use `lake build`. diff --git a/scripts/task.py b/scripts/task.py index 29c3d75..7fb158d 100644 --- a/scripts/task.py +++ b/scripts/task.py @@ -69,8 +69,6 @@ def __post_init__(self): self.prompt_file = Path(self.prompt_file).resolve() if self.result_dir: self.result_dir = Path(self.result_dir).resolve() - if self.mcp_log_dir: - self.mcp_log_dir = Path(self.mcp_log_dir).resolve() if self.safe_verify_path: self.safe_verify_path = Path(self.safe_verify_path).resolve() if self.safe_verify_cwd: