Skip to content

Fix dead TaskMetadata.mcp_log_dir ref and outdated CLI name in prompt #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
dgjszy wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Fix dead TaskMetadata.mcp_log_dir ref and outdated CLI name in prompt #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
59e4682
Remove stale mcp_log_dir reference in TaskMetadata.__post_init__
dgjszy May 27, 2026
bc093a4
Fix outdated CLI script name in prompt_complete_file.txt
dgjszy May 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions prompts/prompt_complete_file.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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`.
2 changes: 0 additions & 2 deletions scripts/task.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down