Raise the harness timeout of the cargo_autoharness_fmt_impls test - #4923
Merged
Merged
Conversation
On the macOS x86_64 CI runners (`regression (macos-15-intel)`), the `LowerExp`, `UpperExp` and `Pointer` harnesses of this test take 40-60s, right at `kani autoharness`'s default `--harness-timeout` of 60s. When one of them times out, its expected `Failed Checks:` line is missing and the test fails. In 33 failing macos-15-intel regression jobs between 2026-09-28 and 2026-09-30, this test failed every time, with 1-3 of those harnesses timing out; in 32 of them it was the only failing test (in the other, `cargo_autoharness_wtf8`'s `len` harness also timed out, at 5m). Locally the three harnesses take about 10s, and a 3s timeout reproduces the failure exactly. Pass `--harness-timeout 5m`, as the other autoharness tests do. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Copilot review overview
🟢 Approval recommended
The focused change matches existing autoharness test conventions and correctly addresses the observed timeout failures.
Review effort: Balanced
Findings: None
What changed in this PR
Raises the formatting autoharness test timeout to prevent macOS Intel CI flakes.
Changes:
- Sets a five-minute harness timeout.
- Enables the required unstable option and documents the rationale.
| File | Description |
|---|---|
tests/script-based-pre/cargo_autoharness_fmt_impls/fmt-impls.sh |
Configures and explains the increased timeout. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
feliperodri
approved these changes
Sep 30, 2026
Member
|
let's merge and see if this decreases the noise. I'll keep an eye on those slow ones. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Pass
--harness-timeout 5mtoscript-based-pre/cargo_autoharness_fmt_impls, as the other autoharness tests (bounded,bounds,byte_str,c_str,formatter,wtf8) already do.Why. On the macOS x86_64 runners (
regression (macos-15-intel)), theLowerExp,UpperExpandPointerharnesses of this test take 40–60 s, right atkani autoharness's default--harness-timeoutof 60 s. When one of them times out, CBMC reportsCBMC timed outinstead of the expected failure, the test'sFailed Checks: "lower exp"/"upper exp"/"pointer"line is missing, and the test fails. The same harnesses take about 10 s on Linux.Evidence. I went through the logs of the
regression (macos-15-intel)jobs between 2026-09-28 and 2026-09-30. 33 of them failed. This test failed in all 33, with 1–3 of those three harnesses timing out each time, and in 32 of them it was the only failing test. The one exception, #4903's merge-queue push run, also hadcargo_autoharness_wtf8'slenharness time out, at 5 m. On main pushes alone, the job failed 7 times out of 12 on 2026-09-30. The failures are independent of the changes under test:LowExp,UpExp,Ptrtimed out; every other regression job passed)mainpushes: 36654469481, 36656240395, 36657849257, 36659060566, 36670355214, 36674524840&Wtf8arguments under --bounded-arguments #4809 36654883143, Fetch a candidate's MIR with the provider that serves its body kind #4848 36663305755, Strip the crate prefix from scanner names to match kani list #4903 36667236036, Fix ICE on pattern types over wide pointers under -Z valid-value-checks #4856 36670723600, LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon bump will touch #4881 36596324505, LLBC: name inherent methods instead of aborting, and deduplicate the name builders #4882 36612997613--quiet#4771 36620184925The runner image version (
20260819.586) was the same in passing and failing runs.Manual testing. Locally the three harnesses take about 10 s each. Running the test with
--harness-timeout 3sreproduces the CI failure exactly: the same three harnesses time out, theirFailed Checkslines are missing, and the summary still reports 9 failures. With this change,cargo run -p compiletest -- --suite script-based-pre --mode exec cargo_autoharness_fmt_implspasses.If the macOS Intel runner gets much slower, a longer timeout alone may not be enough; making these three harnesses cheaper would be the next step.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.