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

.trinity/seals/lanes_TriLanes.json

@@ -0,0 +1,32 @@
+{
+  "built_by": "t27c-bootstrap@0.5.2+b8781fb75",
+  "closure": [
+    {
+      "spec": "specs/tri/lab/receipt.t27",
+      "spec_hash": "sha256:00d9eec8d7be84dde596c9990b3a5574de24aff9f7a94579fc620eb585712441"
+    }
+  ],
+  "config": "gen=c,rust,verilog,zig;tests=zig",
+  "gen_hash_c": "sha256:f08bc5e43e2b648ebf9456020e086df45592fa4186cafe1002e34714df6c015f",
+  "gen_hash_rust": "sha256:f459ec369d21af88cb41113b4c453c930ad514b0a8d10b317b46c3872c06f29c",
+  "gen_hash_verilog": "sha256:379d076d49247e518f1830a17feb71e478a589071494208d9d0c71d651788e99",
+  "gen_hash_zig": "sha256:ef1ebda3983c805a06a7f57ab27489e76d7999949a7d27d6c53449acd3a631d4",
+  "module": "TriLanes",
+  "ring": 12,
+  "seal_schema": 2,
+  "sealed_at": "2026-10-10T13:52:57Z",
+  "sealed_by": "t27c-bootstrap@0.5.2",
+  "spec_hash": "sha256:8b1ff75510259ba9bbaf0a51e619db5f6b48228f31c99c65d3b2db292efa3b21",
+  "spec_path": "specs/tri/lanes/lanes.t27",
+  "tests": {
+    "failed": 0,
+    "failing": [],
+    "forced": false,
+    "passed": 8,
+    "total": 8
+  },
+  "toolchain": {
+    "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d",
+    "zig": "0.16.0"
+  }
+}

cli/tri/src/main.rs

@@ -45,6 +45,7 @@ mod red;
 mod report; // t27c gen-rust of specs/tri/test/report.t27 (#7369): every rule of reading `t27c test-report`
 #[path = "../../../gen/rust/tri/lab/receipt.rs"] #[allow(dead_code, unused_parens)] mod lab; // t27c gen-rust of specs/tri/lab/receipt.t27: every rule of `tri lab receipt`
 #[path = "../../../gen/rust/tri/actors/metrics.rs"] #[allow(dead_code, unused_parens)] mod act; // t27c gen-rust of specs/tri/actors/metrics.t27: every rule of `tri actors`
+#[path = "../../../gen/rust/tri/lanes/lanes.rs"] #[allow(dead_code, unused_parens)] mod lanes; // t27c gen-rust of specs/tri/lanes/lanes.t27: every rule of `tri lanes`
 mod renum;
 mod reseal;
 mod rtl;
@@ -352,6 +353,19 @@ enum Commands {
         #[command(subcommand)]
         action: seals::SealsCmd,
     },
+    /// A loop's lanes: its open pull requests into the base and its worktrees, each judged; a red, conflicting or stale lane is an alarm (rules: specs/tri/lanes/lanes.t27).
+    Lanes {
+        /// The repository: owner/name, or a name of gHashTag's.
+        #[arg(long, default_value = lanes::REPO)] repo: String,
+        /// The branch the lanes merge into.
+        #[arg(long, default_value = lanes::BASE)] base: String,
+        /// The git clone whose worktrees are the lanes.
+        #[arg(long, default_value = ".")] clone: String,
+        /// Only the clone's worktrees whose path starts with this are lanes.
+        #[arg(long, default_value = "")] dir: String,
+        /// Minutes without a commit or push after which a lane is stale.
+        #[arg(long, default_value_t = lanes::STALE_MINUTES)] stale: u64,
+    },
     /// Pure-Rust ports of repository commit / push gates.
     Hooks {
         #[command(subcommand)]
@@ -1229,6 +1243,7 @@ fn main() -> Result<()> {
         Commands::Jumps { action } => jumps::run(action)?,
         Commands::Vsim { action } => vsim::run(action)?,
         Commands::Seals { action } => seals::run(action)?,
+        Commands::Lanes { repo, base, clone, dir, stale } => std::process::exit(cmd_lanes(repo, base, clone, dir, *stale)? as i32),
         Commands::Hooks { action } => hooks::run(action)?,
         Commands::Lab { specs, sha, .. } => std::process::exit(cmd_lab(specs.as_deref(), sha)? as i32),
         Commands::Actors { url, bound, replay } => std::process::exit(cmd_actors(url, *bound, *replay)? as i32),
@@ -1237,6 +1252,31 @@ fn main() -> Result<()> {
     Ok(())
 }
 
+/// `tri lanes`: gh's open pull requests into the base, the clone's worktrees and branch times, and what specs/tri/lanes/lanes.t27 reads in them.
+fn cmd_lanes(repo: &str, base: &str, clone: &str, dir: &str, stale: u64) -> Result<u8> {
+    fn run(c: &str, a: &[&str]) -> Result<&'static str> { Ok(String::from_utf8_lossy(&Command::new(c).args(a).output()?.stdout).into_owned().leak()) }
+    let full = format!("{}{repo}", if lanes::needs_owner(repo.to_string().leak()) { lanes::OWNER } else { "" });
+    let prs: &'static str = serde_json::from_str::<serde_json::Value>(run("gh", &["pr", "list", "-R", &full, "--base", base, "--state", "open", "--limit", lanes::PR_LIMIT, "--json", lanes::PR_FIELDS])?).ok().and_then(|v| serde_json::to_string_pretty(&v).ok()).unwrap_or_default().leak();
+    let (wts, refs, done) = (run("git", &["-C", clone, "worktree", "list", "--porcelain"])?, run("git", &["-C", clone, "for-each-ref", lanes::REF_FORMAT, "refs/heads"])?, run("gh", &["pr", "list", "-R", &full, "--base", base, "--state", "merged", "--limit", lanes::PR_LIMIT, "--json", lanes::MERGED_FIELDS])?);
+    let (now, dir, mut alarms): (u64, &'static str, u64) = (std::time::SystemTime::now().duration_since(std::time::UNIX_EPOCH)?.as_secs(), dir.to_string().leak(), 0);
+    let age = |a: u64| if lanes::age_known(a) { a.to_string() } else { lanes::UNKNOWN.to_string() };
+    let mut o = lanes::next_pr(prs, 0);
+    while o < prs.len() {
+        let e = lanes::pr_end(prs, o);
+        let w = lanes::worktree_of(wts, dir, prs, o, e);
+        let a = lanes::age_minutes(now, lanes::later(lanes::pr_updated(prs, o, e), lanes::commit_time(refs, wts, w))); let v = lanes::pr_verdict(prs, o, e, a, stale); alarms += lanes::is_alarm(v) as u64;
+        println!("{} checks={} age_min={} worktree={}  {}", (0..lanes::PR_CELLS).map(|k| format!("{}={}", lanes::pr_label(k), &prs[lanes::pr_from(prs, o, e, k)..lanes::pr_to(prs, o, e, k)])).collect::<Vec<_>>().join(" "), lanes::ci_name(lanes::ci(prs, o, e)), age(a), &wts[lanes::path_from(wts, w)..lanes::path_to(wts, w)], lanes::why(v));
+        o = lanes::next_pr(prs, e);
+    }
+    let mut w = lanes::next_worktree(wts, 0, dir);
+    while w < wts.len() {
+        let a = lanes::age_minutes(now, lanes::commit_time(refs, wts, w)); let v = lanes::worktree_verdict(wts, w, a, stale, lanes::merged(done, wts, w));
+        if !lanes::has_pr(prs, wts, w) { alarms += lanes::is_alarm(v) as u64; println!("worktree={} branch={} age_min={}  {}", &wts[lanes::path_from(wts, w)..lanes::path_to(wts, w)], &wts[lanes::branch_from(wts, w)..lanes::branch_to(wts, w)], age(a), lanes::why(v)); }
+        w = lanes::next_worktree(wts, lanes::record_end(wts, w), dir);
+    }
+    let x = lanes::exit_code(!prs.is_empty(), alarms); println!("{}", lanes::exit_why(x)); Ok(x)
+}
+
 fn cmd_serve(addr: &str) -> Result<()> {
     use axum::routing::{get, post};
     use axum::Router;

docs/now/2026-10-10-tri-lanes.md

@@ -0,0 +1,8 @@
+# NOW -- tri lanes: a loop's lanes, each judged; red, conflicting and stale lanes are alarms (2026-10-10)
+
+## specs/tri/lanes/lanes.t27, cli/tri/src/main.rs (Closes #8622; night-loop ledger gHashTag/trios#1729, item 10)
+
+- `tri lanes [--repo trios] [--base actors-next-2] [--clone <path>] [--dir <prefix>] [--stale 45]` prints one row per open PR into the base (merge state, checks green / pending / RED, age, its worktree) and one per lane worktree with no open PR. The verdicts RED, CONFLICT and STALE are the ledger's anomalies and exit 1. A worktree whose branch was merged into the base is MERGED, and a detached one is not a lane. If gh gives no PR list, the exit is 2.
+- Every rule is in the spec (8 tests, 0 FAIL, 0 vacuous; 16 negative controls, each FAILs by name or by the invariant). The age is the minutes since the later of the PR's updatedAt and the local branch's last commit. The ledger says "no file change in 45 min", but this reads commits and pushes, not uncommitted edits.
+- Run on the loop's clone: against `--base actors-next`, lanes 1-9 read MERGED and the five fresh lanes read NO PR, exit 0. Against trios `main`, 3 PRs read RED and 4 read STALE, exit 1.
+- Hand-written foreign lines: `cli/tri/src/main.rs` gains 40 and `scripts/gen_w320.py` loses 45, so net -5. The deleted script's port, `specs/port/scripts/gen_w320.t27`, is verified by the lab.