diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml index 771cbf05b..4464ab7ed 100644 --- a/.github/workflows/standards-build.yml +++ b/.github/workflows/standards-build.yml @@ -70,7 +70,7 @@ jobs: # matrix is the entries it selects. plan: name: which workspaces this change touches - runs-on: linux-arm64 + runs-on: linux outputs: include: ${{ steps.plan.outputs.include }} any: ${{ steps.plan.outputs.any }} @@ -406,7 +406,12 @@ jobs: echo "== $h ==" out="$(cargo kani -p joulespec-core --harness "$h" 2>&1)" echo "$out" | grep -E '^ \*\* |^VERIFICATION' - echo "$out" | grep -q '^VERIFICATION:- SUCCESSFUL' \ + # A here-string, not `echo | grep -q`: grep -q exits at the first + # match, echo then dies of SIGPIPE (141), and `set -o pipefail` + # turns a match into a failure. It is a race on how much of $out + # fits the pipe buffer, so it passed while this harness reported 15 + # properties and failed at 336. + grep -q '^VERIFICATION:- SUCCESSFUL' <<<"$out" \ || { echo "$h did not verify"; exit 1; } # "N of M cover properties satisfied". Both numbers are read with # their own expression rather than by splitting one capture, so @@ -434,7 +439,7 @@ jobs: echo "mutation applied: the scale is now computed in 64 bits" out="$(cargo kani -p joulespec-core --harness the_ratio_rule_is_total_over_every_input 2>&1 || true)" echo "$out" | grep -E '^ \*\* |^VERIFICATION' - echo "$out" | grep -q '^VERIFICATION:- FAILED' \ + grep -q '^VERIFICATION:- FAILED' <<<"$out" \ || { echo "the prover did not refute an overflowing ratio rule"; exit 1; } # The NVML backends sit behind features no workspace member enables