Skip to content

Support alternative expected outputs in output tests; add variants for the par test (alternative to #22286) - #22297

Draft
JasonGross wants to merge 2 commits into
rocq-prover:masterfrom
JasonGross:output-tests-alternate-expectations
Draft

Support alternative expected outputs in output tests; add variants for the par test (alternative to #22286)#22297
JasonGross wants to merge 2 commits into
rocq-prover:masterfrom
JasonGross:output-tests-alternate-expectations

Conversation

@JasonGross

@JasonGross JasonGross commented Jul 21, 2026

Copy link
Copy Markdown
Member

This implements one of the two alternative strategies proposed in the review of #22286 for the flaky output/Partac.v test on Windows CI, discussed at #22286 (comment). It contains no stm/ changes. The other alternative (runner-side filtering) is #22295.

Problem

output/Partac.v uses STM par: workers. When the master tears them down, a worker's read/write to the now-closed master can fail with a connection-loss error (Windows: WSAECONNRESET/WSAECONNABORTED; Unix: EPIPE) that takes the loud Slave: critical exception / Fatal marshal error branch of the worker main loop, and the message can race into the captured output, making the test flaky (mostly on Windows CI).

Strategy (multiple accepted expected outputs)

Add generic support for output tests with more than one accepted output. An output test may provide alternative accepted references as sibling files named foo.out.variant-<name> (any suffix after .out.variant-). A new diff_against_candidates make macro compares the produced output against the primary foo.out first and then, only if that differs, against each foo.out.variant-* in shell glob order; the test passes as soon as one candidate matches (first match wins). If none matches, the failure report shows the diff against the primary foo.out and lists every candidate that was tried. When a test has no variants, behaviour and output are byte-for-byte identical to before.

Variant files can be hand-authored or generated via approve-output (see Approve workflow below). This is documented at the macro, at approve-output, and in test-suite/README.md.

Approve workflow

approve-output supports both replacing and adding expectations, selected by an APPROVE variable:

  • APPROVE=replace — the produced output replaces the primary foo.out (today's behaviour); existing foo.out.variant-* are left untouched.
  • APPROVE=add — the produced output is added as the next free numeric variant foo.out.variant-<N> instead of replacing anything; it is a no-op (deduplicated) if byte-identical to the primary or an existing variant.

With APPROVE unset the mode is chosen per test: replace for a single-expectation test (just foo.out), add for a test that already has foo.out.variant-* files — so approving a multi-expectation test never clobbers the primary or silently drops existing variants. Set APPROVE explicitly to override.

Data added

  • Self-test of the mechanism: output/AlternateExpectedOutput.v (Check tt.) whose primary .out deliberately does not match the produced output, while AlternateExpectedOutput.out.variant-accepted does — so the test passes only by matching a variant, exercising the candidate loop end to end.
  • Par-tactic variants: output/Partac.out.variant-* covering the connection-loss teardown lines (forcibly closed by the remote host, Connection reset by peer, Broken pipe, aborted by the software in your host machine, and a Fatal marshal error form). The connection-loss texts are taken verbatim from Exit STM workers quietly on lost master connection (flaky output/Partac.v on Windows CI) #22286.

Honest limitation

The teardown-noise line carries a per-run worker-id prefix (<id>] Slave: critical exception: ...), which a fixed variant file cannot match under plain diff. These variants therefore match only when that prefix happens to equal the one baked into the variant, so they are best-effort for the Partac flake. The runner-side filter in #22295 matches on substrings and is prefix-agnostic, so it is the more robust fix for this particular case; this PR's value is the general multiple-accepted-output mechanism, which is useful for tests whose variation is deterministic and enumerable. I could not retrieve a real polluted Windows log (the PR that exhibited the flake, #22266, has since been rebased green), so the variants are constructed from #22286's patterns.

Test plan

  • output/Partac.v passes on a clean run (matches the primary).
  • Self-test passes purely via its variant (primary intentionally mismatches).
  • Simulated polluted Partac output (noise appended, matching a variant's prefix) matches Partac.out.variant-connreset-windows.
  • A genuinely wrong produced output (a real regression, not noise) matches no candidate and correctly fails.
  • Single-candidate (no-variant) failures produce output byte-identical to the previous diff behaviour.
  • approve-output modes verified: replace-default on a single-expectation test; add-by-request on a single-expectation test; add-by-default on a multi-expectation test; dedupe no-op against both primary and an existing variant; replace-override on a multi-expectation test touches only the primary; deterministic next-free numbering; unknown APPROVE value errors without touching references.
  • test-suite/Makefile parses cleanly; dev/lint-commits.sh passes.

No changelog entry: this is an internal test-suite/CI change with no user-visible effect (consistent with recent test-suite-only commits).

Written by Claude (Anthropic AI) at the request of and under the supervision of @JasonGross.

🤖 Generated with Claude Code

https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw

…ants

Some output tests have output that legitimately varies between runs or
platforms in ways that are not worth (or not possible to) normalise away
in the post-processing pipeline. output/Partac.v is one: its STM par:
workers may, when the master tears them down, race a "connection lost"
teardown message into the captured output, mostly on Windows CI, making
the test flaky.

Let an output test provide alternative accepted references as sibling
files named foo.out.variant-<name>. The produced output is compared
against the primary foo.out first and then, only if that differs,
against each variant in shell glob order; the test passes as soon as one
candidate matches (first match wins). If none matches, the failure
report shows the diff against the primary and lists every candidate that
was tried. approve-output still writes only the primary foo.out; variant
files are hand-authored data.

Add a small self-test of the mechanism (output/AlternateExpectedOutput.v,
whose primary reference deliberately does not match so the test passes
only via a variant) and, for output/Partac.v, variants covering the
connection-loss teardown lines. Note: the worker-id prefix on those
lines varies per run, so these fixed variants are best-effort; the
runner-side filter alternative is prefix-agnostic and thus more robust.

This is an alternative to rocq-prover#22286, which fixes the same flake in the STM.

Co-Authored-By: Claude Fable 5 <[email protected]>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
@coqbot-app coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 21, 2026
Extend approve-output so it can both replace the primary reference and
add the produced output as a new alternative expectation, via an APPROVE
variable:

  APPROVE=replace  produced output replaces the primary $*.out (as
                   before); existing $*.out.variant-* are left untouched.
  APPROVE=add      produced output is added as the next free numeric
                   variant $*.out.variant-<N>; a no-op (deduplicated) if
                   it is byte-identical to the primary or an existing
                   variant.

With APPROVE unset the mode is chosen per test: replace for a
single-expectation test (just $*.out), add for a test that already has
$*.out.variant-* files, so approving a multi-expectation test never
clobbers the primary or drops existing variants. Documented at the recipe
and in test-suite/README.md.

Co-Authored-By: Claude Fable 5 <[email protected]>
Claude-Session: https://claude.ai/code/session_019ttctspSoVoquHLQtbPVZw
@SkySkimmer

Copy link
Copy Markdown
Contributor

I don't think we want this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants