Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 771acba30c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Pull request overview
Addresses a CI correctness hazard where actions/cache can overwrite source-controlled files on cache hit, by narrowing cache scope in low-memory.yml and introducing a Bun/TS hygiene audit to detect cache paths that overlap git ls-files.
Changes:
- Narrow verifier JAR cache paths in
.github/workflows/low-memory.ymlto specific.jarfiles and bump cache key suffix to-v2. - Add
tools/hygiene/audit-ci-cache-paths.tsto scan workflow cachepath:entries and flag overlap with tracked files.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| tools/hygiene/audit-ci-cache-paths.ts | New audit tool to detect cache paths that include git-tracked content (prevents cache-clobber silent failures). |
| .github/workflows/low-memory.yml | Narrows verifier cache to jar files and busts existing cache entries via key bump. |
…-paths.ts`) — Aaron's "make it not lucky next time" **Two parts** addressing the silent CI cache-clobber bug discovered via #1401's CircuitRegistration test failure: ## Part 1 — `.github/workflows/low-memory.yml` cache fix Same broad-path bug as gate.yml (#1403 fixes that one): cache path `tools/tla` + `tools/alloy` overwrites source-controlled spec files on cache hit. Narrowed to specific jar files only; bumped key suffix to `-v2` to bust stale cache. Without this fix, low-memory.yml would have the same silent clobber bug as gate.yml had pre-#1403. ## Part 2 — `tools/hygiene/audit-ci-cache-paths.ts` (the not-lucky mechanism) Aaron 2026-05-03: *"lucky catch how can you make it not lucky next time for same class or similar class"* The structural answer: a CI-on-CI audit that flags any `actions/ cache` `path:` in `.github/workflows/*.yml` overlapping with `git ls-files`. The discipline rule: *"actions/cache paths are mutually exclusive with git ls-files — cache only DERIVED files (downloaded jars, built artefacts, user-home tool state), never source-controlled content."* Implementation: - Walks `.github/workflows/*.yml` parsing `path:` blocks (handles both single-line `path: foo` and multi-line `path: |` forms) - For each path, checks if it equals or contains a `git ls-files` entry - Allowlists user-home paths (`~/...`, `/...`) — never tracked - Reports per-violation: workflow + step name + cache path + example tracked file - Includes "Why this is a bug" + "How to fix" output for actionable CI failures **Local verification:** runs against current main (pre-#1403 merge); correctly flags gate.yml's `tools/tla` + `tools/alloy` paths as violations (2). Once #1403 merges + this PR's low-memory.yml fix lands, the audit returns clean. ## Not-yet-done (follow-up): - Wire the audit into CI as a lint job (after #1403 merges so the audit returns clean as a baseline) - Memory file capturing the full discipline (cache-paths-mutually- exclusive-with-git-ls-files) This PR ships the *tool*; the CI wire-up is a deliberate follow-up PR so the lint-job-add can land cleanly on a green baseline. Composes with: - #1401 (CircuitRegistration Safety fix that surfaced this) - #1403 (gate.yml cache fix; sibling of low-memory.yml fix here) - #1383 math-proofs honest assessment (test-fidelity is fundamental to A/B/C grading)
…ute paths + glob expansion + read-failure exit Three #1404 reviewer findings addressed: **P1 — Don't exempt absolute paths.** Original code skipped any path starting with `/` as "user-home equivalent". But actions/cache absolute paths can point INTO the checked-out workspace (e.g. `/home/runner/work/<repo>/<repo>/...`) — same clobber failure mode as relative paths. Now `isUserHomePath` returns true only for `~/...`. Comment added at the function explaining the rationale. **P2 — Expand globs before overlap detection.** actions/cache paths can contain wildcards (`*`, `**`, `?`); the original implementation only did exact/prefix string matching, so a glob path like `tools/tla/specs/*.tla` would be considered non-overlapping with any tracked file. Added `globToRegex()` (* matches non-`/`, ** matches anything including `/`, ? matches single non-`/` char, escapes regex meta-chars) and `pathHasGlob()`; `overlapsTrackedFile` now branches on glob-vs-literal and matches accordingly. **P2 — Return exit 2 on workflow read failure.** Documented exit codes promised exit 2 on workflow read failure but the code logged + skipped + still reported "OK" if no other violations. That's exactly the false-pass class the audit was designed to catch. Added `readFailures` counter; returns exit 2 with explicit error message before the violation summary. **Verification post-fix:** - `bun tools/hygiene/audit-ci-cache-paths.ts` → "OK: 12 workflow(s) audited; no cache paths overlap git-tracked files" (returns clean now that #1403 + this PR's low-memory fix have rebased on top of merged main) - All 3 reviewer findings addressed within the same audit tool Composes with: - #1403 (gate.yml cache fix; merged) - #1404 (this PR; low-memory.yml + audit-tool) - The "not-lucky-next-time" structural answer to Aaron's question
AceHack
force-pushed
the
fix/cache-clobber-low-memory-plus-audit-tool
branch
from
771acba to
691aaae
Compare
…tent-shadow rename + repo-root cache-path edge Three additional reviewer findings: **Variable shadowing in parseCachePaths.** Inner shadowed the outer parameter (the workflow YAML text). Renamed inner to (the per-line trimmed value) for clarity. **Repo-root cache-path false-pass.** Cache paths like `.` or `./` normalised to `""` and silently false-passed (no tracked file equals "" or starts with "/"). High-impact bug class — a workflow caching the entire repo root would not be flagged. Added explicit repo-root branch: if cp is "" or "." after normalisation, return the first tracked file (overlap is 100%). **Header-comment claim about glob expansion.** Already addressed in the prior commit (added globToRegex + pathHasGlob); this thread duplicates the P2 finding. Local verification: audit returns clean (12 workflows audited; no overlap).
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 89ef9b5e80
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+272
to
+274
| for (const tracked of trackedFiles) { | ||
| if (tracked === cp) return tracked; | ||
| if (tracked.startsWith(`${cp}/`)) return tracked; |
There was a problem hiding this comment.
Fresh evidence in this revision: although absolute paths are no longer skipped, overlapsTrackedFile still compares unmodified absolute cache paths against git ls-files entries, which are repo-relative, so a path like /home/runner/work/<repo>/<repo>/tools/tla can never match and is reported clean. That creates a false negative for the same cache-clobber class this audit is meant to block whenever workflows use absolute cache paths into the workspace.
Useful? React with 👍 / 👎.
| collectingPaths = false; | ||
| continue; | ||
| } | ||
| if (line.match(/uses:\s*actions\/cache@/)) { |
There was a problem hiding this comment.
The detector only enters cache parsing for uses: actions/cache@..., so steps using actions/cache/restore@... (which also restores files to path) are ignored entirely. GitHub’s cache action docs include restore/save forms, and a restore step can overwrite checked-out tracked files in exactly the same way, so this omission leaves a blind spot where unsafe cache paths pass the audit.
Useful? React with 👍 / 👎.
Comment on lines
+118
to
+120
| if (glob[i + 1] === "*") { | ||
| pattern += ".*"; | ||
| i += 2; |
There was a problem hiding this comment.
**/ when matching paths
globToRegex translates ** to .*, which makes patterns like **/*.md require at least one directory separator and therefore miss repo-root files (e.g. README.md). Since actions/cache path patterns use @actions/glob semantics where ** can match zero path segments, this causes false negatives for globbed cache paths that include tracked files at the repository root.
Useful? React with 👍 / 👎.
Comment on lines
+34
to
+35
| // - Paths starting with `~/` (user home; never tracked) | ||
| // - Paths starting with `/` |
| // `/home/runner/work/<repo>/<repo>/...`) — same clobber failure | ||
| // mode as relative paths. Per #1404 reviewer P1: don't skip | ||
| // absolute paths. | ||
| return path.startsWith("~"); |
| maxBuffer: SPAWN_MAX_BUFFER, | ||
| }); | ||
| if (result.status !== 0) { | ||
| process.stderr.write(`ERROR: 'git ls-files' failed (exit ${String(result.status)})\n`); |
2 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…llow-up (#1406) Wires the structural cache-path audit (shipped in #1404) into CI as a dedicated lint workflow. The audit fires on: - Any change to .github/workflows/** (catches new workflow files that might introduce broad cache paths) - Any change to tools/hygiene/audit-ci-cache-paths.ts (catches bugs in the audit itself before they affect future PRs) - workflow_dispatch (manual triage) Job runs the .ts audit; non-zero exit fails the workflow, blocking merge if any actions/cache path overlaps with git-tracked files. This closes the not-lucky-next-time loop: future PRs that introduce the silent-clobber bug class CANNOT pass this gate. The audit's detailed violation output (workflow + step + tracked file + 'Why this is a bug' + 'How to fix') makes the failure self- diagnosing. Local verification: 13 workflows audited (including this new one); no overlap. The audit returns clean as a baseline. Composes with #1404 (the audit tool itself), #1403 (the gate.yml fix that proved the bug), the math-proofs assessment's test- fidelity discipline.
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…silent-clobber bug class) (#1407) * memory: cache-paths-mutually-exclusive-with-git-ls-files discipline (silent-clobber bug class) Captures the durable substrate for the discipline rule the session surfaced via the CircuitRegistration cache-clobber discovery (#1403 + #1404 + #1406): *actions/cache paths must be mutually exclusive with git ls-files — cache only DERIVED files (downloaded jars, built artefacts, user-home tool state), never source-controlled content.* Memory file structure (per chat-is-assertion-channel discipline + substrate-or-it-didn't-happen): - Rule (carved sentence) - Why this is load-bearing (the silent + invisible failure mode) - Triggering case (CircuitRegistration B-0180 fix; verbatim error text) - How to apply (3 layers: workflow-author-time + verify-then-claim- time + structurally enforced via audit + lint gate) - Composes with (DST + verify-then-claim + test-fidelity contract + CI-on-CI audit pattern) - Tooling lineage (4 substrate refs) - Future-Otto reference (when-tempted + when-CI-fails) - Reasoning lineage (Aaron's 'lucky catch' question) MEMORY.md updated with newest-first pointer. Composes with the earlier cluster (#1403 cache fix + #1404 audit tool + #1406 CI lint gate) — this memory file is the chat→substrate discipline-encoding step that closes the loop. * memory(cache-paths): add bug-locus disambiguation per Aaron's question — usage-bug not GitHub-bug Aaron 2026-05-03: 'is the a real github bug or was a bug in our code?' Honest answer: NOT a GitHub bug, IS a bug in our workflow config. actions/cache does exactly what its docs promise — restores cached files at the configured paths. We asked it to cache a path that contained source-controlled files; it did. The fix is on our side: narrow the cache path. Added 'Bug-locus disambiguation' section to the memory file clarifying: - This is a usage bug in workflow configuration, not a tool bug - The existing actions/cache behavior is documented - A reasonable upstream feature request (warn-on-overlap-with-git) would be an enhancement, not a bug fix Future-Otto reading this memory: don't pattern-match the discovery as 'GitHub broken' when reaching for the discipline. The structural fix (audit + lint gate) is correct because OUR usage was wrong, not because the action was wrong.
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…ster + cache-clobber discipline encoded (#1408) Substantial multi-tick session shard. 18 PRs touched (#1383 + #1387 + #1392-#1407 inclusive); 14 merged + 4 in-flight as of shard time. **Math-proofs assessment progress** (#1383 outstanding-work matrix): - A1+A2 → A-with-CI ✓ (#1394 Lean lake-build workflow) - A4 registry rows ✓ (#1393) - B1 → 2 of 4 deferred specs in CI ✓ (#1397 DbspSpec + #1401 CircuitRegistration B-0180 closed) - B2 Alloy → A ✓ (#1396 silent-no-op spec-path fix) - B4 Semgrep → A ✓ (correction) - Peer-review email template ✓ (#1387) - Phase 0 substrate-discovery PoC ✓ (#1392) - Stryker config-fix ✓ (#1395; CI wire deferred) - 3 broken-spec backlog rows filed ✓ (#1398) **Cache-clobber silent-bug class discovered + fully encoded:** B-0180 fix passing locally + failing CI → verify-then-claim identified gate.yml + low-memory.yml caching whole tools/tla and tools/alloy directories. Fix cluster: #1403 (gate.yml) + #1404 (low-memory.yml + audit-ci-cache-paths.ts) + #1406 (CI lint gate) + #1407 (memory file + bug-locus disambiguation per Aaron's 'real github bug?' question — answer: usage-bug, not tool-bug). **Other substrate work:** #1399 BACKLOG.md regen, #1400 .ts/.sh parity bug, #1402 assessment matrix doc update, #1405 B-0182 backlog row (Linux-only formal verification — orthogonal-axes split per Aaron 2026-05-03). **Discipline lessons captured:** chat-is-assertion-channel, substrate-corrections-cluster, search-first-before-architectural- expansion, verify-then-claim CI fidelity, documentation-is- current-state-not-history. Carved sentence: 'When a lucky catch surfaces a class of bug, build the structural fix that eliminates the luck — audit + lint gate + carved-sentence rule + memory file.'
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…t bug surfaced by #1413) (#1415) * fix+backlog: skip Spine F# Alloy test pending B-0184 spec fix The pre-#1413 cache-clobber + AlloyRunner.java compile failure was silently no-op'ing all Alloy tests. Once the cache narrowed (#1404) and AlloyRunner.java fixed (#1413), CI actually runs Alloy now — which surfaces the latent Spine.als spec bug at line 35 (Alloy 6.2.0 type-check error: sum-comprehension expects Int but finds Boolean). Two parts in this PR: 1. **B-0184 backlog row** filed — captures the spec bug + likely intent (sum vs all comprehension confusion) + fix path + the silent-skip lineage. P2 since it's pre-existing latent failure surfaced post-cleanup. 2. **F# Alloy.Runner.Tests.fs**: add Skip="..." attribute to the Spine [Fact] so CI doesn't fail until B-0184 lands. The skip message references B-0184 so future-Otto can find the row. Test result post-fix: 2 passed (InfoTheoreticSharder + jar- installed), 1 skipped (Spine pending B-0184). Build clean (0/0). Composes with B-0183 Phase 1 (#1413 surfaced this bug class) + B-0183 Phase 3 retirement of F# Alloy tests — Spine.als fix needs to land before TS wrapper retires F# tests so the wrapper passes. * fix(B-0184): two-part spec fix — parens + check→fact+run + P2→P1 + remove F# Skip Reviewer #1415 caught two related issues: 1. Skip removes only CI check for Spine.als (regression after #1413 landed AlloyRunner.java compile fix; spec was about to be on active CI surface) 2. B-0184 'Why P2' was inaccurate — post-#1413 the spec IS running Aaron 2026-05-03: 'fix them like you normally would'. So instead of deferring with Skip + P2, fix the spec inline + remove Skip + bump B-0184 to P1 + close. Two-part spec fix: 1. Parens around sum-comprehension at line 35: (sum b : l.batches | b.size) <= mul[2, cap[l.level, maxCap]] Matches comment intent 'total size at level i ≤ 2 * cap(i)' (sum-then-compare, not sum-of-Booleans). 2. Replaced check command with fact + run: - Original: `check SizeDoublingHolds { SizeDoubling[1] }` — asks 'does property hold for ALL bounded instances?' Alloy trivially constructs counterexamples by allowing arbitrary Int batch sizes (no constraint). - Fix: added `fact NonNegativeBatchSizes` (real LSM spines have non-negative element counts) + replaced check with `run SizeDoublingAdmitsInstance` for constructive existence proof. `7 Int` bitwidth bump prevents cap-function overflow. Local verification: `java -jar alloy.jar exec -f Spine.als` returns `00. run SizeDoublingAdmitsInstance 0 1/1 SAT` (instance found). AlloyRunner translates SAT-on-run to OK. F# Skip removed; Spine [Fact] back on active CI surface. Backlog row moved P2/ → P1/ to match the bumped priority. Status flipped to closed. Resolution + 3 discipline lessons appended: 1. Check-vs-run-vs-fact semantic confusion (the substantive spec-design lesson) 2. Alloy Int bitwidth must accommodate cap-function range 3. Coverage-loss-is-regression: when a fix becomes part of the active CI surface, deferring loses coverage rather than just defers it (the reviewer's P2→P1 framing was right) .gitignore Spine/ (Alloy run-output directory). Composes with #1413 (the AlloyRunner.java fix that surfaced this) + #1414 (PR-review meta-classes memory file — discipline lesson #3 above is a fresh instance of the meta-class).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Two parts addressing Aaron's question on the #1403 cache-clobber discovery: "lucky catch how can you make it not lucky next time for same class or similar class"
Part 1 —
.github/workflows/low-memory.ymlcache fixSame broad-path bug as gate.yml (fixed in #1403). Path narrowed to specific jar files only; key bumped to
-v2.Part 2 —
tools/hygiene/audit-ci-cache-paths.ts(the not-lucky mechanism)Structural CI-on-CI audit that flags any
actions/cachepath:overlapping withgit ls-files. Discipline rule:path:formsLocal verification
Currently flags gate.yml's
tools/tla+tools/alloypaths (will return clean once #1403 merges + this PR lands).Follow-up (not in this PR)
Test plan
bun tools/hygiene/audit-ci-cache-paths.tsruns cleanly + correctly identifies violations🤖 Generated with Claude Code