From b697288e768e15aa52eaa6ca344971ba19e40dd1 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 01:47:39 +0100 Subject: [PATCH 1/4] ci(occupancy): move the PR path filter into a gate, so the reading checks can be required squash carried a draft `TH.[_]` placeholder; #117 fixed the proof), because nothing required the check to pass first -- and nothing could have: the pull_request trigger was path-filtered, so the check never posted on PRs that touch no occupancy file, and a required check that never posts can never be satisfied. The path filter now lives in an `Occupancy relevance` gate job: the workflow runs on every PR, the gate diffs the change against the same file list (plain `case` globs; a third-party paths-filter action is refused by the account's allow-list), and the two heavy jobs run only when it matches -- posting `skipped` otherwise, which a required check counts as satisfied. All three job names are stable identifiers with no matrix, as test_install_pins.jl asserts for every job in every workflow. Branch-Floor can then require `Occupancy relevance` (itself included: a failed gate skips its dependents, and a skipped check satisfies a requirement -- the gate is the one check that must not be skipped silently), `Occupancy disagreement test`, `Occupancy typed peak`, alongside ci.yml's `Julia tests` and `Agda proofs`. That ruleset change is a settings change, kept out of this PR on purpose. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- .github/workflows/occupancy.yml | 90 +++++++++++++++++++++++++++------ 1 file changed, 75 insertions(+), 15 deletions(-) diff --git a/.github/workflows/occupancy.yml b/.github/workflows/occupancy.yml index 8e1fdf10..284f0d6d 100644 --- a/.github/workflows/occupancy.yml +++ b/.github/workflows/occupancy.yml @@ -11,6 +11,24 @@ # everything here installs from pinned URLs checked against pinned SHA256s, as # ci.yml now does too. The disagreement test also runs in ci.yml's full suite; # it runs here as well so that a change to the probe gets its own check. +# +# #116 merged with this workflow's "Occupancy typed peak" check red (its squash +# carried a draft `TH.[_]` placeholder; #117 fixed the proof), because nothing +# required the check to pass first -- and nothing COULD have: a check posts +# only when its workflow runs, and the pull_request trigger was path-filtered, +# so requiring these checks would have deadlocked every PR that touches no +# occupancy file. A required check that never posts can never be satisfied; the +# trap ci.yml's header records for its own job names. +# +# So the pull_request path filter moved into the `Occupancy relevance` gate +# below. The workflow now runs on EVERY pull request; the gate decides whether +# the change touches the occupancy reading; the two heavy jobs run only when it +# does, and post their checks as `skipped` otherwise, which a required check +# counts as satisfied. The gate itself posts on every PR too, and it is the one +# check of the three that must be required without exception: if the gate +# failed, its dependents would be skipped and would satisfy their requirement +# silently. The push trigger keeps its native paths filter, so a push to main +# still starts this workflow only when it should. name: Occupancy reading on: @@ -30,22 +48,10 @@ on: - scripts/check-occupancy.sh - scripts/fetch-siblings.sh - .github/workflows/occupancy.yml - # Any base branch, so a PR stacked on another one is checked too. + # No paths filter, on purpose (see above): the gate must post its check on + # every PR, whichever files the PR touches. Any base branch, so a PR stacked + # on another one is gated too. pull_request: - paths: - - src/core/memory_probe.jl - - src/core/provenance.jl - - src/pipeline/tools.jl - - src/server/routes/pipeline.jl - - test/occupancy_disagreement_test.jl - - test/unit/test_occupancy_grade.jl - - scripts/check-occupancy-grades.jl - - scripts/lint-occupancy-readings.sh - - docs/occupancy/** - - docs/occupancy-2026-10.adoc - - scripts/check-occupancy.sh - - scripts/fetch-siblings.sh - - .github/workflows/occupancy.yml permissions: contents: read @@ -62,7 +68,59 @@ env: JULIA_SHA256: 41b84d727e4e96fbf3ed9e92fa195d773d247b9097f73fad688f8b699758bae7 jobs: + # Decides whether the PR touches the occupancy reading at all. The file list + # is the pull_request half of the old paths filter, moved here because a + # pinned-actions workflow cannot use a third-party paths-filter action (the + # account's allow-list refuses one) -- plain `case` globs are all it takes. + # In a case pattern `*` crosses `/`, so `docs/occupancy/*` is the old + # `docs/occupancy/**`. + gate: + name: Occupancy relevance + runs-on: ubuntu-24.04 + timeout-minutes: 10 + outputs: + relevant: ${{ steps.push.outputs.relevant || steps.pr.outputs.relevant }} + steps: + # A push only starts this workflow when a `paths:` file changed (the + # trigger filter above), so the gate has nothing to decide on pushes. + - name: A push is already path-filtered + id: push + if: github.event_name == 'push' + run: echo 'relevant=true' >> "$GITHUB_OUTPUT" + + # Full history, because the three-dot diff names the merge base of the + # PR's base tip and its merge commit -- a shallow checkout does not have + # both, and a stacked PR's merge base sits further back still. + - name: Checkout the change + if: github.event_name == 'pull_request' + uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 + with: + persist-credentials: false # nothing here pushes + fetch-depth: 0 + + - name: Does the change touch the occupancy reading? + id: pr + if: github.event_name == 'pull_request' + run: | + relevant=false + patterns=(src/core/memory_probe.jl src/core/provenance.jl src/pipeline/tools.jl + src/server/routes/pipeline.jl test/occupancy_disagreement_test.jl + test/unit/test_occupancy_grade.jl scripts/check-occupancy-grades.jl + scripts/lint-occupancy-readings.sh 'docs/occupancy/*' + docs/occupancy-2026-10.adoc scripts/check-occupancy.sh + scripts/fetch-siblings.sh .github/workflows/occupancy.yml) + while IFS= read -r file; do + for pattern in "${patterns[@]}"; do + case "$file" in + $pattern) relevant=true; break 2 ;; + esac + done + done < <(git diff --name-only "${{ github.event.pull_request.base.sha }}...HEAD") + echo "relevant=$relevant" >> "$GITHUB_OUTPUT" + disagreement: + needs: gate + if: needs.gate.outputs.relevant == 'true' name: Occupancy disagreement test runs-on: ubuntu-24.04 timeout-minutes: 45 @@ -123,6 +181,8 @@ jobs: run: bash scripts/lint-occupancy-readings.sh typed-peak: + needs: gate + if: needs.gate.outputs.relevant == 'true' name: Occupancy typed peak runs-on: ubuntu-24.04 # The Agda 2.6.4.3 Debian trixie packages, in a digest-pinned image, as the From d160c8daf7a02896a36d7bd688e1c9d42f938b31 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Thu, 15 Oct 2026 02:00:43 +0000 Subject: [PATCH 2/4] ci(occupancy): handle renamed files and NUL-delimited paths in the PR gate --- .github/workflows/occupancy.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/occupancy.yml b/.github/workflows/occupancy.yml index 284f0d6d..00463b0d 100644 --- a/.github/workflows/occupancy.yml +++ b/.github/workflows/occupancy.yml @@ -109,13 +109,13 @@ jobs: scripts/lint-occupancy-readings.sh 'docs/occupancy/*' docs/occupancy-2026-10.adoc scripts/check-occupancy.sh scripts/fetch-siblings.sh .github/workflows/occupancy.yml) - while IFS= read -r file; do + while IFS= read -r -d '' file; do for pattern in "${patterns[@]}"; do case "$file" in $pattern) relevant=true; break 2 ;; esac done - done < <(git diff --name-only "${{ github.event.pull_request.base.sha }}...HEAD") + done < <(git diff --no-renames --name-only -z "${{ github.event.pull_request.base.sha }}...HEAD") echo "relevant=$relevant" >> "$GITHUB_OUTPUT" disagreement: From 18ba1409a555856d76d1720a171eadd2c775dc52 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 03:14:32 +0100 Subject: [PATCH 3/4] ci(occupancy): pass the PR base SHA to the gate through env, not interpolation zizmor's template-injection rule (surfaced with CodeRabbit's review) flags the `${{ github.event.pull_request.base.sha }}` expansion interpolated directly into the gate's run script. The base SHA is GitHub-supplied and hex-only, so it is not practically injectable, but the env indirection costs three lines, silences the lint, and makes the gate fragment runnable locally with BASE_SHA set by hand. The two functional-correctness findings from the same review (NUL-delimited path reading, --no-renames so a renamed-away relevant file still triggers the jobs) were already addressed in d160c8d; this commit does not touch them. Verified locally against an adversarial change set: with the fixes, renaming docs/occupancy/schedules.yml away and adding an unusual-character occupancy doc both mark the gate relevant; an irrelevant-only change stays irrelevant. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- .github/workflows/occupancy.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/occupancy.yml b/.github/workflows/occupancy.yml index 51c4b4d5..a0874f30 100644 --- a/.github/workflows/occupancy.yml +++ b/.github/workflows/occupancy.yml @@ -101,6 +101,12 @@ jobs: - name: Does the change touch the occupancy reading? id: pr if: github.event_name == 'pull_request' + env: + # zizmor flags template expressions interpolated into run scripts + # (template-injection), and the gate script is easier to run locally + # with the value in an environment variable in any case. The base SHA + # is GitHub-supplied, but the indirection costs nothing. + BASE_SHA: ${{ github.event.pull_request.base.sha }} run: | relevant=false patterns=(src/core/memory_probe.jl src/core/provenance.jl src/pipeline/tools.jl @@ -115,7 +121,7 @@ jobs: $pattern) relevant=true; break 2 ;; esac done - done < <(git diff --no-renames --name-only -z "${{ github.event.pull_request.base.sha }}...HEAD") + done < <(git diff --no-renames --name-only -z "$BASE_SHA...HEAD") echo "relevant=$relevant" >> "$GITHUB_OUTPUT" disagreement: From 53e3dde0f11beaf96cf64d8d7bcd60faf9cdba80 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 03:55:50 +0100 Subject: [PATCH 4/4] ci(occupancy): fail the gate when git diff fails, instead of reading it as no changes CodeRabbit functional-correctness finding (Major): the gate read its diff through a process substitution, which hides git diff's exit status. An unavailable comparison SHA or a repository error would supply no pathnames, the loop would read nothing, and the gate would post relevant=false -- skipping the two occupancy jobs, whose skipped conclusion satisfies a required check, and passing a relevant PR silently. The diff now goes to a file first, its exit status is checked, and a failed diff fails the gate itself: the one failure the required-check design cannot afford to skip. Verified with the gate's exact logic in a scratch repository: a bad SHA or missing ref exits 1; a relevant diff still posts true; an irrelevant diff still posts false. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- .github/workflows/occupancy.yml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/workflows/occupancy.yml b/.github/workflows/occupancy.yml index a0874f30..0513de5c 100644 --- a/.github/workflows/occupancy.yml +++ b/.github/workflows/occupancy.yml @@ -115,13 +115,25 @@ jobs: scripts/lint-occupancy-readings.sh 'docs/occupancy/*' docs/occupancy-2026-10.adoc scripts/check-occupancy.sh scripts/fetch-siblings.sh .github/workflows/occupancy.yml) + # The diff goes to a file first because a process substitution hides + # git diff's exit status: an unavailable comparison SHA or a repository + # error would read as "no changes", and the gate would post + # relevant=false -- skipping the two occupancy jobs, whose `skipped` + # conclusion satisfies a required check -- so a relevant PR would + # pass silently. A failed diff must fail the gate itself: that is + # the one failure the required-check design cannot afford to skip. + changed="$RUNNER_TEMP/occupancy-changed-files" + if ! git diff --no-renames --name-only -z "$BASE_SHA...HEAD" > "$changed"; then + echo "ERROR: git diff $BASE_SHA...HEAD failed" >&2 + exit 1 + fi while IFS= read -r -d '' file; do for pattern in "${patterns[@]}"; do case "$file" in $pattern) relevant=true; break 2 ;; esac done - done < <(git diff --no-renames --name-only -z "$BASE_SHA...HEAD") + done < "$changed" echo "relevant=$relevant" >> "$GITHUB_OUTPUT" disagreement: