Merge branch 'main' into chore/track-session-handoff

Author: hyperpolymath

.github/workflows/agda.yml

@@ -26,15 +26,16 @@ jobs:
       - name: Fetch Agda standard library (v2.3)
         id: stdlib
         run: |
-          STDLIB_DIR="$RUNNER_TEMP/agda-stdlib"
+          STDLIB_DIR="$HOME/agda-stdlib"
           git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
           echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
 
       - name: Fetch absolute-zero library
         id: absz
         run: |
-          ABSZ_DIR="$RUNNER_TEMP/absolute-zero"
+          ABSZ_DIR="$HOME/absolute-zero"
           git clone --depth 1 https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
+          echo "absz_commit=$(git -C "$ABSZ_DIR" rev-parse HEAD)" >> "$GITHUB_OUTPUT"
           echo "absz_dir=$ABSZ_DIR" >> "$GITHUB_OUTPUT"
 
       - name: Register libraries for Agda
@@ -56,6 +57,25 @@ jobs:
           printf '%s\n%s\n' "$STDLIB_LIB" "$ABSZ_LIB" > "$HOME/.agda/libraries"
           printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
 
+      # Cache Agda interface (.agdai) files. A fresh runner otherwise
+      # recompiles the entire stdlib subset + the whole proof development
+      # from scratch every run (the multi-minute cold pass). Agda validates
+      # each .agdai against its source, so a stale cache is always safe —
+      # it just means more modules recompile. The key rotates on any proof
+      # source change or absolute-zero bump; restore-keys give a warm
+      # partial cache even when it does.
+      - name: Cache Agda interface files
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/agda-stdlib/**/*.agdai
+            ~/absolute-zero/**/*.agdai
+            proofs/agda/**/*.agdai
+          key: agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-absz${{ steps.absz.outputs.absz_commit }}-${{ hashFiles('proofs/agda/**/*.agda') }}
+          restore-keys: |
+            agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-absz${{ steps.absz.outputs.absz_commit }}-
+            agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-
+
       - name: Typecheck full suite
         run: agda -i proofs/agda proofs/agda/All.agda
 

.github/workflows/hypatia-scan.yml

@@ -1,6 +1,22 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # Hypatia Neurosymbolic CI/CD Security Scan — SELF-SCAN (dogfooding)
 # The standards repo that defines Hypatia scans itself with Hypatia.
+#
+# Non-gating by design: this job exists to surface compliance gaps, not to
+# block merges. Two failure classes are handled distinctly:
+#
+#   1. External-infrastructure failure (BEAM provisioning, cloning or
+#      building the upstream hyperpolymath/hypatia scanner). These are
+#      outages in dependencies we do not control. They MUST NOT turn the
+#      check red — a contributor's unrelated PR cannot be held hostage to
+#      an upstream outage. We emit a ::warning:: annotation and exit green
+#      so the signal is visible without being a gate.
+#
+#   2. Scan findings (the scanner ran and reported issues). Per the
+#      "fix forward" policy these are warnings, never hard failures.
+#
+# Net effect: this job is green unless the scanner itself runs AND we
+# deliberately decide a finding class should gate (currently none do).
 name: Hypatia Self-Scan
 
 on:
@@ -26,24 +42,48 @@ jobs:
           fetch-depth: 0
 
       - name: Setup Elixir for Hypatia scanner
+        id: beam
+        continue-on-error: true
         uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.24.0
         with:
           elixir-version: '1.19.4'
           otp-version: '28.3'
 
-      - name: Clone Hypatia
+      - name: Provision Hypatia scanner (clone + build)
+        id: scanner
         run: |
+          # Any external-infra failure here is tolerated: we record
+          # ready=false and let downstream steps skip cleanly.
+          set +e
+
+          if [ "${{ steps.beam.outcome }}" != "success" ]; then
+            echo "::warning title=Hypatia self-scan skipped::Elixir/BEAM provisioning failed (upstream setup-beam). Non-gating; scanner not run."
+            echo "ready=false" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+
           git clone --depth 1 https://github.com/hyperpolymath/hypatia.git "$HOME/hypatia"
+          if [ $? -ne 0 ]; then
+            echo "::warning title=Hypatia self-scan skipped::Could not clone hyperpolymath/hypatia (upstream outage). Non-gating; scanner not run."
+            echo "ready=false" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
 
-      - name: Build Hypatia scanner
-        run: |
           cd "$HOME/hypatia"
           if [ ! -f hypatia-v2 ]; then
-            cd scanner && mix deps.get && mix escript.build && mv hypatia ../hypatia-v2
+            ( cd scanner && mix deps.get && mix escript.build && mv hypatia ../hypatia-v2 )
+            if [ $? -ne 0 ]; then
+              echo "::warning title=Hypatia self-scan skipped::Hypatia scanner build failed (upstream). Non-gating; scanner not run."
+              echo "ready=false" >> "$GITHUB_OUTPUT"
+              exit 0
+            fi
           fi
 
+          echo "ready=true" >> "$GITHUB_OUTPUT"
+
       - name: Run Hypatia scan
         id: scan
+        if: steps.scanner.outputs.ready == 'true'
         run: |
           echo "Scanning standards repo (dogfooding)"
           HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . > hypatia-findings.json
@@ -70,7 +110,22 @@ jobs:
           echo "| Medium   | $MEDIUM |" >> $GITHUB_STEP_SUMMARY
           echo "| **Total**| $FINDING_COUNT |" >> $GITHUB_STEP_SUMMARY
 
+      - name: Note skipped scan
+        if: steps.scanner.outputs.ready != 'true'
+        run: |
+          {
+            echo "## Hypatia Self-Scan: SKIPPED (non-gating)"
+            echo ""
+            echo "The upstream Hypatia scanner could not be provisioned"
+            echo "(BEAM setup, clone, or build failed). This is an external"
+            echo "infrastructure outage, not a finding in this repo. The"
+            echo "check is intentionally green so unrelated PRs are not"
+            echo "blocked. Re-run once upstream is healthy, or wait for the"
+            echo "weekly scheduled scan."
+          } >> "$GITHUB_STEP_SUMMARY"
+
       - name: Run panic-attack assail
+        if: steps.scanner.outputs.ready == 'true'
         run: |
           # Install panic-attack if available
           if command -v panic-attack >/dev/null 2>&1; then
@@ -82,6 +137,7 @@ jobs:
           fi
 
       - name: Upload findings artifacts
+        if: steps.scanner.outputs.ready == 'true'
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
           name: standards-self-scan