a73x

ba8d96a0

build: a push to main brings a line about what slowed it down

a73x   2026-08-22 16:12

Commit message
build: a push to main brings a line about what slowed it down

The retro rule lived in a habit, and habits are not enforced. Now the
pre-push hook asks for one before it asks for a green build: cheap
check first, five-minute one after.

It cannot tell an honest line from a space, and does not try. It only
makes sure the moment is not skipped.
.githooks/pre-push
Old New
@@ -1,8 +1,8 @@
1 #!/usr/bin/env bash 1 #!/usr/bin/env bash
2 # 2 #
3 # pre-push — the merge gate. Any push that updates the shared `main` branch must 3 # pre-push — the merge gate. Any push that updates the shared `main` branch must
4 # pass `make ci` first (the same gate CI enforces). This is the guard that was 4 # carry a RETRO.md line and pass `make ci` first (the same gate CI enforces).
5 # missing when work merged to main red. 5 # This is the guard that was missing when work merged to main red.
6 # 6 #
7 # Scope: ONLY pushes that update the remote refs/heads/main are gated. Feature- 7 # Scope: ONLY pushes that update the remote refs/heads/main are gated. Feature-
8 # branch pushes and branch deletions run free. In a genuine emergency, bypass 8 # branch pushes and branch deletions run free. In a genuine emergency, bypass
@@ -17,14 +17,34 @@ zero="0000000000000000000000000000000000000000"
17 # git feeds pre-push one line per ref being pushed: 17 # git feeds pre-push one line per ref being pushed:
18 # <local ref> <local oid> <remote ref> <remote oid> 18 # <local ref> <local oid> <remote ref> <remote oid>
19 gate=0 19 gate=0
20 while read -r _local_ref local_oid remote_ref _remote_oid; do 20 range=""
21 while read -r _local_ref local_oid remote_ref remote_oid; do
21 [ "$remote_ref" = "$protected" ] || continue # not touching main 22 [ "$remote_ref" = "$protected" ] || continue # not touching main
22 [ "$local_oid" = "$zero" ] && continue # deleting main — nothing to test 23 [ "$local_oid" = "$zero" ] && continue # deleting main — nothing to test
23 gate=1 24 gate=1
25 # What this push actually adds. A remote that does not have main yet reports
26 # the zero oid, and there is no range to diff — fall back to the last commit,
27 # which is all a first push can be asked for.
28 if [ "$remote_oid" = "$zero" ]; then
29 range="$local_oid~1..$local_oid"
30 else
31 range="$remote_oid..$local_oid"
32 fi
24 done 33 done
25 34
26 [ "$gate" -eq 1 ] || exit 0 35 [ "$gate" -eq 1 ] || exit 0
27 36
37 # One line per push, not per commit: a push of eight commits owes one retro, and
38 # the range is the whole push. The gate is the ritual, not the prose — it cannot
39 # tell an honest line from a space. It only makes sure the moment is not skipped.
40 if ! git diff --name-only "$range" | grep -qx RETRO.md; then
41 echo >&2
42 echo "pre-push: BLOCKED — nothing in this push touches RETRO.md." >&2
43 echo " Append one line to RETRO.md: what slowed this work down." >&2
44 echo " Then commit or amend it, and push again (override: git push --no-verify)." >&2
45 exit 1
46 fi
47
28 echo "pre-push: '$protected' is being updated — running 'make ci' (bypass: git push --no-verify)" 48 echo "pre-push: '$protected' is being updated — running 'make ci' (bypass: git push --no-verify)"
29 if ! make ci; then 49 if ! make ci; then
30 echo >&2 50 echo >&2
RETRO.md
Old New
@@ -0,0 +1,11 @@
1 # Retro
2
3 One line per push to `main`: what slowed the work down. Enforced by
4 `.githooks/pre-push` — a push that adds no line here is refused.
5
6 ## 2026-08-22
7
8 - Mutation testing: two full sweeps were spent before noticing the workdir
9 filesystem, not the tool, was producing the numbers — ext4 reported 207
10 timed-out mutants and a flattering 100% efficacy where tmpfs reported 199
11 killed and an honest 93%.