Follow the default branch and budget the proof job for both phases - #60
Conversation
Both workflows offered essential/parser as the revision to check out, a branch that has outlived its purpose and is due to be deleted. Neither would have run against it: the branch predates .github/scripts entirely, so the step that invokes the runner script would fail on a missing file. That made the search workflow unusable at its own default, and the proof workflow inherited the same default from it. Both now offer main, which is where the grammar lives. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj
#59 gave the abstract proof a deadline of its own, so --timeout applies to each search phase rather than only to the concretization search. Two comments here described the old behaviour, and one of them was load-bearing. The input is now labelled per phase, since a run picking 30m is asking for up to an hour of searching rather than half of one. The job cap has to clear that. At 60 minutes it sat exactly on the worst-case search total with nothing left for checkout, Devbox, the opam bootstrap or the build, so the largest offered timeout would have been killed mid-run -- and a killed job writes no verdict line, so ambiguity-verdict fails closed at status 2 and an honest "not proven" is reported as a broken run. That is the failure #59 set out to remove; leaving the cap here would have reintroduced it one layer up. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj
|
Warning Review limit reached
Next review available in: 38 minutes Limit details: You’ve used all 1 included review currently available under your plan. 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 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 for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Repository: zane-lang/coderabbit/.coderabbit.yaml Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
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. Comment |
2 participants
Two small fixes to the ambiguity workflows. The second is the one that matters.
Point both workflows at the default branch
refdefaulted toessential/parserinambiguity-search.ymlandambiguity-prove.yml. That branch is stale and due for deletion, and it has no.github/scripts/directory, so a search dispatched at its own default would fail after paying for checkout, Devbox, the opam bootstrap and the build. Both now default tomain.Budget the proof job for a timeout that bounds both phases
#59 gave the abstract proof a deadline of its own, so
--timeoutnow applies to each search phase rather than only to the concretization search. Two comments here described the old behaviour, and one of them was load-bearing.The input is relabelled per phase, since a run picking
30mis asking for up to an hour of searching rather than half of one.The job cap has to clear that. At
timeout-minutes: 60it sat exactly on the worst-case search total, with nothing left for checkout, Devbox, the opam bootstrap or the build — so the largest offered timeout would have been killed mid-run. A killed job writes no verdict line, so the reportambiguity-verdictreads its answer out of is never written, and it fails closed at status 2: a broken run, where the honest answer was "not proven".That is the failure #59 set out to remove from the engine. Leaving the cap at 60 would have reintroduced it one layer up, which is why this is not just a comment refresh. Raised to 75.
Note on the branch
The branch was auto-deleted when #58 merged, so it is restarted from current
mainwith the unmergedrefcommit reapplied rather than stacked on already-merged history.Verification
YAML parses and the three changed values read back as intended (
timeout-minutes: 75,refdefaultmainin both workflows,Timeout per search phase). No code changes, sobuild-and-testcovers nothing here; the real check is a dispatch, and run 32063418332 is currently exercising the prove workflow onmain— though at15m, not the30mcase this fixes.🤖 Generated with Claude Code
https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj
Generated by Claude Code