From e6865613a8612e7553c3294631309f0800c08d49 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 19 Aug 2026 09:12:52 +0000 Subject: [PATCH] Offer the long timeouts a survey needs The level-3 survey on main came back as a floor: 1290 distinct divergence sites and 1 accepting abstract pair after 121131 pairs, with the walk still going when the 30-minute deadline arrived. 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 -- that is the whole point of it -- so its cost is the size of the abstract space rather than the distance to the first candidate, and at roughly 67 pairs per second the space is hours wide. An ordinary proof is unaffected: 30m already exceeds what it has ever needed, since it stops as soon as it has a verdict. 1h and 3h join the offered values. The job cap has to clear the worst case an option permits -- two phases at the largest value, plus checkout, Devbox, the opam bootstrap and the build -- because a job killed by the cap writes no verdict line, and ambiguity-verdict then fails closed at status 2, reporting a broken run where the answer was "not proven". A survey spends one phase rather than two, since it exits before concretization, so only an ordinary proof can reach the full six hours. Both comments describing the old 30m ceiling are updated with it. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01N4KejxPN4Q9uQ67dHwUDgj --- .github/workflows/ambiguity-prove.yml | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ambiguity-prove.yml b/.github/workflows/ambiguity-prove.yml index 65659ff..ff8f2c6 100644 --- a/.github/workflows/ambiguity-prove.yml +++ b/.github/workflows/ambiguity-prove.yml @@ -41,9 +41,10 @@ on: timeout: # Each search phase gets this in full: the abstract proof runs under # its own deadline, and the concretization search that may follow - # starts a fresh one. Budget the job for twice the value chosen, on - # top of checkout, Devbox, the opam bootstrap and the build — 30m is - # the largest offered, so the 60-minute job cap holds. + # starts a fresh one, so an ordinary proof can spend twice the value + # chosen. A survey exits before concretization and spends it once. + # The long options exist for surveys, which cannot stop at the first + # divergence; 30m is already generous for an ordinary proof. description: Timeout per search phase required: true default: 15m @@ -52,6 +53,8 @@ on: - 5m - 15m - 30m + - 1h + - 3h survey: # Diagnostic rather than verdict: instead of stopping at the first # divergence, walk the whole abstract space and count how many distinct @@ -83,13 +86,19 @@ jobs: prove: name: Prove level ${{ inputs.level || '3' }} on ${{ inputs.ref || github.ref_name }} runs-on: ubuntu-latest - # Both search phases obey --timeout, so the tool now bounds itself: at the - # largest offered value the two phases total 60 minutes. This cap is the + # Both search phases obey --timeout, so the tool bounds itself: at the + # largest offered value the two phases total six hours. This cap is the # backstop around them and has to clear that total plus checkout, Devbox, # the opam bootstrap and the build, because a job killed here prints no # verdict line at all and the report the verdict is read from is never # written — turning an honest "not proven" into a broken run. - timeout-minutes: 75 + # + # It is a backstop, not an expected duration. A survey is what needs the + # long end: it cannot stop at the first divergence, and at level 3 the walk + # was still going after 121k pairs in 30 minutes, so the counts came back + # as a floor. Only a survey run should reach for 3h, and a survey exits + # before the concretization search, so it spends one phase rather than two. + timeout-minutes: 380 env: # Public ubuntu-latest runners provide four CPUs and 16 GB RAM: # https://docs.github.com/en/actions/reference/runners/github-hosted-runners#standard-github-hosted-runners-for-public-repositories