night: a red night check opens or updates one issue; RELEASE step 2 reads the nightly first (PMAT-2174, PMAT-2175)

.github/actions/night-issue/action.yml

@@ -0,0 +1,69 @@
+name: night-issue
+description: >
+  A red night check opens or updates its ONE issue (PMAT-2174). Called as the
+  LAST step of every night-only (advisory) job in ci.yml, under
+  `if: failure() && github.event_name == 'schedule'`, so it runs only after
+  that job has already failed on a scheduled run. It finds the open issue
+  titled exactly `night: <check> red on main`; if there is one it comments the
+  run on it, otherwise it creates it assigned to the one owner. It cannot turn
+  a red job green (the job has already failed) and it never runs on
+  pull_request, merge_group, push or workflow_dispatch: the script refuses any
+  event but `schedule` before it calls gh. Pinned by
+  crates/xpile/tests/night_checks_off_pr_path.rs (XPILE-NIGHT-CHECKS-001).
+
+inputs:
+  check:
+    description: The ci.yml job id of the night check that failed.
+    required: true
+  owner:
+    description: >
+      The ONE owner (a GitHub login) a new night issue is assigned to. One
+      login, never a list: a ticket with two owners has none.
+    required: false
+    default: noahgift
+
+runs:
+  using: composite
+  steps:
+    - name: open or update the night issue
+      shell: bash
+      env:
+        GH_TOKEN: ${{ github.token }}
+        CHECK: ${{ inputs.check }}
+        OWNER: ${{ inputs.owner }}
+      run: |
+        set -euo pipefail
+        if [ "${GITHUB_EVENT_NAME:-}" != "schedule" ]; then
+          echo "night-issue: refusing on event '${GITHUB_EVENT_NAME:-}': only a scheduled run files a night issue" >&2
+          exit 2
+        fi
+        : "${CHECK:?night-issue: no check named}"
+        : "${OWNER:?night-issue: no owner named}"
+        title="night: ${CHECK} red on main"
+        run_url="${GITHUB_SERVER_URL}/${GITHUB_REPOSITORY}/actions/runs/${GITHUB_RUN_ID}"
+        # Find by EXACT title. The search narrows, the comparison decides: a
+        # search hit whose title merely contains this one is not this issue.
+        # A failed list exits here (set -e), so an API error never becomes a
+        # duplicate issue.
+        found=$(gh issue list --repo "$GITHUB_REPOSITORY" --state open \
+          --search "\"${title}\" in:title" --limit 100 \
+          --json number,title --jq '.[] | "\(.number)\t\(.title)"')
+        number=""
+        while IFS=$'\t' read -r n t; do
+          if [ -n "$n" ] && [ "$t" = "$title" ]; then
+            number="$n"
+            break
+          fi
+        done <<< "$found"
+        if [ -n "$number" ]; then
+          gh issue comment "$number" --repo "$GITHUB_REPOSITORY" \
+            --body "Still red: \`${CHECK}\` failed again on the scheduled run ${run_url} (\`${GITHUB_SHA}\`)."
+          echo "night-issue: commented on #${number} (${title})"
+        else
+          gh issue create --repo "$GITHUB_REPOSITORY" --title "$title" \
+            --assignee "$OWNER" \
+            --body "The night check \`${CHECK}\` failed on the scheduled ci run ${run_url} (\`${GITHUB_SHA}\`).
+
+        This is the one issue for this check: later red nights comment here. A night check cannot block a merge or a release (it runs only on \`schedule\` and \`workflow_dispatch\`, PMAT-2170); this issue is its only output. Close it when the check is green again."
+          echo "night-issue: opened '${title}' for ${OWNER}"
+        fi

.github/workflows/ci.yml

@@ -148,8 +148,18 @@ jobs:
   # job in the marker line above carries exactly the job-level
   #   if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
   # so it runs only on the nightly schedule and on a manual dispatch (RELEASE.md
-  # §5 step 2 dispatches ci on the pinned SHA). A red there opens or updates one
-  # issue with one owner and never holds a merge or a tag. The REQUIRED jobs
+  # §5 step 2 reads the latest scheduled run on the pinned SHA and dispatches ci
+  # only if there is none). A red there never holds a merge or a tag; on a
+  # scheduled run it opens or updates ONE issue with ONE owner (PMAT-2174): the
+  # LAST step of every night job is
+  #   if: failure() && github.event_name == 'schedule'
+  #   uses: ./.github/actions/night-issue   (with: check: <job id>)
+  # which comments on the open issue titled exactly `night: <job id> red on main`
+  # or creates it, assigned to the action's one `owner` input. It runs only
+  # after its job has already failed, so it cannot change a job's result, and
+  # it refuses any event but `schedule`, so a pull request, a merge group or a
+  # manual dispatch files nothing. The night jobs carry `issues: write` for
+  # it. The REQUIRED jobs
   # carry no job-level `if:` and need no night job. Making a night job blocking
   # is the owner's ruling (plan row L4). Pinned by
   # `crates/xpile/tests/night_checks_off_pr_path.rs` (XPILE-NIGHT-CHECKS-001),
@@ -238,6 +248,9 @@ jobs:
     name: kani
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     steps:
       - uses: actions/checkout@v4
 
@@ -277,6 +290,15 @@ jobs:
           XPILE_REQUIRE_KANI: "1"
         run: cargo test -p xpile --test kani_verify -- --nocapture
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: kani
+
   # ── Optional check: lake-build (Proof lane / PMAT-903) ────────
   # Elaborates the machine-checked PILOT set in `contracts/lean/`
   # via `lake build` against the pinned `lean-toolchain` (v4.15.0).
@@ -297,6 +319,9 @@ jobs:
     name: lake-build
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     steps:
       - uses: actions/checkout@v4
 
@@ -319,6 +344,15 @@ jobs:
         working-directory: contracts/lean
         run: lake build
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: lake-build
+
   # ── Optional check: docs (README/documentation quality) ───────
   # Grades and enforces the documentation with `pmat`:
   #   - validate-docs --fail-on-error : every relative + external
@@ -338,6 +372,9 @@ jobs:
     name: docs
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     env:
       # Pinned prebuilt musl binary: no `cargo install` (pmat needs rustc
       # ≥1.95 while this repo's toolchain is 1.93), no compile time, and a
@@ -368,6 +405,15 @@ jobs:
             exit 1
           }
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: docs
+
   # ── Optional check: wasi (universal-binary path) ──────────────
   # Proves the "works everywhere" claim end to end: xpile emits a proven model
   # as a buildable crate (`transpile --emit-crate`), that crate builds to a
@@ -379,6 +425,9 @@ jobs:
     name: wasi
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     env:
       # Pinned prebuilt release asset, mirroring the `docs` job's PMAT_VERSION
       # pattern. PMAT-1370: this job used to run
@@ -443,6 +492,15 @@ jobs:
           fi
           echo "OK — the universal .wasm matches CPython byte-for-byte"
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: wasi
+
   # ── Optional check: lean-models (Mathlib model-proof lane / PMAT-956) ──
   # The deliberate, walled-off Mathlib lane: elaborates the OLS-uniqueness
   # certificate in `contracts/lean-models/` against Mathlib (fetched as prebuilt
@@ -457,6 +515,9 @@ jobs:
     name: lean-models
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     steps:
       - uses: actions/checkout@v4
 
@@ -482,6 +543,15 @@ jobs:
         working-directory: contracts/lean-models
         run: lake build
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: lean-models
+
   # ── Optional check: shader-validate (offline WGSL+SPIR-V corpus / PMAT-482) ──
   # Converts the GPU-lane SKIP into a VALIDATED gate on free CI. `naga` is the
   # SINGLE shared oracle for the WGSL lane (front-end parse+validate) AND the
@@ -502,6 +572,9 @@ jobs:
     name: shader-validate
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     steps:
       - uses: actions/checkout@v4
 
@@ -516,6 +589,15 @@ jobs:
       - name: offline WGSL naga-validate + WGSL->SPIR-V corpus (no GPU)
         run: cargo test -p xpile-spirv-codegen --test offline_validate -- --nocapture
 
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: shader-validate
+
   # ── license-scan (ADVISORY — PMAT-1409) ──────────────────────
   # deny.toml has configured `[licenses]`, `[bans]` and `[graph]` since the
   # file was written. Until this job existed NONE of them had ever executed:
@@ -546,6 +628,9 @@ jobs:
     name: license-scan
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      issues: write
     env:
       # Turns the "cargo-deny is not installed" skip in
       # dependency_license_policy.rs into a hard failure. Without this the
@@ -575,3 +660,12 @@ jobs:
         # the point, not the exit code.
         continue-on-error: true
         run: cargo deny check licenses bans sources
+
+      # PMAT-2174: the one issue a red night opens or updates. LAST step, so
+      # failure() covers every step above it; schedule only, so a manual
+      # dispatch (RELEASE.md §5 step 2) files nothing.
+      - name: night issue — open or update the one issue for this check
+        if: failure() && github.event_name == 'schedule'
+        uses: ./.github/actions/night-issue
+        with:
+          check: license-scan