Offer the long timeouts a survey needs

[TheLazyCat00]

Adds 1h and 3h to the proof workflow's timeout choices, and raises the job cap to match.

Why

The first level-3 survey on main (run 32233014108) came back as a floor:

Survey at level 3: 1290 distinct divergence site(s), 1 accepting abstract pair(s),
121131 pairs explored (incomplete: the counts are a floor).
  1. AMPERSAND UIDENT LBRACKET RBRACKET SEMICOLON EOF

The walk was still going when the 30-minute deadline arrived, and 30m was the largest value the workflow offered — so there was no way to ask for more from Actions at all.

A survey is the mode that needs the long end. It cannot stop at the first divergence, which is the entire point of it, so its cost is the size of the abstract space rather than the distance to the first candidate. At roughly 67 pairs/second (121,131 pairs in 1,800s) against a 7,895,160-pair budget, the space is hours wide.

An ordinary proof is unaffected. It stops as soon as it has a verdict, and has never needed more than a few minutes of abstract phase — 30m was already generous.

The job cap

timeout-minutes has to clear the worst case any offered option permits: two phases at the largest value, plus checkout, Devbox, the opam bootstrap and the build. A job killed by the cap writes no verdict line, so ambiguity-verdict fails closed at status 2 and reports a broken run where the honest answer was "not proven" — the failure mode #59 and #60 already went to some trouble to remove.

75 → 380. It is a backstop, not an expected duration: a survey exits before the concretization search, so it spends one phase rather than two, and only an ordinary proof can reach the full six hours.

Verification

No code changes. parse_duration accepts every offered value (5m, 15m, 30m, 1h, 3h → 300, 900, 1800, 3600, 10800 seconds), the YAML parses, and the two comments describing the old 30m ceiling are updated rather than left contradicting the options above them.

🤖 Generated with Claude Code

https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

@TheLazyCat00, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 6 minutes

Limit details: You’ve used the included review currently available.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits within each organization.

For paid Pro and Pro+ reviews, CodeRabbit uses a developer's included PR review attempts over the past 7 days to set the current hourly allowance. At typical activity levels, the full plan allowance applies. Higher sustained activity can lower the allowance until earlier attempts leave the 7-day window.

Please refer docs for additional details.

Review details

⚙️ Run configuration

Configuration used: Repository: zane-lang/coderabbit/.coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 7411f2c1-8f15-48ae-9e29-a93ba75c4621

📥 Commits

Reviewing files that changed from the base of the PR and between 082cb0c and e686561.

📒 Files selected for processing (1)

• .github/workflows/ambiguity-prove.yml

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}