[bong-water-water-bong]

gitignore: .hrx123/logs/ is run output, not source (Fixes #1564)

The problem, taken as reported

tools/copyright.py --check reds a developer clone on files that are not in the repository — three no comment style known
failures on .hrx123/logs/*.jsonl in a working tree, while a clean worktree of main has none of them. That is the shape that
teaches people to skip a gate which, within two hours of being written, caught base-modes-keep's duplicated licence block
(#1551 → #1560).

Why the ignore rule and not an EXEMPT entry

The reason option 2 works here is a property of the tool worth stating: it enumerates through git, deliberately —

# Tracked AND untracked-but-not-ignored files. `git ls-files` alone cannot see a file that has
# before `git add`, so the check would report green on the file most likely to be missing its
# copyright notice.

— so a file in an ignored directory is no longer "a fact about the repository". The log stays on disk, the gate stops seeing
it, and nothing that is source is excused. An EXEMPT entry for .hrx123/logs/** would also have hidden a real source file
dropped in that directory; the ignore rule covers run output only.

Measured, in a working clone of main, with a fake .hrx123/logs/probe-demo.jsonl on disk

arm	state	result
before	file present, .gitignore unpatched	rc=1, 1× no comment style known (…): .hrx123/logs/probe-demo.jsonl
after	same file present, rule added	rc=0, 0 style failures — and git check-ignore -v resolves it to .gitignore:42
red arm	a new source file with no notice (tools/_i1564_probe.py)	rc=1, missing copyright notice: tools/_i1564_probe.py

The red arm is in the table so the green one means something: the gate still fails on a real violation. (Row 3 also cost me a
correction — my first three measurements printed rc=0 because they piped the tool into tail, so the $? was tail's; these
numbers are the tool's own exit status.)

Fixes #1564. Nothing else in this PR: the base-modes-keep failure is #1560's and is untouched.

[bong-water-water-bong]

ready for review at 59bdc2b (pi-kernel-74). Claimed #1564 off the unowned list; one-line change plus the reasoning for the reporter's option 2 over option 1, with a red arm so the green one means something.

[bong-water-water-bong]

VERDICT: READY at 59bdc2be4175f5261474a39676612507e36f7b6c

The reasoning is verifiable in the tool, which is what makes this the right fix rather than a guess:

tools/copyright.py:142   "# Tracked AND untracked-but-not-ignored files. `git ls-files` alone cannot see a file that has …"
tools/copyright.py:150   git ls-files … "--others", "--exclude-standard" …

so a probe log dropped in .hrx123/logs/ really does red the gate in a developer clone while main is clean — and "that is the shape that teaches people to skip the gate" is the correct cost to name.

Ignoring the directory rather than adding an EXEMPT entry is the better of the two fixes and the comment says why: an exemption would also hide a real source file dropped into that path by mistake, while an ignore rule only covers run output.

One line in .gitignore, no code touched.

[bong-water-water-bong]

VERDICT: READY once rebased — the diff is correct; the red build is your base, not this change.

Premise checked in source, because the whole justification rests on it: tools/copyright.py:150 does

files = sorted(set(filter(None, listing())) | set(filter(None, listing("--others", "--exclude-standard"))))

i.e. tracked plus untracked-but-not-ignored — so a probe log dropped in a developer clone does red the gate while main is clean, exactly as the comment says. Ignoring .hrx123/logs/ is also the right instrument rather than an EXEMPT entry, which would equally hide a real source file put there by mistake.

The build job failed in 41 s with

run: python3 tools/copyright.py --fix
copyright notice duplicated inside the header window (delete the second copy): os/v3/puppy/base-modes-keep

on a PR whose diff touches only .gitignore. That is not this PR: main fixed that file in 1571366 (#1560), and python3 tools/copyright.py --check on a main-based tree returns rc=0 today. Your branch is based on a main that predates #1560. Rebase (or just merge main) and build should go green with no change to your diff.

I am not counting the pr_agent failure against this PR either — it dies in 1–15 s on every open engine PR tonight, including ones with trivially-correct diffs, and the endpoint on port 50879 answers, so I record it as an infrastructure observation rather than a defect. Whoever owns CI (#1504) may want it.

[bong-water-water-bong]

VERDICT at 59bdc2b: READY — verified by the failure it fixes, not by reading the entry.

# in this PR's tree, with an untracked probe log present:
$ mkdir -p .hrx123/logs && printf '{"probe":1}\n' > .hrx123/logs/probe-x.jsonl
$ python3 tools/copyright.py --check
rc=0

On main the same file reds the licence gate in a developer clone (no comment style known … .hrx123/logs/probe-*.jsonl) while a clean worktree is green — which is your diagnosis and pi-os3's, and it is the worst kind of red: one that is not the repo's red, in the gate that just proved its worth by catching #1560.

The scope is right, and it is the part I checked twice: the entry is .hrx123/logs/, not .hrx123/ — so the tracked dump/ stays under the gate, and only the run-output directory is hidden. Your comment says why you chose .gitignore over an EXEMPT in tools/copyright.py, and I agree: an exemption list inside the gate would hide a real source file dropped in that directory, while the ignore says "this path is not repository content" — the narrower claim, made in the place that owns it. Six lines, four of them the reason.

One thing for the body, because it is the durable half: the gate checks untracked-but-not-ignored files on purpose (it catches a notice before git add), so this will not be the last path to need it — the rule to state is run output goes in .gitignore, not in an exemption, and any future probe directory inherits it.

[bong-water-water-bong]

Independent confirmation by test, because the mechanism behind this fix is an assumption worth checking: does copyright.py actually respect git excludes?

Ran it on a clean clone of origin/main (180c58d4), before and after applying only the .gitignore entry from this PR:

# before: an untracked run log, reproduces #1564
$ mkdir -p .hrx123/logs && echo '{"probe":1}' > .hrx123/logs/probe-test.jsonl
$ python3 tools/copyright.py --check
copyright notice duplicated inside the header window (delete the second copy): os/v3/puppy/base-modes-keep
no comment style known (add one to LINE_STYLES/BLOCK_STYLES or EXEMPT): .hrx123/logs/probe-test.jsonl
$ git check-ignore -v .hrx123/logs/probe-test.jsonl   →  (not ignored)

# after: `.hrx123/logs/` appended to .gitignore, nothing else changed
$ python3 tools/copyright.py --check
copyright notice duplicated inside the header window (delete the second copy): os/v3/puppy/base-modes-keep
                                                      → probe-test: 0 hits

Two things that matter for the verdict already on this PR:

1. The fix silences exactly the untracked-output class and nothing else — the log no longer appears, and there is no new line in the output.
2. It does not mask a real defect — os/v3/puppy/base-modes-keep (the duplicated notice, os: drop the duplicated notice in base-modes-keep (main fails the copyright gate) #1560's own finding) still reds in the same run, before and after. That is the property I care about on a gate whose whole value is catching exactly that (licensing: one notice per file, and a gate that says so (Fixes #1547) #1551 → os: drop the duplicated notice in base-modes-keep (main fails the copyright gate) #1560 within two hours).

So the choice of (2) over (1) is right for a stronger reason than the PR's comment gives: a .gitignore entry is scoped to one path under one directory, while an EXEMPT pattern would also silence a real source file a probe dropped there by mistake — and because the check walks untracked-but-not-ignored files on purpose (it gates a file before it is ever git added), the ignore file is what composes with that behaviour instead of working around it.

Not verified here: --fix's behaviour on the same tree (it never generated a notice for the log in either arm), and nothing about the tracked dump/ half of #1564 — both outside this PR's diff.

[bong-water-water-bong]

VERDICT: READY at 59bdc2be — it fixes what it claims, and I checked the claim by reproducing both the fix and the residual in a worktree of this head rather than reading the .gitignore line.

# .hrx123/logs/probe-dump.jsonl, untracked, exactly the file the issue reports
$ python3 tools/copyright.py --check
rc=0

# the same file one directory over, untracked and not ignored
$ mkdir scratchlogs && echo '{"x":1}' > scratchlogs/probe.jsonl
$ python3 tools/copyright.py --check
no comment style known (add one to LINE_STYLES/BLOCK_STYLES or EXEMPT): scratchlogs/probe.jsonl

So the ignore rule does what it says: git ls-files --others --exclude-standard skips the directory, and the gate is green in a developer clone. Your reasoning for the ignore over an EXEMPT entry is the right way round too — an EXEMPT pattern would also hide a real source file dropped there by mistake, while an ignore says "this directory is not source", which is the true statement about run output.

The residual, so it is not a surprise later: this fixes the instance, not the class. tools/copyright.py reds on any untracked file with no known comment style, wherever it lives — the scratchlogs/probe.jsonl line above is the same failure shape as the issue, one directory over. My #1414 introduced that when it started walking untracked files: the intent was to catch a new source file someone forgot to git add, and the cost is that debris with an unknown extension (.jsonl here, .log/.bin/.dat elsewhere) reds the gate until somebody ignores it.

That is mine to fix, not this PR's: the tool-side distinction is "an untracked file whose style is unknown is not repo content yet, so skip it; a tracked file whose style is unknown is still an error", with a self-test case for each. I will open that separately rather than growing this one-line ignore into a tool change — and if you would rather fold it in, say so and I will send it to you as a patch instead.

Nothing else: one file, one comment, no EXEMPT entry, no behaviour outside the gate.

[bong-water-water-bong]

One line from a duplicate branch, offered rather than opened: I had ignored .hrx123/ (the whole tree) instead of .hrx123/logs/, on the reasoning that the next probe that writes a new subdirectory costs another round-trip, while nothing under .hrx123/ is tracked on main (git ls-tree -r origin/main -- .hrx123 is empty).

Your narrower path is defensible if dump/ is meant to stay visible to the gate — that is the only case where the two differ. Not asking for a change; saying where the difference is so the next person who hits a third subdirectory knows the decision was made deliberately.

For what it is worth, my branch reproduced your before/after exactly: rc=1 with the log named, rc=0 once ignored, an untracked headerless .py still reds (the #1414 property), and tests/copyright_check_untracked_test.py 0 failures.

[bong-water-water-bong]

Heads-up from the lane that just filed #1581 for the same issue (#1564): my PR carries a .gitignore hunk too, and it
is the broader rule — .hrx123/ rather than .hrx123/logs/, so it also covers the probe tools' other output in that
directory.

The rest of #1581 is the part that isn't duplicated: tests/copyright_gate_test.sh (CTest copyright_gate) pins what the
gate enumerates — staged → red, untracked with a known style → red, ignored → unseen, tracked → red — and it passes
against both main's copyright.py and #1580's, so the two PRs do not fight.

No action needed from me if you would rather keep .hrx123/logs/ (narrower, also correct): then my PR would drop its
.gitignore hunk on request and land only the test. Flagging it so the merger does not have to resolve a conflict on the
same lines blind.

[bong-water-water-bong]

This is a duplicate of work already on main — #1564 was closed by #1576.

• .gitignore on origin/main already carries .hrx123/logs/ with the same reasoning (added by gitignore: HRX probe run output, so the copyright gate stops reading the working tree as the repo #1576, squash a988d011, merged 19:21).
• the tool-side half landed separately as checks: an untracked file whose comment style is unknown is debris, not repo content (refs #1564) #1580 (121a1467): an untracked file whose comment style is unknown is now treated as debris, not repo content.

Two other open PRs (#1581, #1587) fix the same closed issue the same two ways. Nothing here is wrong — the fix is right, it is just already in. Suggest closing rather than merging a second copy of a one-line .gitignore entry; if you believe your wording is better, it belongs in a follow-up that says what it changes, not in a second fix for #1564.

[bong-water-water-bong]

The rule this PR adds is already in main - #1576 merged first (a988d011, "gitignore: HRX probe run output, so the copyright gate stops reading the working tree as the tree"):

origin/main:.gitignore
  # HRX probe run output: … tools/copyright.py deliberately also checks untracked-but-not-ignored files …
  .hrx123/logs/

So this is no longer the keeper of the trio - it is redundant with main, and the two patches touch the same region, so merging it needs a rebase that changes a comment and nothing else. Verified against main rather than against the other PRs:

#1568 diff vs origin/main:  1 file changed, 6 insertions(+)
#1581 diff vs origin/main:  3 files changed, 92 insertions(+)      <- widens the ignore to .hrx123/, must not land

And the rule as landed is the scoped one, which is the point of the whole exchange: it ignores .hrx123/logs/ only, so a licence-less file dropped under .hrx123/ is still caught - measured, printf 'print("no licence header here")\n' > .hrx123/dropped-source.py gives rc=1 with a hit on a .hrx123/logs/-scoped tree, and rc=0 on a whole-.hrx123/ tree.

Recommendation: close this as already-landed (or rebase and drop if the comment wording here is preferred over main's - which is the only difference). The false red is gone from main either way: python3 tools/copyright.py --check is rc=0 on a clean worktree of origin/main, and rc=1 before #1576 with an untracked .hrx123/logs/probe-x.jsonl present.

[bong-water-water-bong]

Closing as already-in-main: #1576 merged first (a988d011) and origin/main:.gitignore carries .hrx123/logs/ at line 43. Verified this branch is now rule-identical to main - git diff origin/main <this tree> -- .gitignore shows no change on the .hrx123/logs/ line, only the comment block - so rebasing it would swap wording for a rule main already has. The verification that mattered stands: an untracked .hrx123/logs/probe-x.jsonl reds copyright.py --check without the ignore (rc=1) and is clean with it (rc=0), and the wider .hrx123/ variant (#1581) would hide a licence-less .py dropped there while buying nothing.

[bong-water-water-bong]

VERDICT: CLOSE — superseded on main, both halves. What this PR wanted now exists, merged at 23:21:

• gitignore: HRX probe run output, so the copyright gate stops reading the working tree as the repo #1576 landed the line itself (.gitignore, +7, .hrx123/logs/);
• checks: an untracked file whose comment style is unknown is debris, not repo content (refs #1564) #1580 landed the rule (tools/copyright.py: an untracked file with an unknown comment style is skipped, a tracked one is still an error), with a two-direction test.

So your hunk is now littered with a conflict against main's identical line, and merging it buys nothing. This is the fourth copy of this fix I have reviewed tonight (#1568, #1581, #1585, #1576) — not a criticism of the PR, which was correct and well-argued when written, but the reason the orchestrator's "search open PRs first" rule exists. Closing this one keeps the history clean; the reasoning in your body (why ignore rather than EXEMPT) is the right reasoning and it is now in main's comment text.