diff --git a/codeframe/cli/pr_commands.py b/codeframe/cli/pr_commands.py index 41a72d55..aa6c9610 100644 --- a/codeframe/cli/pr_commands.py +++ b/codeframe/cli/pr_commands.py @@ -463,6 +463,22 @@ def _check_merge_gate( console.print(f"[red]PROOF9 gate check failed:[/red] {e} — merge blocked") raise typer.Exit(1) if not blocking_reqs: + # Consistent with `cf proof run` (#1118): say so when the ledger is + # empty, rather than letting silence read as "PROOF9 verified this". + # The merge is still allowed — blocking every merge in a workspace with + # no requirements would be a far larger change than this issue asks for, + # and #731's gate is about *open* requirements. + try: + from codeframe.core.proof import ledger as _ledger + + if not _ledger.list_requirements(workspace): + console.print( + "[yellow]PROOF9:[/yellow] the ledger is empty — this merge " + "was not verified against any requirement." + ) + except Exception: + # Reporting only; never let it affect the merge decision. + pass return None if not override: diff --git a/codeframe/cli/proof_commands.py b/codeframe/cli/proof_commands.py index 092657ac..71a98fdb 100644 --- a/codeframe/cli/proof_commands.py +++ b/codeframe/cli/proof_commands.py @@ -135,12 +135,25 @@ def run( gate: Optional[str] = typer.Option( None, "--gate", help="Run only this gate (e.g., unit, e2e)", ), + allow_empty: bool = typer.Option( + False, + "--allow-empty", + help=( + "Exit 0 when there are no applicable obligations. Off by default: " + "a run that verified nothing is not a pass (#1118)." + ), + ), ) -> None: """Run proof obligations for current changes. Determines which requirements apply to changed files, runs their obligations, and collects evidence. + Exit codes: + 0 obligations ran and none failed + 1 an obligation failed + 2 nothing was verified — no applicable obligations (see --allow-empty) + Example: codeframe proof run codeframe proof run --full @@ -172,8 +185,112 @@ def run( results = run_proof(workspace, full=full, gate_filter=gate_filter) if not results: - console.print("[green]No applicable obligations found.[/green]") - return + # `run_proof` returning {} has three causes and they need different + # answers. Two review rounds went by patching one branch at a time and + # getting the reason wrong each time, so this asks the runner's own + # selector instead of inferring it from the mode: + # + # ledger empty -> nothing to verify at all (the #1118 case) + # nothing runnable -> requirements exist but all SATISFIED/WAIVED + # for this mode; scope was never consulted, + # because run_proof short-circuits first + # nothing in scope -> runnable requirements existed and the scope + # filter excluded every one + from codeframe.core.proof import ledger as _ledger + from codeframe.core.proof.models import ReqStatus + from codeframe.core.proof.runner import _requirements_for_run + + try: + all_reqs = _ledger.list_requirements(workspace) + # Same selector the runner uses, so this cannot drift from it. + runnable = _requirements_for_run(workspace, full=full) + except Exception: + # A ledger we cannot read is not evidence of an empty one; fall + # through to the unverified case rather than inventing a reason. + all_reqs, runnable = [], [] + + if runnable: + # Four review rounds went by asserting a specific reason here and + # being wrong each time. The CLI genuinely cannot tell them apart: + # run_proof returns only results, and discards the scope_skipped + # list it computes internally (runner.py:334/435). With a non-empty + # runnable set an empty result can mean the scope filter excluded + # everything, --gate excluded every obligation, enabled_gates config + # did, or a requirement simply has none. + # + # So state what is known and list the candidates, rather than + # asserting one and sending the user somewhere useless. #1138 tracks + # having the runner report the reason so this can be precise. + console.print( + f"[yellow]Nothing was verified.[/yellow] " + f"{len(runnable)} requirement(s) were eligible for this run, " + f"but no obligations ran." + ) + reasons = [] + if not full: + # --full provably ignores scope (runner.py:339), so listing it + # there would put an impossible cause in the candidate list. + reasons.append("none of them cover the changed files") + if gate_filter is not None: + reasons.append(f"--gate {gate_filter.value} excluded their obligations") + reasons.append("their obligations are disabled in proof_config.json") + reasons.append("they have no obligations defined") + console.print("Possible reasons: " + "; ".join(reasons) + ".") + if not full: + console.print( + "Try [bold]cf proof run --full[/bold] to ignore scope, or " + "[bold]cf proof status[/bold] for the ledger." + ) + else: + console.print("See [bold]cf proof status[/bold] for the ledger.") + return + + if all_reqs: + # This one IS knowable: the runnable set is empty while the ledger + # is not, so every requirement was excluded by its status. WAIVED is + # excluded from both modes; SATISFIED only from a scoped run. + satisfied = sum(1 for r in all_reqs if r.status == ReqStatus.SATISFIED) + waived = sum(1 for r in all_reqs if r.status == ReqStatus.WAIVED) + detail = ", ".join( + part + for part in ( + f"{satisfied} satisfied" if satisfied else "", + f"{waived} waived" if waived else "", + ) + if part + ) + console.print( + f"[yellow]Nothing was verified.[/yellow] " + f"{len(all_reqs)} requirement(s) exist, but none are runnable" + + (f" ({detail})." if detail else ".") + ) + console.print( + "A waiver is an accepted risk that no run re-checks; " + "[bold]cf proof run --full[/bold] also re-verifies satisfied " + "ones. See [bold]cf proof status[/bold] for the ledger." + ) + return + + # An empty ledger is not a pass (#1118). Exiting 0 here is what let the + # quickstart's PROVE step read as "PROOF9 gates passed" when nothing had + # been checked — and every new workspace is in exactly this state. + # + # Exit 2 rather than 1: this is not a failure either, and a script needs + # to tell "the gate failed" from "the gate had nothing to check". CI + # treats any non-zero as a stop, which is the point. + console.print("[yellow]Nothing was verified.[/yellow]") + console.print( + "There are no proof obligations in this workspace, so this run " + "checked nothing — it is not a pass." + ) + console.print( + "\nCapture your first requirement with:\n" + " [bold]cf proof capture[/bold]" + ) + if allow_empty: + console.print("\n[dim]--allow-empty: exiting 0 anyway.[/dim]") + return + raise typer.Exit(2) # Display results table = Table(title="Proof Results") @@ -427,7 +544,13 @@ def status_cmd( reqs = ledger.list_requirements(workspace) if not reqs: - console.print("No proof requirements. Use 'cf proof capture' to add one.") + # Same framing as `cf proof run` (#1118): an empty ledger means nothing + # is being verified, which is a state to act on, not a clean bill. + console.print( + "[yellow]No proof requirements — nothing in this workspace is " + "being verified.[/yellow]" + ) + console.print("Capture your first one with: [bold]cf proof capture[/bold]") return counts = {"open": 0, "satisfied": 0, "waived": 0} diff --git a/docs/QUICKSTART.md b/docs/QUICKSTART.md index 67559f96..d35dc936 100644 --- a/docs/QUICKSTART.md +++ b/docs/QUICKSTART.md @@ -240,8 +240,12 @@ Then run the PROOF9 quality gates: codeframe proof run ``` -> On a brand-new workspace this reports `No applicable obligations found` and -> exits 0 — there is nothing to verify yet, which is **not** the same as passing. +> On a brand-new workspace this reports that **nothing was verified** and exits +> **2** — there is nothing to check yet, which is not the same as passing, so it +> is not reported as one (#1118). Exit codes: `0` obligations ran and none +> failed, `1` an obligation failed, `2` nothing was verified. Pass +> `--allow-empty` to exit 0 on an empty ledger where that is expected. +> > Obligations accumulate as you capture glitches with `codeframe proof capture`; > each one becomes a permanent check. See `codeframe proof status` for the ledger. diff --git a/tests/cli/test_proof_commands.py b/tests/cli/test_proof_commands.py index 44ba89d8..5d57d257 100644 --- a/tests/cli/test_proof_commands.py +++ b/tests/cli/test_proof_commands.py @@ -247,12 +247,25 @@ def _outcome(_ws, gate, _rules=()): assert result.exit_code == 1, result.output assert "FAIL" in result.output - def test_run_no_requirements_exits_zero(self, ws): - """run on an empty workspace should exit 0 and say no obligations.""" + def test_run_no_requirements_does_not_exit_zero(self, ws): + """run on an empty workspace reports that nothing was verified (#1118). + + This asserted exit 0 and "No applicable obligations found", which is the + vacuous pass #1118 removes: a green exit on an empty ledger reads as + "PROOF9 gates passed" when nothing was checked. Exit 2 is distinct from + both pass (0) and failure (1); --allow-empty opts back into 0. + """ _, workspace_path = ws result = runner.invoke(app, ["proof", "run", "-w", str(workspace_path), "--full"]) + assert result.exit_code == 2, result.output + assert "Nothing was verified" in result.output + + def test_run_no_requirements_with_allow_empty_exits_zero(self, ws): + _, workspace_path = ws + result = runner.invoke(app, [ + "proof", "run", "-w", str(workspace_path), "--full", "--allow-empty", + ]) assert result.exit_code == 0, result.output - assert "No applicable obligations found" in result.output def test_run_invalid_gate_exits_nonzero(self, ws): """run with an unrecognised --gate should exit non-zero and print error.""" diff --git a/tests/cli/test_proof_empty_ledger_1118.py b/tests/cli/test_proof_empty_ledger_1118.py new file mode 100644 index 00000000..860bf09b --- /dev/null +++ b/tests/cli/test_proof_empty_ledger_1118.py @@ -0,0 +1,294 @@ +"""#1118 — `cf proof run` exited 0 on an empty ledger, so PROVE was a vacuous pass. + +The quickstart's last step, on the product's stated differentiator, printed +"No applicable obligations found." in green and exited 0. A user reads that as +"PROOF9 quality gates passed". Nothing had been verified — and every new +workspace is in exactly that state, including after a full agent run had written +code and tests. + +An empty ledger is now its own outcome: exit 2, distinct from pass (0) and fail +(1), so CI cannot be green on it and a script can tell the two apart. +""" + +from pathlib import Path +import re +from unittest.mock import patch + + +import pytest +from typer.testing import CliRunner + +from codeframe.cli.app import app +from codeframe.core.workspace import create_or_load_workspace + +def _flat(text: str) -> str: + """Rich hard-wraps console output, so assertions must ignore line breaks.""" + return re.sub(r"\s+", " ", text) + + +pytestmark = pytest.mark.v2 + +runner = CliRunner() + + +@pytest.fixture +def workspace_dir(tmp_path: Path) -> Path: + create_or_load_workspace(tmp_path) + return tmp_path + + +class TestAnEmptyLedgerIsNotAPass: + """AC: zero applicable obligations is reported distinctly from a pass.""" + + def test_it_does_not_exit_zero(self, workspace_dir): + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + assert result.exit_code != 0, ( + "exit 0 on an empty ledger is what made PROVE a vacuous pass" + ) + + def test_it_is_distinguishable_from_a_failure(self, workspace_dir): + """AC: distinct in the exit code — 2, not 1. + + A failed obligation and an absent one need different responses, so they + need different codes. + """ + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + assert result.exit_code == 2 + + def test_it_does_not_claim_anything_passed(self, workspace_dir): + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + lowered = result.output.lower() + assert "nothing was verified" in lowered + assert "not a pass" in lowered + + def test_it_says_how_to_get_a_first_obligation(self, workspace_dir): + """AC: tell a new user how to proceed, not that the gate was satisfied.""" + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + assert "cf proof capture" in result.output + + +class TestTheEscapeHatch: + """AC: an explicit flag, defaulting to the safe behaviour.""" + + def test_allow_empty_exits_zero(self, workspace_dir): + result = runner.invoke( + app, ["proof", "run", "-w", str(workspace_dir), "--allow-empty"] + ) + assert result.exit_code == 0 + + def test_allow_empty_still_says_nothing_was_verified(self, workspace_dir): + """Opting into exit 0 must not also silence the explanation.""" + result = runner.invoke( + app, ["proof", "run", "-w", str(workspace_dir), "--allow-empty"] + ) + assert "nothing was verified" in result.output.lower() + + def test_the_safe_behaviour_is_the_default(self, workspace_dir): + """The flag has to be asked for; empty is not silently green.""" + assert ( + runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]).exit_code + != 0 + ) + + +class TestStatusSaysTheSameThing: + """The two surfaces should not disagree about what an empty ledger means.""" + + def test_status_frames_it_as_unverified(self, workspace_dir): + result = runner.invoke(app, ["proof", "status", "-w", str(workspace_dir)]) + lowered = result.output.lower() + assert "nothing" in lowered and "verified" in lowered + assert "cf proof capture" in result.output + + +class TestAScopeFilteredRunIsNotAnEmptyLedger: + """Raised in review, and a real regression in my first version. + + `run_proof` returning {} is ambiguous: the ledger may be empty, or it may + hold requirements none of which intersect the changed scope. Only the first + is the #1118 vacuous pass. Conflating them told a user with three + requirements that their ledger was empty, and failed CI on a doc-only PR + because its scope matched nothing — a new bug in the name of fixing one. + """ + + def _capture_req(self, workspace_dir: Path, scope_path: str) -> None: + """A real requirement scoped to a path the run will not touch.""" + result = runner.invoke( + app, + [ + "proof", "capture", + "--title", "Login must not 500", + "--description", "Expected 200, got 500 on POST /login", + "--where", scope_path, + "--severity", "high", + "--source", "production", + "-w", str(workspace_dir), + ], + ) + assert result.exit_code == 0, result.output + + def _run_with_nothing_in_scope(self, workspace_dir: Path): + """`run_proof` returns {} because the scope filter skipped everything. + + Patched rather than staged through git: with no working-tree changes the + detector fails closed and runs every requirement, so the real filter + cannot produce this state here. The ambiguity under test is in how the + CLI reports an empty result, not in scope detection. + """ + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + return runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + + def test_it_does_not_claim_the_ledger_is_empty(self, workspace_dir): + self._capture_req(workspace_dir, "src/auth/login.py") + + result = self._run_with_nothing_in_scope(workspace_dir) + + assert "no proof obligations in this workspace" not in result.output.lower() + assert "cf proof capture" not in result.output, ( + "telling someone with requirements to capture their first one is wrong" + ) + + def test_it_does_not_fail_ci_on_an_out_of_scope_change(self, workspace_dir): + """A doc-only PR must not be failed by the scope filter working.""" + self._capture_req(workspace_dir, "src/auth/login.py") + + result = self._run_with_nothing_in_scope(workspace_dir) + + assert result.exit_code == 0, result.output + + def test_it_still_says_nothing_was_verified(self, workspace_dir): + """Accurate either way — it just is not the vacuous-pass case.""" + self._capture_req(workspace_dir, "src/auth/login.py") + + result = self._run_with_nothing_in_scope(workspace_dir) + + assert "nothing was verified" in result.output.lower() + assert "--full" in result.output, "point at the way to check them anyway" + + def test_a_truly_empty_ledger_still_exits_two(self, workspace_dir): + """The two paths must not have been collapsed the other way.""" + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + assert result.exit_code == 2 + + def test_full_mode_does_not_offer_full_as_the_remedy(self, workspace_dir): + """--full never consults scope, so re-running it changes nothing.""" + self._capture_req(workspace_dir, "src/auth/login.py") + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + result = runner.invoke( + app, ["proof", "run", "-w", str(workspace_dir), "--full"] + ) + assert result.exit_code == 0, result.output + assert "--full" not in _flat(result.output) + + +class TestTheReasonIsDerivedNotGuessed: + """Third review finding, and the reason the first two kept recurring. + + `run_proof` returning {} has three causes. Inferring which one from the + --full flag was wrong twice: it short-circuits when the runnable set is + empty, *before* scope detection, so an all-SATISFIED (scoped) or all-WAIVED + ledger never had its scope evaluated at all. The reason now comes from the + runner's own `_requirements_for_run`, so the CLI cannot drift from it. + """ + + def _capture(self, workspace_dir: Path) -> None: + result = runner.invoke( + app, + [ + "proof", "capture", + "--title", "Login must not 500", + "--description", "Expected 200, got 500", + "--where", "src/auth/login.py", + "--severity", "high", + "--source", "production", + "-w", str(workspace_dir), + ], + ) + assert result.exit_code == 0, result.output + + def _req_id(self, workspace_dir: Path) -> str: + from codeframe.core.proof import ledger + from codeframe.core.workspace import get_workspace + + return ledger.list_requirements(get_workspace(workspace_dir))[0].id + + def test_a_waived_only_ledger_is_not_blamed_on_scope(self, workspace_dir): + """The scoped path: run_proof short-circuits before scope is computed.""" + self._capture(workspace_dir) + waive = runner.invoke( + app, + [ + "proof", "waive", self._req_id(workspace_dir), + "--reason", "accepted risk for now", + "-w", str(workspace_dir), + ], + ) + assert waive.exit_code == 0, waive.output + + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + + assert result.exit_code == 0, result.output + assert "changed files" not in _flat(result.output), ( + "scope was never evaluated — the requirement was excluded by status" + ) + assert "none are runnable" in _flat(result.output) + assert "waived" in result.output + + def test_it_offers_scope_as_a_candidate_not_a_verdict(self, workspace_dir): + """With an eligible requirement the cause is genuinely ambiguous. + + Scope, --gate, disabled gates in proof_config.json, or a requirement + with no obligations all produce {} here, and run_proof does not report + which. Asserting one was wrong four review rounds running. + """ + self._capture(workspace_dir) + + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + + flat = _flat(result.output) + assert result.exit_code == 0, result.output + assert "Possible reasons" in flat, "it must not assert a single cause" + assert "changed files" in flat, "scope is still one of the candidates" + + def test_the_gate_filter_is_named_when_one_was_used(self, workspace_dir): + """`--gate unit` excluding every obligation is one of the causes.""" + self._capture(workspace_dir) + + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + result = runner.invoke( + app, ["proof", "run", "-w", str(workspace_dir), "--gate", "unit"] + ) + + flat = _flat(result.output) + assert result.exit_code == 0, result.output + assert "--gate unit" in flat + + def test_an_empty_ledger_is_still_the_vacuous_pass_case(self, workspace_dir): + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + assert result.exit_code == 2 + assert "cf proof capture" in result.output + + def test_full_mode_omits_scope_from_the_candidates(self, workspace_dir): + """--full provably ignores scope, so listing it is an impossible cause.""" + self._capture(workspace_dir) + + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + result = runner.invoke( + app, + ["proof", "run", "-w", str(workspace_dir), "--full", "--gate", "unit"], + ) + + flat = _flat(result.output) + assert result.exit_code == 0, result.output + assert "changed files" not in flat, "scope cannot be the reason under --full" + assert "--gate unit" in flat, "the real candidate is still named" + + def test_the_gate_candidate_is_omitted_when_no_gate_was_passed(self, workspace_dir): + """Only list causes that could actually apply to this invocation.""" + self._capture(workspace_dir) + + with patch("codeframe.core.proof.runner.run_proof", return_value={}): + result = runner.invoke(app, ["proof", "run", "-w", str(workspace_dir)]) + + assert "--gate" not in _flat(result.output)