Skip to content

Commit b792a35

Browse files
avrabeclaude
andauthored
chore(ci): raise verify-gate timeout 30 → 60 min for lake build (#229)
After #227 reverted TEST-PROOF-LATENCY / TEST-PROOF-ARINC653 verification steps from sorry-grep to `cd proofs && lake build`, the first PR after #227 (#228 Mermaid M3) timed out the verify-gate at the 30-minute hard budget. lake build against Mathlib on a cold elan cache takes 25–35 min; the runner ran for 26 min before hitting the timeout, then GitHub killed the orphan `lake` process during job cleanup. Bumps the verify-gate job's `timeout-minutes` from 30 → 60 to give `lake build` headroom while the smithy team adds Lake build-artifact caching across runs. Once that lands, the timeout can drop toward the original 20m. The dedicated "Lean proof typecheck (lake build)" workflow has its own budget for the same step (already empirically green), so this only affects the rivet verification gate runs. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
1 parent d902bf2 commit b792a35

1 file changed

Lines changed: 6 additions & 1 deletion

File tree

.github/workflows/verification-gate.yml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,12 @@ jobs:
1717
rivet-verification:
1818
name: Verification Gate (rivet-driven)
1919
runs-on: [self-hosted, linux, x64, rust-cpu]
20-
timeout-minutes: 30
20+
# 60m budget: TEST-PROOF-* steps run `cd proofs && lake build`, which
21+
# against Mathlib on a cold elan cache takes 25–35 min. Once smithy
22+
# adds Lake build-artifact caching across runs, this can drop back
23+
# toward 20m. The dedicated "Lean proof typecheck" workflow has its
24+
# own budget for the same step.
25+
timeout-minutes: 60
2126
env:
2227
CARGO_TERM_COLOR: always
2328
RUSTFLAGS: -D warnings

0 commit comments

Comments
 (0)