ci: make scheduled verification a cold build - #2217
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟠 1 finding(s) (1 high) — see inline comments.
✅ Posted 1 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: config-docs (router-v10)
- Changed files: 3 supported / 3 total; Lean 0, trust docs 0, workflow/scripts 3, contracts 0, docs 0
- Changed lines: 46 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 1; files 3; tokens 1118795; tool calls 76; warnings 0; duration 283s
- Largest changed files: .github/workflows/verify.yml (+11/-7), scripts/verify_sync_spec_source.py (+9/-7), scripts/verify_sync_spec.json (+6/-6)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
|
Codex Review: Didn't find any major issues. Hooray! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟢 No findings from the OCR first pass. Advisory only.
No comments generated. Looks good to me.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: config-docs (router-v10)
- Changed files: 3 supported / 3 total; Lean 0, trust docs 0, workflow/scripts 3, contracts 0, docs 0
- Changed lines: 59 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 3; tokens 403403; tool calls 42; warnings 0; duration 209s
- Largest changed files: scripts/verify_sync_spec.json (+15/-6), scripts/verify_sync_spec_source.py (+13/-7), .github/workflows/verify.yml (+11/-7)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review |
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review |
|
@codex review |
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 58f031ef95
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_74ed8a29-dfc2-49db-9249-c8b7866e0e53) |
|
Codex Review: Didn't find any major issues. 🚀 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟠 2 finding(s) (1 high / 1 medium) — see inline comments.
✅ Posted 2 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: config-docs (router-v10)
- Changed files: 7 supported / 7 total; Lean 0, trust docs 0, workflow/scripts 6, contracts 0, docs 1
- Changed lines: 204 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 2; files 7; tokens 1351812; tool calls 113; warnings 0; duration 598s
- Largest changed files: scripts/verify_sync_spec.json (+55/-6), scripts/verify_sync_spec_source.py (+46/-7), .github/workflows/verify.yml (+34/-18), scripts/check_verify_sync.py (+22/-0), docs/CI_RUNNERS.md (+6/-3)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_411d57d9-6ba2-4096-b3da-01bfd3b36307) |
|
Codex Review: Something went wrong. Try again later by commenting “@codex review”. ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_a9815d73-0133-4d7f-9d30-946a790e8b1e) |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
OpenCodeReview first-pass review🟠 1 finding(s) (1 medium) — see inline comments. ✅ Posted 1 inline comment(s). OCR pilot metrics & packet coverageOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_1aa7ec12-232e-4eb9-9d9e-ff8ef78b24b8) |
|
Codex Review: Didn't find any major issues. Delightful! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟢 No findings from the OCR first pass. Advisory only.
No comments generated. Looks good to me.
OCR stderr highlights
[ocr] ✘ file_read failed: invalid line range: start_line 470 is greater than end_line 100
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: small-lean (router-v10)
- Changed files: 8 supported / 8 total; Lean 1, trust docs 0, workflow/scripts 6, contracts 0, docs 1
- Changed lines: 209 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 8; tokens 1906014; tool calls 130; warnings 0; duration 631s
- Largest changed files: scripts/verify_sync_spec.json (+55/-6), scripts/verify_sync_spec_source.py (+46/-7), .github/workflows/verify.yml (+34/-18), scripts/check_verify_sync.py (+22/-0), docs/CI_RUNNERS.md (+7/-3)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Merging with corroborating evidence from last night: the un-provisioned cgroup-capped runner on agent-core picked up |
1 participant
Summary
build-heavycapability label and document/install that label consistentlyWhy
The daily workflow forced the full graph but still consumed runner-local build and compiler state, so it did not prove that pinned sources build cleanly. During validation, the existing generic build route also exposed a capped 20 GiB host and reused-workspace cleanup hazards. This slice turns the scheduled lane into a reproducible cold receipt and gives heavy jobs an explicit resource capability gate.
Validation
make check: 640 tests, exit 0, 1:40.34, 78,536 KiB peak RSSpython3 scripts/check_verify_sync.py: 9 invariant groups, exit 0python3 -m unittest scripts.test_check_verify_sync scripts.test_ci_infra_maintenance: 46 tests, exit 0lake build Compiler.Modules.CallsTest: exit 0, 2:26.70, 64 remote jobs/threads requested by the focused run, nodeold-agentlake build PrintAxioms Compiler Contracts: 2,687 jobs, exit 0, 1:29:40, 17,152 KiB local orchestrator peak RSS, nodeold-agentmake test-evmyullean-fork: exit 0, 1:06:18, 17,152 KiB local orchestrator peak RSS; bridge lemmas/test, native harness, and EndToEnd receipts passed acrossashurandbabylon30577938694passed: build, compiler regressions/audits, patched Foundry, gas calibration, and all four Foundry shardsLean
4.31.0, Lake5.0.0,LEAN_NUM_THREADS=8for final acceptance commands. EVMYulLean remains pinned to official revisionf7e4ee0dc8f8d5265ce822a937ab5be771f182e9. No theorem, axiom, proof gate, allowlist, unsafe declaration, or bypass was added.