You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
ci(nightly): rebalance the route model's TLA+ legs - #8583
Two of today's Nightly TLA+ legs for the route model failed (run):
TLA+ (route behind) named rs/moq-net/verify/route/BehindDear.cfg, which moq-dev/moq#8541 deleted, so sh/tla.sh found no config.
TLA+ (route) was cancelled at its 180-minute limit. On 4 workers it took Blind 23, Dead 26, Early 46, and Lag 19 minutes, and LagWide had passed 68 when the job was cancelled; Loop and Twice never ran.
Summary
Early.cfg and LagWide.cfg each get their own leg (route early, route wide).
RouteHandoff.cfg and Ring.cfg rejoin the route leg; each took about 6 minutes as its own job today, including setup.
The route behind leg is gone.
The route leg should now take about 95 minutes, estimated from today's times plus local runs of Loop and Twice.
Public API: none. Wire: none.
Caused by
moq-dev/moq#8541 - deleted BehindDear.cfg and made the route configs larger without updating the Nightly matrix
Checks
just check: passes.
Models
Size: XS
Implementer: Claude Code, Opus 5.5, high effort
Score: 9/10, The revised matrix uses existing configs, preserves complete model coverage through complementary path exclusions, and removes the deleted config's dedicated job, though runtime timings were not independently verified.
The `route behind` leg named BehindDear.cfg, which #8541 deleted, so it
failed. The `route` leg ran past its 180-minute limit: Early.cfg (46
minutes on 4 workers) and LagWide.cfg (over 68) now get a runner each,
while RouteHandoff.cfg and Ring.cfg, about 5 minutes each, rejoin it.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The reason will be displayed to describe this comment to others. Learn more.
✅ No new issues found.
Reviewed changes: the single-file change to the Nightly TLA+ matrix in .github/workflows/nightly.yml.
New legs: route early and route wide run Early.cfg and LagWide.cfg, each in its own job.
Removed legs: route triangle, route behind and route ring are gone. route behind pointed at the deleted BehindDear.cfg.
route leg: it now excludes only Early.cfg and LagWide.cfg, so RouteHandoff.cfg, Ring.cfg and any new route config are picked up.
The two exclusions are complementary to the two dedicated legs, so every config in rs/moq-net/verify/route/ runs exactly once. The route leg's estimated ~95 minutes and the 180-minute timeout-minutes leave headroom. I did not re-measure any timings.
No actionable comments were generated in the recent review.
Walkthrough
The nightly TLA+ matrix now assigns Early.cfg and LagWide.cfg to separate route legs. The general route leg excludes these two configurations. The comments describe the updated allocation.
Merge Risk: Minimal · up to 2633a
This change rebalances nightly model-checking jobs and does not affect runtime behavior or public APIs. No actionable merge-blocking risk remains.
Pre-merge checks: 4
Check name
Status
Explanation
Title check
The title names the main change: the nightly CI workflow's route-model TLA+ legs are rebalanced. The diff moves Early.cfg and LagWide.cfg into their own legs, moves RouteHandoff.cfg and Ring.cfg back …
Description check
The description matches the changeset. It explains why the route legs failed, which are the deleted BehindDear.cfg reference and the 180-minute timeout. It lists the new route early and route wide leg…
Linked Issues check
Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check
Check skipped because no linked issues were found for this pull request.
Full details: Title check
Explanation
The title names the main change: the nightly CI workflow's route-model TLA+ legs are rebalanced. The diff moves Early.cfg and LagWide.cfg into their own legs, moves RouteHandoff.cfg and Ring.cfg back into the route leg, and removes the route behind leg. The title is specific and matches the changeset.
Full details: Description check
Explanation
The description matches the changeset. It explains why the route legs failed, which are the deleted BehindDear.cfg reference and the 180-minute timeout. It lists the new route early and route wide legs, the reassigned RouteHandoff.cfg and Ring.cfg, and the removed route behind leg. It also gives the verification status.
Finishing Touches
Simplify code
Commit to this branch
Create a new PR
Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
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.
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: CHILL
Plan: Advanced
Run ID: 16212a70-6c20-485f-9054-0812e9c7f052
Commits
Reviewing files that changed from the base of the PR and between 36931c3 and 2633a55.
Files selected for processing: 1
.github/workflows/nightly.yml
Included review availability: This review used your included allowance. Your plan provides up to 4 included reviews per hour; 3 remain after this review.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
![pullfrog[bot]](https://avatars.githubusercontent.com/in/1768019?s=60&v=4){kind=small}
Two of today's Nightly TLA+ legs for the route model failed (run):
TLA+ (route behind)namedrs/moq-net/verify/route/BehindDear.cfg, which moq-dev/moq#8541 deleted, sosh/tla.shfound no config.TLA+ (route)was cancelled at its 180-minute limit. On 4 workers it took Blind 23, Dead 26, Early 46, and Lag 19 minutes, and LagWide had passed 68 when the job was cancelled; Loop and Twice never ran.Summary
Early.cfgandLagWide.cfgeach get their own leg (route early,route wide).RouteHandoff.cfgandRing.cfgrejoin therouteleg; each took about 6 minutes as its own job today, including setup.route behindleg is gone.routeleg should now take about 95 minutes, estimated from today's times plus local runs of Loop and Twice.Public API: none. Wire: none.
Caused by
BehindDear.cfgand made the route configs larger without updating the Nightly matrixChecks
just check: passes.Models
Size: XS
Implementer: Claude Code, Opus 5.5, high effort
🤖 Generated with Claude Code
(Written by Claude Opus 5.5 with high)
Review
Rewritten by
quest reviewafter each round.01a1d14e-c60b-7aa3-8f13-993812841e71, round 1The revised matrix uses existing configs, preserves complete model coverage through complementary path exclusions, and removes the deleted config's dedicated job, though runtime timings were not independently verified.