From e2f0b7a430821acbb0cd116d8fa42a0af25811f4 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Thu, 8 Oct 2026 03:41:40 +0000 Subject: [PATCH 1/3] Restore recorded settings when resuming runs --- docs/USAGE.md | 12 +- src/evaluator/backends/claude_code.py | 5 +- src/evaluator/runner.py | 154 +++++++++++++- tests/evaluator/test_claude_code_auth.py | 54 +++++ .../test_proof_from_scratch_runner.py | 70 +++++++ tests/evaluator/test_resume_options.py | 196 ++++++++++++++++++ 6 files changed, 485 insertions(+), 6 deletions(-) create mode 100644 tests/evaluator/test_claude_code_auth.py create mode 100644 tests/evaluator/test_resume_options.py diff --git a/docs/USAGE.md b/docs/USAGE.md index 7458ebb8..98570b0d 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -439,9 +439,17 @@ uv run tlaps-bench run --mode proof-completion --backend codex --model gpt-5.5 - The runner skips benchmarks already recorded as `SKIP` or as a genuine `PASS` in that directory (first-attempt or via a continuation round), and reruns the rest. -For PFS, resume must select the same module tasks as the original run. A default run can resume without selection flags only while Current still resolves to the same tasks. To resume an older full-PFS run, supply a task-list file containing its original module IDs. For an explicit task-list run in either mode, pass the same list again. +For PFS runs with a current `run-manifest.json`, only the output directory is needed: -`--dry-run --resume --output-dir DIR` checks the selected cohort against `task-list.json` without starting a run. Full PFS resume also checks `run-manifest.json`: the canonical corpus, execution sources, pinned proof libraries, verification toolchain, execution limits, and persistent-session policy must still match. If the original run used `--session-dir` or the implicit directory from `--keep-container`, retain that session path. Keep the original checkout and inputs when continuing a historical run. +```bash +uv run tlaps-bench run --resume --output-dir results/my-pfs-run +``` + +Omitted options inherit the recorded backend, model, reasoning effort, output-token limit, container/local mode, agent and checker budgets, checker CPU limit, retry and continuation limits, and persistent session directory. Explicit conflicting options are rejected, even when they equal the normal CLI defaults. The exact cohort is restored from `task-list.json`, so changes to the Current collection do not silently change the selected tasks. Explicit selection flags must still select the original cohort. + +Only recorded settings can be recovered. Scheduling and operational options such as `--jobs`, quota thresholds, and `--keep-container` still use their normal defaults unless supplied. Proof Completion runs do not record an execution manifest: their recorded task list can restore the mode and cohort, but backend/model/budget options must be supplied again. Unsupported older PFS manifest schemas require the original checkout. + +`--dry-run --resume --output-dir DIR` checks recorded options and the selected cohort without starting a run. Full PFS resume also checks `run-manifest.json`: the canonical corpus, execution sources, pinned proof libraries, verification toolchain, execution limits, and persistent-session policy must still match. Restoring options does not waive these identity checks. Keep the original checkout and inputs when continuing a historical run. Inline infra retries are intentionally short: the default `--infra-retries 3` gives the original attempt plus three retries with brief backoff. If a longer provider or network outage leaves `INFRA_ERROR` / `QUOTA_EXHAUSTED` results, rerun later with the same `--output-dir --resume`; those non-genuine results are not skipped. diff --git a/src/evaluator/backends/claude_code.py b/src/evaluator/backends/claude_code.py index d7740f0e..49291687 100644 --- a/src/evaluator/backends/claude_code.py +++ b/src/evaluator/backends/claude_code.py @@ -640,18 +640,21 @@ def check_auth(self) -> str | None: return None return "claude_code: Bedrock/Mantle selected but no AWS credentials detected" # Fast path: env var present. - if os.environ.get("ANTHROPIC_API_KEY"): + if not self._needs_claude_credentials(): return None # Slow path: probe the CLI with --no-session-persistence so the # probe doesn't pollute the user's resume history. This makes one # tiny API call but covers OAuth / subscription auth that env-var # checks can't see. + # Keep this credential-only probe cheap without changing the experiment's + # effort or the parent environment (the model preflight checks those). try: r = subprocess.run( ["claude", "--print", "--no-session-persistence", "--output-format", "text", "ok"], capture_output=True, text=True, timeout=30, + env={**os.environ, "CLAUDE_CODE_EFFORT_LEVEL": "low"}, ) if r.returncode == 0: return None diff --git a/src/evaluator/runner.py b/src/evaluator/runner.py index 0dcdf944..a436e08c 100644 --- a/src/evaluator/runner.py +++ b/src/evaluator/runner.py @@ -1760,6 +1760,150 @@ def _write_task_list_record(output_dir: str, mode_name: str, task_ids: list[str] f.write("\n") +def _read_resume_options(output_dir: str) -> tuple[dict[str, object], list[str] | None]: + """Recover only recorded CLI inputs; identity validation still runs afterward.""" + + def read_record(filename): + path = os.path.join(output_dir, filename) + try: + with open(path, encoding="utf-8") as stream: + value = json.load(stream) + except FileNotFoundError: + return None + except (OSError, UnicodeError, json.JSONDecodeError) as exc: + raise ValueError(f"cannot read resume record {path!r}: {exc}") from exc + if type(value) is not dict: + raise ValueError(f"invalid resume record {path!r}: expected an object") + return value + + options = {} + task_ids = None + tasks = read_record(TASK_LIST_RECORD) + if tasks is not None: + task_ids = tasks.get("tasks") + if ( + set(tasks) != {"mode", "tasks"} + or tasks["mode"] not in list_modes() + or type(task_ids) is not list + or not task_ids + or any(type(task_id) is not str or not task_id for task_id in task_ids) + or len(set(task_ids)) != len(task_ids) + ): + raise ValueError(f"invalid recorded task list in {TASK_LIST_RECORD}") + options["mode"] = tasks["mode"] + + manifest = read_record(RUN_MANIFEST_RECORD) + if manifest is None: + return options, task_ids + if type(manifest.get("schema_version")) is not int or manifest["schema_version"] != 5: + raise ValueError(f"unsupported recorded {RUN_MANIFEST_RECORD} schema; keep the original checkout for this run") + if manifest.get("mode") != "proof-from-scratch": + raise ValueError(f"invalid recorded mode in {RUN_MANIFEST_RECORD}") + if options.get("mode", manifest["mode"]) != manifest["mode"]: + raise ValueError("recorded task list and run manifest have different modes") + options["mode"] = manifest["mode"] + policy = manifest.get("execution_policy") + if type(policy) is not dict: + raise ValueError("invalid recorded execution policy") + for name, types in ( + ("backend", (str,)), + ("model", (str, type(None))), + ("reasoning_effort", (str, type(None))), + ("max_output_tokens", (int, type(None))), + ("timeout", (int,)), + ("check_timeout", (int,)), + ("infra_retries", (int,)), + ("max_continuations", (int,)), + ): + if name not in policy or type(policy[name]) not in types: + raise ValueError(f"invalid recorded execution option {name!r}") + value = policy[name] + if type(value) is str and not value: + raise ValueError(f"empty recorded execution option {name!r}") + if type(value) is int and value < (1 if name in {"check_timeout", "max_output_tokens"} else 0): + raise ValueError(f"invalid recorded execution option {name!r}") + options[name] = value + if options["backend"] not in list_backends() or policy.get("environment") not in ("container", "local"): + raise ValueError("invalid recorded backend or execution environment") + options["no_container"] = policy["environment"] == "local" + + session = policy.get("session") + if ( + type(session) is not dict + or type(session.get("persistence")) is not bool + or type(session.get("root")) not in {str, type(None)} + or session["persistence"] != bool(session["root"]) + or (session["root"] is not None and not os.path.isabs(session["root"])) + or session.get("key_scheme") != SESSION_KEY_SCHEME + ): + raise ValueError("invalid recorded session policy") + options["session_dir"] = session["root"] + + verification = policy.get("verification") + if ( + type(verification) is not dict + or verification.get("version") != POLICY_VERSION + or type(verification.get("modules")) is not dict + or not verification["modules"] + ): + raise ValueError("invalid recorded verification policy") + cpus = set() + for value in verification["modules"].values(): + module_policy = VerificationPolicy.from_dict(value) + if module_policy.base_timeout_secs != options["check_timeout"]: + raise ValueError("recorded module budget differs from the execution policy") + cpus.add(module_policy.cpus) + if len(cpus) != 1: + raise ValueError("recorded module CPU limits are inconsistent") + options["check_cpus"] = cpus.pop() + return options, task_ids + + +def _parse_run_args(parser: argparse.ArgumentParser) -> tuple[argparse.Namespace, list[str] | None]: + # A sentinel distinguishes omission from explicitly supplying a default + # value, including --backend codex, --timeout 28800, and --no-container. + names = ( + "mode", + "backend", + "model", + "reasoning_effort", + "max_output_tokens", + "timeout", + "check_timeout", + "check_cpus", + "infra_retries", + "max_continuations", + "no_container", + "session_dir", + ) + omitted = object() + args = parser.parse_args(namespace=argparse.Namespace(**dict.fromkeys(names, omitted))) + recorded_options = {} + recorded_tasks = None + if args.resume: + if not args.output_dir: + parser.error("--resume requires --output-dir") + try: + recorded_options, recorded_tasks = _read_resume_options(args.output_dir) + except ValueError as exc: + parser.error(str(exc)) + for name in names: + value = getattr(args, name) + if value is omitted: + setattr(args, name, recorded_options.get(name, parser.get_default(name))) + elif name in recorded_options and name != "session_dir" and value != recorded_options[name]: + parser.error( + f"cannot resume with different --{name.replace('_', '-')}; recorded value is {recorded_options[name]!r}" + ) + if "session_dir" in recorded_options: + session_dir = _resolve_session_dir(args.session_dir, args.keep_container, not args.no_container) + if session_dir != (recorded_options["session_dir"] or ""): + parser.error("cannot resume with a different persistent session directory") + if args.filter is not None or args.task_list is not None: + recorded_tasks = None + return args, recorded_tasks + + def _update_identity_digest(digest, value: bytes) -> None: digest.update(len(value).to_bytes(8, byteorder="big")) digest.update(value) @@ -4080,7 +4224,7 @@ def main(): parser.add_argument( "--resume", action="store_true", - help="Reuse --output-dir: skip benchmarks already SKIP or genuinely passed there (first-attempt or continuation), run the rest", + help="Reuse --output-dir, inherit recorded settings for omitted options, skip benchmarks already SKIP or genuinely passed there, and run the rest", ) parser.add_argument( "--min-free-gb", @@ -4146,7 +4290,7 @@ def main(): action="store_true", help="Continue when public API pricing is unavailable; equivalent_cost_usd will be blank", ) - args = parser.parse_args() + args, resume_task_ids = _parse_run_args(parser) # Container mode is default; --no-container disables it use_container = not args.no_container @@ -4163,7 +4307,11 @@ def main(): mode = get_mode(args.mode, benchmark_root, checker_binary) task_ids = None try: - if args.filter is not None: + if resume_task_ids is not None: + task_ids = resume_task_ids + benchmark_files = _select_exact_tasks(mode, task_ids) + selection_label = f"recorded cohort from {TASK_LIST_RECORD}" + elif args.filter is not None: if not any(pattern.strip() for pattern in args.filter.split(",")): raise ValueError("--filter requires at least one non-empty pattern") benchmark_files = mode.get_benchmark_files(args.filter) diff --git a/tests/evaluator/test_claude_code_auth.py b/tests/evaluator/test_claude_code_auth.py new file mode 100644 index 00000000..d1a94d88 --- /dev/null +++ b/tests/evaluator/test_claude_code_auth.py @@ -0,0 +1,54 @@ +"""Credential discovery must not inherit expensive experiment effort settings.""" + +import os +import subprocess +from unittest.mock import MagicMock + +import pytest + +from evaluator.backends.claude_code import ClaudeCodeBackend + + +@pytest.fixture(autouse=True) +def direct_claude_credentials(monkeypatch): + for name in ("CLAUDE_CODE_USE_BEDROCK", "CLAUDE_CODE_USE_MANTLE", "ANTHROPIC_API_KEY", "CLAUDE_CODE_OAUTH_TOKEN"): + monkeypatch.delenv(name, raising=False) + + +@pytest.mark.parametrize("name", ["ANTHROPIC_API_KEY", "CLAUDE_CODE_OAUTH_TOKEN"]) +def test_explicit_credentials_skip_host_model_probe(monkeypatch, name): + monkeypatch.setenv(name, "test-credential") + probe = MagicMock() + monkeypatch.setattr(subprocess, "run", probe) + + assert ClaudeCodeBackend().check_auth() is None + probe.assert_not_called() + + +def test_cached_credential_probe_overrides_only_its_own_effort(monkeypatch): + monkeypatch.setenv("CLAUDE_CODE_EFFORT_LEVEL", "xhigh") + probe = MagicMock(return_value=subprocess.CompletedProcess([], 0, "ok", "")) + monkeypatch.setattr(subprocess, "run", probe) + backend = ClaudeCodeBackend() + backend.set_reasoning_effort("max") + + assert backend.check_auth() is None + assert probe.call_args.kwargs["env"]["CLAUDE_CODE_EFFORT_LEVEL"] == "low" + assert probe.call_args.kwargs["timeout"] == 30 + assert "--no-session-persistence" in probe.call_args.args[0] + assert os.environ["CLAUDE_CODE_EFFORT_LEVEL"] == "xhigh" + command = backend.build_command("/workspace", "/results") + assert command[command.index("--effort") + 1] == "max" + + +@pytest.mark.parametrize( + "outcome,expected", + [ + (subprocess.CompletedProcess([], 1, "", "Invalid bearer token"), "auth probe failed"), + (subprocess.TimeoutExpired("claude", 30), "auth probe timed out"), + ], +) +def test_auth_probe_errors_still_fail(monkeypatch, outcome, expected): + probe = MagicMock(**({"side_effect": outcome} if isinstance(outcome, Exception) else {"return_value": outcome})) + monkeypatch.setattr(subprocess, "run", probe) + assert expected in ClaudeCodeBackend().check_auth() diff --git a/tests/evaluator/test_proof_from_scratch_runner.py b/tests/evaluator/test_proof_from_scratch_runner.py index cfdcb4bb..933ff5dc 100644 --- a/tests/evaluator/test_proof_from_scratch_runner.py +++ b/tests/evaluator/test_proof_from_scratch_runner.py @@ -23,6 +23,7 @@ from evaluator import runner from evaluator.backends.agentic import AgenticBackend from evaluator.backends.base import BackendCapabilities, SubmissionDisposition, SubmissionPlan +from evaluator.backends.claude_code import ClaudeCodeBackend from evaluator.modes.proof_from_scratch import ProofFromScratch @@ -610,3 +611,72 @@ def test_container_proof_from_scratch_uses_image_environment(tmp_path, monkeypat assert inspected_images == ["tlaps-bench-base:locked"] assert captured_items[0].container_image == "tlaps-bench-base:locked" assert captured_items[0].canonical_inputs.proof_library_catalog == _catalog().to_bytes() + + +@pytest.mark.parametrize("changed_sources", [False, True]) +def test_resume_restores_policy_through_dispatch_and_retains_source_gate(tmp_path, monkeypatch, changed_sources): + benchmark_root, _suite, task, *_ = _write_fixture(tmp_path) + mode = ProofFromScratch(str(benchmark_root), "/checker") + backend = ClaudeCodeBackend(model="claude-opus-4-8") + backend.set_reasoning_effort("low") + policy = VerificationPolicy.create(1200, mode.module_task_spec(str(task)).proof_unit_ids, 4) + output = tmp_path / "output" + output.mkdir() + identity = runner._proof_from_scratch_run_identity( + mode, + _catalog(), + _toolchain(), + runner._execution_policy_identity( + backend, + use_container=True, + timeout=0, + check_timeout=1200, + infra_retries=5, + max_continuations=2, + session_dir="", + verification_policies={MODULE_TASK_ID: policy.as_dict()}, + ), + runner.AgentSkillsSnapshot.capture(backend, runner.SKILLS_DIR), + ) + if changed_sources: + identity["execution_source_digest"] = "previous-execution-sources" + runner._write_run_manifest(str(output), identity) + runner._write_task_list_record(str(output), mode.name, [MODULE_TASK_ID]) + original_records = {p.name: p.read_bytes() for p in output.iterdir()} + items = [] + model_setup = [] + monkeypatch.setattr(runner, "get_mode", lambda *args, **kwargs: mode) + monkeypatch.setattr(runner, "ensure_image", lambda **kwargs: "test-image") + monkeypatch.setattr(runner, "_container_verification_environment", lambda _: (_catalog(), _toolchain())) + monkeypatch.setattr(runner, "_run_sany_preflight", lambda **kwargs: None) + monkeypatch.setattr(runner, "_confirm_public_pricing", lambda *args, **kwargs: True) + monkeypatch.setattr(ClaudeCodeBackend, "check_auth", lambda self: model_setup.append("auth")) + monkeypatch.setattr(runner, "_run_preflight", lambda *args: model_setup.append("preflight")) + monkeypatch.setattr(runner.quota, "fetch_usage", lambda *args: None) + monkeypatch.setattr(runner, "update_summary", lambda *args: None) + monkeypatch.setattr( + runner, + "run_single_benchmark", + lambda item: items.append(item) or {"benchmark": MODULE_TASK_ID, "check_verdict": "ERROR", "time_secs": 0}, + ) + monkeypatch.setattr(sys, "argv", ["tlaps-bench", "--resume", "--output-dir", str(output)]) + + if changed_sources: + with pytest.raises(SystemExit, match="2"): + runner.main() + assert model_setup == [] + assert items == [] + assert {p.name: p.read_bytes() for p in output.iterdir()} == original_records + else: + runner.main() + assert model_setup == ["auth", "preflight"] + assert len(items) == 1 + item = items[0] + assert item.backend.name == "claude_code" + assert item.backend.model == "claude-opus-4-8" + assert item.backend.reasoning_effort == "low" + assert item.timeout == 0 + assert item.verification_policy == policy + assert item.infra_retries == 5 + assert item.max_continuations == 2 + assert (output / runner.RUN_MANIFEST_RECORD).read_bytes() == original_records[runner.RUN_MANIFEST_RECORD] diff --git a/tests/evaluator/test_resume_options.py b/tests/evaluator/test_resume_options.py new file mode 100644 index 00000000..f97bb4ec --- /dev/null +++ b/tests/evaluator/test_resume_options.py @@ -0,0 +1,196 @@ +"""Resume configuration recovery without model calls or output mutations.""" + +from __future__ import annotations + +import json +import sys +from types import SimpleNamespace +from unittest.mock import MagicMock + +import pytest + +from common.verification_budget import VerificationPolicy +from evaluator import runner + + +@pytest.fixture +def saved_run(tmp_path): + task_id = "Suite/Task.tla" + policy = runner._execution_policy_identity( + SimpleNamespace( + name="claude_code", + approach="agentic", + model="claude-opus-4-8", + reasoning_effort="low", + max_output_tokens=None, + ), + use_container=True, + timeout=0, + check_timeout=1200, + infra_retries=5, + max_continuations=2, + session_dir=str(tmp_path / "sessions"), + verification_policies={task_id: VerificationPolicy.create(1200, ("A", "B"), 4).as_dict()}, + ) + manifest = {"schema_version": 5, "mode": "proof-from-scratch", "execution_policy": policy} + runner._write_run_manifest(str(tmp_path), manifest) + runner._write_task_list_record(str(tmp_path), "proof-from-scratch", [task_id]) + return tmp_path, manifest + + +def _snapshot(path): + return {str(p.relative_to(path)): p.read_bytes() for p in path.rglob("*") if p.is_file()} + + +def _dry_run(monkeypatch, path, *options): + task = str(path / "suite" / "Suite" / "Task.tla") + mode = SimpleNamespace( + name="proof-from-scratch", + benchmark_dir=lambda: str(path / "suite"), + get_benchmark_files=lambda: [task], + ) + monkeypatch.setattr(runner, "get_mode", lambda *args: mode) + setup = MagicMock(side_effect=AssertionError("unexpected backend or toolchain setup")) + for name in ("get_backend", "ensure_image", "resolve_paths", "_run_preflight", "_native_verification_environment"): + monkeypatch.setattr(runner, name, setup) + parsed = [] + original = runner._parse_run_args + + def capture(parser): + result = original(parser) + parsed.append(result) + return result + + monkeypatch.setattr(runner, "_parse_run_args", capture) + monkeypatch.setattr(sys, "argv", ["tlaps-bench run", "--resume", "--output-dir", str(path), "--dry-run", *options]) + runner.main() + setup.assert_not_called() + return parsed[0] + + +def test_omitted_resume_options_and_exact_cohort_are_inherited(saved_run, monkeypatch, capsys): + path, _manifest = saved_run + before = _snapshot(path) + monkeypatch.setattr(runner, "_collection_task_ids", lambda *args: pytest.fail("re-resolved a collection alias")) + + args, tasks = _dry_run(monkeypatch, path) + + assert tasks == ["Suite/Task.tla"] + assert args.backend == "claude_code" + assert args.model == "claude-opus-4-8" + assert args.reasoning_effort == "low" + assert args.timeout == 0 + assert args.check_timeout == 1200 + assert args.check_cpus == 4 + assert args.infra_retries == 5 + assert args.max_continuations == 2 + assert args.session_dir == str(path / "sessions") + assert args.no_container is False + assert args.keep_container is False + assert args.jobs == 1 + assert "recorded cohort" in capsys.readouterr().out + assert _snapshot(path) == before + + +@pytest.mark.parametrize( + "options", + [ + ["--backend", "codex"], + ["--timeout", "28800"], + ["--check-timeout", "600"], + ["--check-cpus", "8"], + ["--max-continuations", "0"], + ["--infra-retries", "3"], + ["--reasoning-effort=high"], + ["--model", "different"], + ["--no-container"], + ["--mode", "proof-completion"], + ["--session-dir", "different"], + ["--max-output-tokens", "100"], + ], +) +def test_explicit_conflicts_including_cli_defaults_reject_without_mutation(saved_run, monkeypatch, capsys, options): + path, _manifest = saved_run + before = _snapshot(path) + with pytest.raises(SystemExit) as exc: + _dry_run(monkeypatch, path, *options) + assert exc.value.code == 2 + assert "cannot resume with" in capsys.readouterr().err + assert _snapshot(path) == before + + +def test_explicit_matching_options_and_equivalent_session_path_are_accepted(saved_run, monkeypatch): + path, _manifest = saved_run + args, _tasks = _dry_run( + monkeypatch, + path, + "--backend", + "claude_code", + "--timeout", + "0", + "--keep-container", + "--session-dir", + str(path / "sessions" / ".." / "sessions"), + ) + assert args.timeout == 0 + assert args.keep_container is True + + +@pytest.mark.parametrize( + "field,value", + [ + ("backend", "unknown"), + ("timeout", True), + ("check_timeout", 0), + ("max_output_tokens", -1), + ("environment", []), + ("session", []), + ("verification", {}), + ], +) +def test_invalid_saved_options_fail_before_setup(saved_run, monkeypatch, capsys, field, value): + path, manifest = saved_run + manifest["execution_policy"][field] = value + runner._write_run_manifest(str(path), manifest) + before = _snapshot(path) + with pytest.raises(SystemExit) as exc: + _dry_run(monkeypatch, path) + assert exc.value.code == 2 + assert "invalid recorded" in capsys.readouterr().err + assert _snapshot(path) == before + + +def test_old_manifest_is_not_upgraded_silently(saved_run, monkeypatch, capsys): + path, manifest = saved_run + manifest["schema_version"] = 4 + runner._write_run_manifest(str(path), manifest) + with pytest.raises(SystemExit) as exc: + _dry_run(monkeypatch, path) + assert exc.value.code == 2 + assert "unsupported recorded run-manifest.json schema" in capsys.readouterr().err + + +def test_task_list_only_recovers_only_what_was_recorded(tmp_path): + runner._write_task_list_record(str(tmp_path), "proof-completion", ["Suite/A.tla"]) + assert runner._read_resume_options(str(tmp_path)) == ({"mode": "proof-completion"}, ["Suite/A.tla"]) + + +def test_no_records_leave_existing_defaults_available(tmp_path): + assert runner._read_resume_options(str(tmp_path)) == ({}, None) + + +def test_resume_requires_explicit_output_directory(monkeypatch, capsys): + monkeypatch.setattr(sys, "argv", ["tlaps-bench run", "--resume"]) + with pytest.raises(SystemExit) as exc: + runner.main() + assert exc.value.code == 2 + assert "--resume requires --output-dir" in capsys.readouterr().err + + +def test_nonobject_records_fail_cleanly(saved_run, monkeypatch, capsys): + path, _manifest = saved_run + (path / runner.RUN_MANIFEST_RECORD).write_text(json.dumps([])) + with pytest.raises(SystemExit) as exc: + _dry_run(monkeypatch, path) + assert exc.value.code == 2 + assert "expected an object" in capsys.readouterr().err From b04e5fbb197190442304da796b3f0f6685be2cbd Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Thu, 8 Oct 2026 04:04:58 +0000 Subject: [PATCH 2/3] Align resume fixtures with recorded configuration --- tests/evaluator/test_problem_sets.py | 6 +++++- tests/evaluator/test_proof_module_checkpoint.py | 14 ++++++++++++-- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/tests/evaluator/test_problem_sets.py b/tests/evaluator/test_problem_sets.py index 6a6066b2..48003d1b 100644 --- a/tests/evaluator/test_problem_sets.py +++ b/tests/evaluator/test_problem_sets.py @@ -179,11 +179,15 @@ def test_default_selection_is_recorded_and_compared_on_resume(pfs_mode, preview_ runner._write_task_list_record(str(tmp_path), "proof-from-scratch", list(CURRENT)) arguments = ["run", "--resume", "--output-dir", str(tmp_path), "--dry-run"] assert cli.main(arguments) == 0 + assert set(_selected(capsys.readouterr().out)) == set(CURRENT) # An old full-suite run must not silently resume as Current. old = list(CURRENT) + ["Walgit/WalgitProof.tla"] runner._write_task_list_record(str(tmp_path), "proof-from-scratch", old) + assert cli.main(arguments) == 0 + assert set(_selected(capsys.readouterr().out)) == set(old) + # Explicitly requesting Current must still reject a changed cohort. with pytest.raises(SystemExit) as exc: - cli.main(arguments) + cli.main([*arguments, "--task-list", "current"]) assert exc.value.code == 2 assert "different task list or mode" in capsys.readouterr().err assert json.loads((tmp_path / runner.TASK_LIST_RECORD).read_text())["tasks"] == sorted(old) diff --git a/tests/evaluator/test_proof_module_checkpoint.py b/tests/evaluator/test_proof_module_checkpoint.py index 4d838a43..3bace92b 100644 --- a/tests/evaluator/test_proof_module_checkpoint.py +++ b/tests/evaluator/test_proof_module_checkpoint.py @@ -407,12 +407,23 @@ def test_runner_resume_work_item_carries_checkpoint_identity_and_submission(tmp_ output_dir.mkdir() (tmp_path / "lib" / "tlapm").mkdir(parents=True) + backend = _ModuleBackend() run_identity = { - "schema_version": 2, + "schema_version": 5, "mode": "proof-from-scratch", "corpus_digest": "corpus", "proof_library_digest": "libraries", "verification_toolchain_digest": "toolchain", + "execution_policy": runner._execution_policy_identity( + backend, + use_container=False, + timeout=28800, + check_timeout=600, + infra_retries=3, + max_continuations=0, + session_dir="", + verification_policies={TASK_ID: runner.VerificationPolicy.create(600, (UNIT_ID,)).as_dict()}, + ), } canonical_inputs = runner.CanonicalInputs.capture(str(task), task.name, []) identity = ModuleCheckpointIdentity( @@ -431,7 +442,6 @@ def test_runner_resume_work_item_carries_checkpoint_identity_and_submission(tmp_ (output_dir / "task-list.json").write_text(json.dumps({"mode": "proof-from-scratch", "tasks": [TASK_ID]})) (output_dir / "results.json").write_text(json.dumps([{"benchmark": TASK_ID, "check_verdict": "FAIL"}])) - backend = _ModuleBackend() mode = _ModuleMode(benchmark_root, task) captured: list[runner.WorkItem] = [] monkeypatch.setattr(runner, "get_backend", lambda *_args, **_kwargs: backend) From bcb0ff964f082430822d8912ea46b1e40910c344 Mon Sep 17 00:00:00 2001 From: Qian-Cheng-nju Date: Thu, 8 Oct 2026 05:31:12 +0000 Subject: [PATCH 3/3] Simplify resume usage guidance --- docs/USAGE.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 98570b0d..ffa0c2b4 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -439,17 +439,15 @@ uv run tlaps-bench run --mode proof-completion --backend codex --model gpt-5.5 - The runner skips benchmarks already recorded as `SKIP` or as a genuine `PASS` in that directory (first-attempt or via a continuation round), and reruns the rest. -For PFS runs with a current `run-manifest.json`, only the output directory is needed: +For PFS, resume with the saved configuration and task list: ```bash uv run tlaps-bench run --resume --output-dir results/my-pfs-run ``` -Omitted options inherit the recorded backend, model, reasoning effort, output-token limit, container/local mode, agent and checker budgets, checker CPU limit, retry and continuation limits, and persistent session directory. Explicit conflicting options are rejected, even when they equal the normal CLI defaults. The exact cohort is restored from `task-list.json`, so changes to the Current collection do not silently change the selected tasks. Explicit selection flags must still select the original cohort. +Conflicting options are rejected. Reapply `--jobs`, quota limits, and `--keep-container` if needed. For Proof Completion, repeat the original run options. -Only recorded settings can be recovered. Scheduling and operational options such as `--jobs`, quota thresholds, and `--keep-container` still use their normal defaults unless supplied. Proof Completion runs do not record an execution manifest: their recorded task list can restore the mode and cohort, but backend/model/budget options must be supplied again. Unsupported older PFS manifest schemas require the original checkout. - -`--dry-run --resume --output-dir DIR` checks recorded options and the selected cohort without starting a run. Full PFS resume also checks `run-manifest.json`: the canonical corpus, execution sources, pinned proof libraries, verification toolchain, execution limits, and persistent-session policy must still match. Restoring options does not waive these identity checks. Keep the original checkout and inputs when continuing a historical run. +Use `--dry-run --resume --output-dir DIR` to preview the selection. Keep the original checkout and inputs when resuming. Inline infra retries are intentionally short: the default `--infra-retries 3` gives the original attempt plus three retries with brief backoff. If a longer provider or network outage leaves `INFRA_ERROR` / `QUOTA_EXHAUSTED` results, rerun later with the same `--output-dir --resume`; those non-genuine results are not skipped.