Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 90 additions & 0 deletions .claude/skills/ci-gates/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -12384,3 +12384,93 @@ The rule that follows is narrow and mechanical: a figure describing the state AF
change is taken as the LAST action before the commit, from the tree that is committed,
and is written with that commit's sha. Any earlier reading describes a different tree,
however few minutes earlier it was.


## 471. A lesson written down four times, and the command run anyway

`cargo fmt -p t27c`, on a branch holding a two-file change, came back with **155
tracked files modified**. `cargo fmt --all` on a one-file change: **165 dirty, 164
of them collateral**. Both sets include `bootstrap/src/compiler.rs`, which is
M5-frozen — `build.rs` refuses to build unless `FROZEN_HASH` matches its sha256 —
so the formatter turns a real gate red while tidying a file in another crate.

The diagnosis takes one grep and it is already in this file. §72 has it, with
150 files, the same frozen file, and the same command:
`grep -rn "cargo fmt" .github/workflows/` returns nothing. §381 has the mod-graph
half. §407 says format only your own hunks. §447 has the forty sorted
`mod` lines.

**Four sections, and I ran it anyway.** That is the finding. The failure was not
that the knowledge was missing; it was that nothing stood between the habit and
the command, and a fifth paragraph would stand exactly as far from it as the other
four.

So the section ends in a binary rather than in advice. `tri fmt` takes the dirty
set, runs the formatter, and restores every file that was **clean before and is
dirty after**. Clean-before means identical to HEAD, so the restore loses nothing,
and that is the whole reason the dirty set is taken first rather than derived from
a base ref. Measured on this repository: 165 dirty, 1 kept, 164 restored,
`FROZEN_HASH` intact afterwards.

Two things it does not do, both said out loud rather than discovered later. A
concurrent process sharing the same worktree can dirty a file between the two
`git status` calls and have it reverted; the window is the formatter's runtime,
and every restored path is printed for that reason. And untracked files are never
restored — they are yours by construction — which is also why the summary counts
"modified tracked files you kept" and not "files formatted", a larger number
this command is in no position to state.

And the limitation the FIRST use exposed, which is §447 arriving inside the
new tool: the command protects every file except the one you edited. `cargo fmt`
sorted the `mod` declarations at the top of `cli/tri/src/main.rs` while formatting
the thirteen lines this command added to it, and a 13-insertion diff was reported
as **31 insertions and 18 deletions**. `tri fmt` kept that file because it was
yours, which is correct and is also exactly why it cannot help there. The shape of
the diff gave it away, as it did in §447: deletions on a pure addition.

The general form: **when a rule has been written down repeatedly and broken
anyway, the next unit of work is an executable, not another paragraph.** The count
of prior sections is the evidence for that, and it is worth taking before writing
the new one — `grep -c` on the file you are about to append to. And write down
what the executable does not reach, at the moment you find out, rather than
leaving it for whoever trusts it next.


## 472. The machine that could not answer, and the population nobody asked

`t27c corpus` was given an UNRESOLVED channel: a tool that could not be spawned, a
capture file that could not be written, and a child killed by a signal are not
rejections, and the run refuses rather than publishing them as zeros. Six tests
pinned it. The module docstring stated the rule as a universal — *a run that
produced no usable numbers must not be able to exit 0.*

The sentence was false for the simplest input in its own space:

```
$ t27c corpus --specs-dir <an empty directory> --json
{"specs":0,"zig_build":0,...,"verilog_build":0,...}
$ echo $?
0
```

The constant 0 in the format of a measurement — the exact thing the refusal exists
to prevent — arriving through the one door the refusal does not watch. A
**mistyped** `--specs-dir` reaches it identically, because the walk opens the tree
with `read_dir(..).else { continue }`, so a path that does not exist is
indistinguishable from a tree with no specs in it.

Two classes produce no numbers: **the machine could not answer**, and **nothing was
asked**. All six tests fed a non-empty tree, so every one of them lived in the
first class, while the docstring quantified over both.

It was found by running the binary against an empty directory. The reading had
already been done — twice, by two agents — and both wrote the universal down as
though the guard implied it. A docstring that states a universal is a claim about a
**population**, and the population's edges are cheap: empty, absent, one.

The mutation is the other half. Deleting the new empty-population guard kills the
new test; keeping the guard but re-adding a single acceptance key to its refusal
JSON kills it too; and **neither moves any other test in the file**. That last
clause is not decoration — it is the measurement that the six existing tests never
covered this branch, which is the same fact the docstring got wrong, restated in a
form that fails if someone deletes it.
229 changes: 229 additions & 0 deletions cli/tri/src/fmtmine.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,229 @@
//! `tri fmt` -- run the formatter without authoring 155 files you did not touch.
//!
//! `cargo fmt -p t27c`, on a branch holding a TWO-file change, came back with
//! **155 tracked files modified**: every `bootstrap/src/host/*.rs`, seventy test
//! files, `build.rs`, and `bootstrap/src/compiler.rs` -- which is M5-frozen, with
//! `bootstrap/stage0/FROZEN_HASH` holding its sha256, so the freeze gate goes red
//! the moment the formatter touches it.
//!
//! Nothing is wrong with the formatter. This repository has never been through
//! it, and one grep says why: no workflow invokes `cargo fmt`, so nothing keeps
//! master formatted and the first person to run it locally does not tidy their
//! own change -- they author a 155-file diff on top of it.
//!
//! This is not a new finding. The skill records it in &sect;72 (150 files, the
//! same frozen file, the same grep), &sect;381, &sect;407 and &sect;447. It was
//! recorded four times and the command was still run. Prose that has failed four
//! times does not get a fifth paragraph; it gets a binary that does the safe
//! thing by default.
//!
//! So: note what is dirty, format, and put back everything that was CLEAN before
//! and is dirty after. A file that was clean before is identical to HEAD, so
//! restoring it loses nothing -- which is the whole reason the revert is safe and
//! the reason the dirty set is taken first rather than derived from a base ref.
//!
//! WHAT THIS DOES NOT COVER, FIRST. The file you are editing. It is dirty before,
//! so it is kept -- correctly -- and the formatter's rewrite of the REST of it is
//! kept with it. Formatting the thirteen lines this command added to `main.rs`
//! also sorted that file's `mod` declarations, turning a 13-insertion diff into
//! 31 insertions and 18 deletions. The tell is the shape: deletions on a pure
//! addition. There is no fix inside this command; the fix is `git checkout --`
//! that one file and re-apply the hunks.
//!
//! WHAT THIS DOES NOT COVER, SECOND. Between the first `git status` and the second, a
//! concurrent process sharing this worktree can dirty a file that this command
//! will then revert. The window is the formatter's runtime. Every reverted path
//! is printed for that reason. Separate worktrees are unaffected: `git checkout`
//! is per-worktree, unlike `git stash`, which is not.

use anyhow::{bail, Result};
use std::collections::BTreeSet;
use std::path::Path;
use std::process::Command;

/// Files the formatter dirtied that were clean when it started.
///
/// Set subtraction, not string work: `after` and `before` come from the same
/// command with the same quoting, and the only question is membership.
pub fn collateral(before: &BTreeSet<String>, after: &BTreeSet<String>) -> Vec<String> {
after.difference(before).cloned().collect()
}

/// `true` when some workflow actually invokes the formatter.
///
/// The point of asking: if nothing runs it, an unformatted tree is the
/// repository's normal state and reformatting it is not a fix. `--check` counts
/// -- a gate that only verifies is still a gate that keeps master clean.
pub fn any_workflow_runs_fmt(workflows: &[String]) -> bool {
workflows.iter().any(|w| {
w.lines()
.filter(|l| !l.trim_start().starts_with('#'))
.any(|l| l.contains("cargo fmt") || l.contains("rustfmt"))
})
}

fn dirty(root: &Path) -> Result<BTreeSet<String>> {
let out = Command::new("git")
.args(["status", "--porcelain", "--untracked-files=no"])
.current_dir(root)
.output()?;
if !out.status.success() {
bail!("git status failed in {}", root.display());
}
Ok(parse_porcelain(&String::from_utf8_lossy(&out.stdout)))
}

/// Porcelain v1: two status columns, a space, then the path. A rename carries
/// `old -> new` and the NEW name is the one on disk.
pub fn parse_porcelain(s: &str) -> BTreeSet<String> {
s.lines()
.filter(|l| l.len() > 3)
.map(|l| {
let p = &l[3..];
match p.split_once(" -> ") {
Some((_, new)) => new.to_string(),
None => p.to_string(),
}
})
.collect()
}

fn workflow_texts(root: &Path) -> Vec<String> {
let dir = root.join(".github/workflows");
let Ok(rd) = std::fs::read_dir(&dir) else {
return Vec::new();
};
rd.flatten()
.filter_map(|e| std::fs::read_to_string(e.path()).ok())
.collect()
}

pub fn run(root: &Path, package: Option<&str>, dry: bool) -> Result<()> {
let gated = any_workflow_runs_fmt(&workflow_texts(root));
println!(
" a workflow runs the formatter {}",
if gated {
"yes -- master is kept formatted"
} else {
"NO -- an unformatted tree is this repository's normal state"
}
);

let before = dirty(root)?;
println!(" dirty before {}", before.len());
if dry {
println!(" --dry-run: the formatter was not run.");
return Ok(());
}

let mut cmd = Command::new("cargo");
cmd.arg("fmt");
match package {
Some(p) => {
cmd.args(["-p", p]);
}
None => {
cmd.arg("--all");
}
}
let st = cmd.current_dir(root).status()?;
if !st.success() {
bail!("cargo fmt exited {:?}", st.code());
}

let after = dirty(root)?;
let extra = collateral(&before, &after);
println!(
" dirty after {} (+{} the formatter added)",
after.len(),
extra.len()
);

for p in &extra {
let st = Command::new("git")
.args(["checkout", "--", p])
.current_dir(root)
.status()?;
if !st.success() {
bail!("could not restore {p}");
}
println!(" restored {p}");
}

let left = dirty(root)?;
if left != before {
bail!(
"the tree did not come back to the set it started with: {} before, {} now",
before.len(),
left.len()
);
}
// Says what it counted. `before.len()` is TRACKED files you had already
// modified -- not "files formatted", which is larger: an untracked file is
// yours by construction, never appears in `--untracked-files=no`, and is
// therefore kept without ever being counted here.
println!(
" kept your {} modified tracked file(s) and every untracked one; {} the formatter had also rewritten are back at HEAD.",
before.len(),
extra.len()
);
Ok(())
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn only_files_that_were_clean_before_are_restored() {
let before: BTreeSet<String> = ["a.rs", "b.rs"].iter().map(|s| s.to_string()).collect();
let after: BTreeSet<String> = ["a.rs", "b.rs", "c.rs", "d.rs"]
.iter()
.map(|s| s.to_string())
.collect();
assert_eq!(collateral(&before, &after), vec!["c.rs", "d.rs"]);
// The load-bearing direction: a file you were already editing is never
// restored, however the formatter rewrote it.
assert!(!collateral(&before, &after).contains(&"a.rs".to_string()));
}

#[test]
fn a_formatter_that_touched_nothing_new_restores_nothing() {
let s: BTreeSet<String> = ["a.rs"].iter().map(|x| x.to_string()).collect();
assert!(collateral(&s, &s).is_empty());
}

#[test]
fn porcelain_paths_survive_the_status_columns_and_a_rename() {
let got =
parse_porcelain(" M bootstrap/src/service.rs\n?? new.rs\nR old.rs -> new/one.rs\n");
assert!(got.contains("bootstrap/src/service.rs"));
assert!(got.contains("new.rs"));
// The NEW name is the file on disk; restoring the old one would not
// undo the rename and `git checkout -- old.rs` would fail outright.
assert!(got.contains("new/one.rs"));
assert!(!got.contains("old.rs -> new/one.rs"));
}

#[test]
fn a_repository_with_no_workflow_that_formats_says_so() {
assert!(!any_workflow_runs_fmt(&[
"jobs:\n build:\n steps:\n - run: cargo test --all\n".to_string()
]));
assert!(any_workflow_runs_fmt(&[
" - run: cargo fmt --all -- --check\n".to_string()
]));
assert!(any_workflow_runs_fmt(&[
" - run: rustfmt --check x.rs\n".to_string()
]));
}

#[test]
fn a_commented_out_formatter_step_is_not_a_gate() {
// This is the difference between "the gate exists" and "the gate ran":
// a disabled step reads as the string either way.
assert!(!any_workflow_runs_fmt(&[
" # - run: cargo fmt --all -- --check\n".to_string()
]));
}
}
13 changes: 13 additions & 0 deletions cli/tri/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ mod competitors;
mod issues;
mod cibase;
mod fleet;
mod fmtmine;
mod fpga;
mod elab;
mod modreach;
Expand Down Expand Up @@ -205,6 +206,15 @@ enum Commands {
action: abandoned::AbandonedCmd,
},
/// Type names with more than one definition in the spec tree.
/// Run the formatter and restore every file it rewrote that you had not touched.
Fmt {
/// One package instead of the whole workspace.
#[arg(short, long)]
package: Option<String>,
/// Report what is dirty and whether a workflow formats, and stop.
#[arg(long)]
dry_run: bool,
},
Types {
#[command(subcommand)]
action: types_dup::TypesCmd,
Expand Down Expand Up @@ -951,6 +961,9 @@ fn main() -> Result<()> {
Commands::Elab { action } => elab::run(action)?,
Commands::Rtl { action } => rtl::run(action)?,
Commands::Abandoned { action } => abandoned::run(action)?,
Commands::Fmt { package, dry_run } => {
fmtmine::run(&find_trinity_root()?, package.as_deref(), *dry_run)?
}
Commands::Types { action } => types_dup::run(action)?,
Commands::Quantifiers { action } => quant::run(action)?,
Commands::Orphaned { action } => orphaned::run(action)?,
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
# NOW -- A rule written down four times becomes a binary (2026-09-04)

## `tri fmt` runs the formatter and puts back what was not yours

- `cargo fmt --all` on a one-file change leaves **165 files dirty**, 164 of them
collateral, including `bootstrap/src/compiler.rs` -- M5-frozen, so the freeze
gate goes red as a side effect of tidying another crate. An earlier run with
`-p t27c` produced 155.
- Nothing keeps this tree formatted: no workflow invokes `cargo fmt` or
`rustfmt`, so an unformatted tree is the repository's normal state and running
the formatter is not a fix.
- `tri fmt` takes the dirty set, runs the formatter, and restores every file that
was clean before and is dirty after. Clean-before means identical to HEAD, so
the restore loses nothing. Measured here: 165 dirty, 1 kept, 164 restored,
`FROZEN_HASH` intact afterwards. Every restored path is printed.
- The reason this is a command and not a note: the skill already recorded it four
times (sections 72, 381, 407, 447) and the command was run anyway this week.
- The limitation the first use exposed, now stated in both the section and the
module: it protects every file except the one you edited. Formatting the
thirteen added lines of `main.rs` also sorted that file's `mod` declarations
and reported 31 insertions with 18 deletions.
Loading