ci: stabilize verify workflow timeouts#1647
Conversation
![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: 4d221cbe9b
ℹ️ 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".
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
| \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``` |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: cf4a0048a5
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e5bb37ee18
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0fdbd564c8
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bfb315161a
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6232ca36c3
ℹ️ 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".
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
| raw = _extract_top_level_job_value(extract_job_body(workflow_text, job, workflow_path), "timeout-minutes") | ||
| if raw is None: | ||
| continue | ||
| timeouts[job] = int(raw) |
There was a problem hiding this comment.
Watchdog crashes on dynamic timeout expressions
High Severity
load_timeouts_from_text calls int(raw) on every extracted timeout-minutes value. Several jobs now use dynamic expressions like ${{ fromJSON(github.event_name == 'workflow_dispatch' && inputs.clean_build && '60' || '35') }}, which are not valid integer strings. This causes an unhandled ValueError that crashes the watchdog script. The except urllib.error.URLError handler in main() does not catch ValueError, so the timeout-watchdog CI job will fail on every workflow run.
Additional Locations (1)
Inspired by lfglabs-dev/verity#1647. Instead of each downstream job rebuilding from cache, verity-proofs now uploads the verified .lake workspace as an artifact. verity-compiler-artifacts downloads it directly, eliminating redundant Lean compilation. Also save the Lean/Lake cache only on master to avoid cache pollution from PR branches. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
#363) * Mark accrueInterestPublic as macro-migrated The EDSL accrueInterest function already implements both the public entry point (id computation, market-exists check) and the internal _accrueInterest logic. Update obligation to reflect this — all 18/18 obligations are now macroMigrated. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Fix CI parity target tuple check failures - Revert accrueInterestPublic macroMigrated to false since the function does not exist as a separate entry point in MacroSlice.lean (the check scripts enforce name-level correspondence) - Add test_uniquify_yul_shadows.py to satisfy script-test-pairs check Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Add toUint128 overflow checks, callback invocations, and complete macro migration - Add uint128 overflow guards (require <= 2^128-1) before all packed-uint128 field writes in supply, borrow, supplyCollateral, and accrueInterest - Add callback invocations via ecmDo for onMorphoSupply, onMorphoRepay, onMorphoSupplyCollateral, onMorphoLiquidate, and onMorphoFlashLoan - Mark accrueInterestPublic as macro-migrated (maps to accrueInterest via macroAlias); all 18/18 obligations now macro-migrated - Add macroAlias support to check_spec_correspondence.py and check_semantic_bridge_obligations.py for operations that share a MacroSlice function under a different name - Update SemanticBridgeReadiness.lean proofs: 18/18 migrated, 0 pending - Update EQUIVALENCE_OBLIGATIONS.md: zero remaining blockers Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Fix CI: inline uint128Max, remove ecmDo callbacks, fix duplicate variable - Replace uint128Max references with inline literal (macro doesn't resolve external defs) - Remove ecmDo callback invocations (elaboration function not implemented in current Verity) - Revert callback obligation texts to original wording - Fix duplicate newTotalBorrowAssets binding in borrow function Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Fix review issues: event indexed fields, alias-aware coverage, Yul shadow rewrites - Set correct indexed/unindexed event param kinds in Generated.lean to match Solidity EventsLib.sol (P1: preserves ABI topic/data layout) - Make check_primitive_coverage.py alias-aware so macroAlias operations (e.g. accrueInterestPublic → accrueInterest) resolve correctly (P2) - Fix uniquify_yul_shadows.py: limit brace scope tracking to before the let declaration, and rewrite same-line references after renamed declarations (P2+Medium) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Drop manual SupportedStmtList witnesses, delegate Links 2+3 to Verity The verity_contract macro generates code exclusively from supported patterns, so SupportedStmtList/SupportedSpec witnesses should be constructive — produced by the macro, not proven manually per-contract. This commit removes the manual witness files and makes the trust assumption explicit across all surfaces. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Add constructor to Verity contract for owner initialization The verity_contract macro fully supports constructors. Add a constructor that takes initialOwner and stores it via setStorageAddr, matching the original Morpho Blue constructor behavior. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Optimize CI: upload Lean workspace artifact, reuse in downstream jobs Inspired by lfglabs-dev/verity#1647. Instead of each downstream job rebuilding from cache, verity-proofs now uploads the verified .lake workspace as an artifact. verity-compiler-artifacts downloads it directly, eliminating redundant Lean compilation. Also save the Lean/Lake cache only on master to avoid cache pollution from PR branches. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 42d74feda7
ℹ️ 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".
| raw = _extract_top_level_job_value(extract_job_body(workflow_text, job, workflow_path), "timeout-minutes") | ||
| if raw is None: | ||
| continue | ||
| timeouts[job] = int(raw) |
There was a problem hiding this comment.
timeout-minutes values
Once this workflow lands on the branch being inspected (for example, pushes to main, or PRs after main has this commit), client.get_file_text() will read jobs whose timeout-minutes are expressions such as ${{ fromJSON(...) }}. Converting that string with int(raw) raises ValueError, so the new timeout-watchdog job fails before it can emit any warning on every such run.
Useful? React with 👍 / 👎.
| payload = self.get_json( | ||
| f"/actions/workflows/{workflow}/runs", | ||
| {"branch": branch, "status": "completed", "per_page": limit}, | ||
| ) |
There was a problem hiding this comment.
workflow_dispatch clean builds out of watchdog data
If someone runs verify.yml via workflow_dispatch with clean_build=true, later normal runs on the same branch will still pull that run into the sample set here because list_workflow_runs() only filters by branch and status. Those manual clean builds intentionally have larger timeouts than the default path (for example build is 60 minutes instead of 35), so their durations can be counted as "risky" against the normal budget and produce misleading timeout-trend warnings until they age out of the window.
Useful? React with 👍 / 👎.
1 participant
Summary
.lakecache produced earlier in the same workflow run and shardmacro-fuzzto reduce timeout pressuremake checkTesting
python3 -m unittest -v scripts.test_generate_verify_sync_spec scripts.test_ci_timeout_watchdogmake checklake buildpython3 scripts/ci_timeout_watchdog.py --repo lfglabs-dev/verity --workflow verify.yml --branch mainenv MACRO_FUZZ_SHARD_COUNT=4 MACRO_FUZZ_SHARD_INDEX=0 lake exe macro-roundtrip-fuzzlocally; it entered a cold dependency rebuild and did not finish within the working windowNote
Medium Risk
Medium risk because it significantly restructures CI caching/artifact flow and job dependencies, which could cause cache misses, stale artifacts, or unexpected rebuilds/timeouts if misconfigured. No production/runtime code paths are affected beyond CI and the fuzz harness sharding inputs.
Overview
Stabilizes
verify.ymlby reducing redundant Lean rebuilds and splitting long-running work across jobs/shards. Thesetup-leancomposite action now supports sticky disks (elan,.lake/packages, optional.lake/build), configurable cache keys/restore fallbacks, and an opt-out for cache restore; it also skipslake exe cache getwhen dependencies are already hydrated.Verify workflow changes: adds a
workflow_dispatchclean build mode (disables sticky disks/cache restore and increases timeouts), restores the exact.lakecache saved earlier in the same run, and packages/uploads prepared.lake/buildstate so downstream jobs (build-audits, compiler steps, macro-fuzz prep) can reuse it.macro-fuzzis split into aprepare-macro-fuzzbuild stage and a 4-shard matrix run usingMACRO_FUZZ_SHARD_INDEX/COUNT.Workflow hygiene tooling: introduces
scripts/ci_timeout_watchdog.py(newtimeout-watchdogjob) to warn when recent runs approach job timeouts, and replaces the hand-editedverify_sync_spec.jsonwith a generated artifact (verify_sync_spec_source.py+generate_verify_sync_spec.py) enforced viamake check;check_verify_sync.pyis updated to load the Python spec and to better parse YAML block scalars and multi-job compiler expectations.Written by Cursor Bugbot for commit 42d74fe. This will update automatically on new commits. Configure here.