Skip to content

tri lanes: a loop's lanes, each judged; red, conflicting and stale lanes are alarms (Closes #8622) - #8623

Merged
gHashTag merged 1 commit into
masterfrom
tri-lanes
Oct 10, 2026
Merged

gHashTag merged 1 commit into
masterfrom
tri-lanes

Conversation

@gHashTag

Copy link
Copy Markdown
Owner

Closes #8622

Night-loop tooling (ledger gHashTag/trios#1729, item 10). Every tick the loop checked its lanes by hand: the open PRs into actors-next-2, each PR's checks, the worktrees of the shared clone, and how long each lane had been quiet. The ledger names the anomalies to look for: a red PR, a stale agent (no change in 45 min), and a lane that conflicts with its base.

What

tri lanes [--repo trios] [--base actors-next-2] [--clone <path>] [--dir <prefix>] [--stale 45]

It prints two kinds of row:

  • One row per open PR into the base. The row gives pr= branch= draft= merge= checks= age_min= worktree= and a verdict.
    • checks is the PR's statusCheckRollup, read as green, pending or RED.
    • age_min counts minutes since the later of two times: the PR's updatedAt and its local branch's last commit.
    • worktree is the lane worktree checked out on the PR's head branch.
  • One row per lane worktree with no open PR: worktree= branch= age_min= and a verdict.

Verdicts:

Verdict Meaning Alarm
RED a check failed (a cancelled run counts) yes
CONFLICT mergeStateStatus DIRTY yes
STALE no commit or push for --stale minutes yes
READY checks green, CLEAN no
PENDING checks running no
BEHIND rebase it no
BLOCKED a rule of the base holds it no
NO PR worktree with no open PR no
MERGED the worktree's branch was merged into the base: a finished lane, the worktree can go no
DETACHED on no branch, not a lane no

Exit codes: 0 when nothing raises an alarm, 1 on an alarm, 2 when gh gave no PR list.

Where the rules live

specs/tri/lanes/lanes.t27 holds the rules:

  • the defaults, including the ledger's 45 minutes;
  • which texts are read: gh pretty-printed, git's worktree porcelain, for-each-ref, and gh's compact list of merged heads;
  • how a check rollup is judged (CheckRun and StatusContext words);
  • the UTC parse (days_from_civil);
  • branch matching by whole name, so queen-drain is not queen-drain-bound;
  • which worktrees are lanes: the clone itself is not one, and --dir is a path prefix;
  • the verdicts and the exit code.

The line readers are imported from specs/tri/lab/receipt.t27. gen/rust/tri/lanes/lanes.rs is the spec's t27c gen-rust output. cmd_lanes is glue: gh, git, print.

Evidence

  • t27c test-report specs/tri/lanes/lanes.t27: 8 tests, 8 pass, 0 vacuous. Seal saved. The test fixtures are gh's real answer for trios PRs Wave Loop 874 — module-scope [567][2]^6 Pt non-power-of-two outer-dimension array-of-struct variable from call with indexed signed writes #1696 and W82 R-PROXY: SSRF, path traversal, data race, duplicated headers (HIGH) #958 (shortened) and the porcelain of the loop's clone. The UTC values were checked against Python's calendar.timegm.
  • Run on the loop's clone of trios, against --base actors-next: lanes 1-9 read merged: a finished lane, its worktree can go, and the five fresh lanes read no PR yet. Exit 0.
  • The same clone against trios main (paths shortened):
    pr=1696 branch=docs/actors-not-threads draft=false merge=BLOCKED checks=green age_min=2650 worktree=  STALE: no commit or push for the stale minutes
    pr=1674 branch=golden-bridge-p1-bibliography draft=false merge=BEHIND checks=RED age_min=11170 worktree=  RED: a check failed
    pr=958 branch=feat/trios-phd-no-image-train draft=false merge=DIRTY checks=RED age_min=11424 worktree=  RED: a check failed
    ...
    worktree=$S/w/lane-drain branch=queen-drain-bound age_min=29  no PR yet
    worktree=$S/w/qbase branch= age_min=?  detached: on no branch, not a lane
    exit 1: a lane is RED, in CONFLICT or STALE
    
  • With a repository that does not exist, gh prints nothing and the exit is 2.
  • Today, with the default base, there are no open PRs into actors-next-2, so only worktree rows print.

Negative controls

Each control is one edit to a copy of the spec. Every one fails a test by name, except the last, which fails the invariant:

Control FAILs
a cancelled check is not a failure the_checks_are_judged
a running check reads as green the_checks_are_judged, the_lanes_are_judged
checks read at the PR's indent (a title is a check) the_checks_are_judged, the_lanes_are_judged
a conflict outranks a red check the_lanes_are_judged
stale one minute late (> for >=) the_lanes_are_judged
an unknown age is stale the_lanes_are_judged
BEHIND reads as ready the_lanes_are_judged
a merged lane is stale the_lanes_are_judged
merged matched by prefix a_merged_lane_is_its_own_branch
a branch time matched by prefix a_branch_time_is_its_own
the clone itself is a lane 4 tests
--dir ignored the_worktrees_are_read
a leap-day date off by one utc_times_are_read
a time without its Z is read utc_times_are_read
no PR list is a quiet exit alarms_exits_and_words
the stale default drifts from 45 the invariant (does not compile)

Census moved

The fetches census moved: lines naming --limit went from 76 to 78, and lines refused as not a fetch went from 41 to 43. It is re-blessed in tools/census/fetches.txt.

The two new lines are cmd_lanes' gh pr list --limit calls. The matcher refuses them because the bound is a spec constant (lanes::PR_LIMIT, 200), not a literal. Both calls are still bounded: a base with more than 200 merged lanes would show the older ones as STALE. That failure is noisy, not silent.

Foreign lines

  • cli/tri/src/main.rs: +40 lines of glue, at the cap.
  • scripts/gen_w320.py: -45 lines, deleted. It is a one-off wave script that nothing runs, and the lab verifies its port specs/port/scripts/gen_w320.t27.

Net -5. check_all (--ci) and check_budget pass locally.

Known limit

The ledger's rule is "no file change in 45 min", but this command reads commits and pushes, not uncommitted edits in a worktree. A lane that edits for 45 minutes without committing therefore reads as STALE.

🤖 Generated with Claude Code

…nes are alarms (Closes #8622)

`tri lanes [--repo trios] [--base actors-next-2] [--clone <path>] [--dir <prefix>] [--stale 45]`
prints one row per open pull request into the base (merge state, checks green / pending / RED, age
in minutes, its local worktree) and one per lane worktree of the clone with no open pull request.
RED, CONFLICT and STALE are the night ledger's anomalies (gHashTag/trios#1729) and exit 1; READY,
PENDING, BEHIND, BLOCKED, NO PR, MERGED (the branch was merged into the base: a finished lane) and
DETACHED (on no branch: not a lane) do not. No PR list from gh exits 2.

Every rule is specs/tri/lanes/lanes.t27 (8 tests, 0 FAIL, 0 vacuous; 16 negative controls, each
FAILs by name or by the invariant): the defaults (the ledger's 45 minutes), how a check rollup is
judged (a cancelled run is red: it did not run on the head), how GitHub's UTC time is read
(days_from_civil), how a branch's last commit is found by its whole name, which worktrees are lanes,
the verdicts and the exit. The line readers are imported from specs/tri/lab/receipt.t27.
gen/rust/tri/lanes/lanes.rs is its t27c gen-rust; cmd_lanes is glue: gh, git, print.

On the loop's clone: against --base actors-next, lanes 1-9 read MERGED and the five fresh lanes NO
PR, exit 0; against trios main, 3 pull requests read RED and 4 STALE, exit 1.

Census moved: fetches, lines naming --limit 76 -> 78, refused as not a fetch 41 -> 43 (re-blessed
in tools/census/fetches.txt). The two are cmd_lanes' `gh pr list --limit` calls; the matcher refuses
them because the bound is a spec constant (lanes::PR_LIMIT, 200), not a literal. Both ARE bounded: a
base with more than 200 merged lanes would show the older ones STALE (noisy, not silent).

Hand-written foreign lines: +40 (cli/tri/src/main.rs), -45 (scripts/gen_w320.py, a one-off wave
script whose port specs/port/scripts/gen_w320.t27 the lab verifies). Net -5.

Closes #8622

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag
gHashTag enabled auto-merge (squash) October 10, 2026 13:55
@github-actions

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-10 13:55:31 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 49
PRs with All Checks Green 1
READY 0
FAILING 49
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 49 + 0 + 0 = 49, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=96f3a5f9cbd0 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag
gHashTag merged commit a162313 into master Oct 10, 2026
24 of 29 checks passed
gHashTag added a commit that referenced this pull request Oct 10, 2026
…phan reaches renum.rs again (Closes #8628) (#8631)

#8601, #8614 and #8623 mounted their gen-rust modules on one line each,
`#[path = ...] #[allow(...)] mod x; // ...`. rustc reads that. tri mods orphan
(modreach.rs edges_from) takes a line starting with `#[path` as an attribute
alone and hands the path to the next `mod` line, `mod renum;`, so renum.rs (994
lines, 26 tests) read as orphaned and "Orphaned modules" went red on master
(cli/tri: orphaned rose 0 -> 1). The three mounts are now two lines each, as
the rest of main.rs writes them; tri mods orphan --gate: ORPHAN CEILING: CLEAN.
Joining the last three lines of cmd_lab and of cmd_actors pays for them:
main.rs +8 -9.

Duplicate bodies (tools/dupe_scan.py): lanes.t27 pr_end was receipt.t27's
object_end written again and now calls it (8 tests pass, reseal). receipt.t27
line_end is report.t27's body and stays a ledgered copy (`line_end 2`):
importing it makes every importer of receipt.t27 inline report.t27 as well, and
their two V_BLOCKED (3 and 2) drop out, so metrics.t27 stops compiling -- a gen
closure defect, filed as #8630. The scan's remaining errors, bits and clear,
were red before these PRs.

Closes #8628

Co-authored-by: Claude <claude@anthropic.com>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

tri lanes: a loop's lanes (open PRs into its base, its worktrees), each judged; red, conflicting and stale lanes are alarms

2 participants