hyperpolymath
diff --git a/‎.github/workflows/ci-pipeline.yml‎
Lines changed: 72 additions & 7 deletions b/‎.github/workflows/ci-pipeline.yml‎
Lines changed: 72 additions & 7 deletions
@@ -129,7 +129,14 @@ jobs:
           # Every probe here has a CONSUMING job later in this file. That is
           # the entry requirement for this list, not a coincidence.
           N_RUST=$(count 'Cargo.toml' '*/Cargo.toml')
-          N_NICKEL=$(count '*.ncl')
+          # A suffix is not a format. `*.k9.ncl` files open with a `K9!` sentinel on
+          # line 1 and are k9 contracts, not Nickel source — `nickel typecheck` dies
+          # at 1:3 on the `!`. They are excluded here so `has_nickel` cannot go true
+          # on a repo holding no Nickel at all, and excluded by the SAME pathspec in
+          # the `nickel` job: a guard that counts a different set than its consumer
+          # checks is how a gate comes to fail over files the repo cannot fix.
+          N_NICKEL=$(count '*.ncl' ':!*.k9.ncl')
+          N_K9=$(count '*.k9.ncl')
           N_RESCRIPT=$(count 'rescript.json' '*/rescript.json' 'bsconfig.json' '*/bsconfig.json' '*.res')
           # V is gated on `v.mod` ALONE. The `.v` extension is shared with Coq
           # proof scripts and Verilog sources, so globbing `*.v` would install
@@ -224,13 +231,17 @@ jobs:
             echo "| Ecosystem | Marker | Tracked files matched |"
             echo "|---|---|---|"
             echo "| Rust | \`Cargo.toml\` | ${N_RUST} |"
-            echo "| Nickel | \`*.ncl\` | ${N_NICKEL} |"
+            echo "| Nickel | \`*.ncl\` excluding \`*.k9.ncl\` | ${N_NICKEL} |"
             echo "| ReScript | \`rescript.json\`, \`bsconfig.json\`, \`*.res\` | ${N_RESCRIPT} |"
             echo "| V | \`v.mod\` only | ${N_V} |"
             echo "| Haskell | \`*.cabal\`, \`stack.yaml\`, \`*.hs\` | ${N_HASKELL} |"
             echo "| Deno | \`deno.json(c)\` | ${N_DENO} |"
             echo "| **Total checkable** | | **${TOTAL}** |"
             echo ""
+            if [ "$N_K9" -gt 0 ]; then
+              echo "> **${N_K9} \`*.k9.ncl\` excluded.** These are k9 contracts (a \`K9!\` sentinel on line 1), not Nickel source. They are neither typechecked nor counted above, and they cannot raise the Total."
+              echo ""
+            fi
             if [ "$N_UNSUPPORTED" -gt 0 ]; then
               echo "#### Detected, but this pipeline has no gate for it"
               echo ""
@@ -437,25 +448,79 @@ jobs:
         shell: bash
         run: |
           set -euo pipefail
-          mapfile -d '' FILES < <(git ls-files -z -- '*.ncl')
-          echo "Nickel files: ${#FILES[@]}"
+
+          # Same pathspec as `detect`. k9 contracts are a DIFFERENT format that
+          # merely shares the suffix; typechecking them reports a parse error the
+          # repo has no way to fix.
+          mapfile -d '' FILES < <(git ls-files -z -- '*.ncl' ':!*.k9.ncl')
+          N_K9=$(git ls-files -z -- '*.k9.ncl' | tr -cd '\0' | wc -c)
+
+          echo "Nickel files: ${#FILES[@]} (k9 contracts excluded: ${N_K9})"
           if [ "${#FILES[@]}" -eq 0 ]; then
-            echo "::error::detect said Nickel was present but zero .ncl files are tracked here. Refusing to report a pass over an empty set."
+            echo "::error::detect said Nickel was present but zero Nickel files are tracked here (${N_K9} *.k9.ncl were excluded as k9 contracts). Refusing to report a pass over an empty set."
             exit 1
           fi
+
           FAILED=0
+          TYPECHECKED=0
+          SKIPPED=()
+
           for f in "${FILES[@]}"; do
             # --check is read-only: it reports, it does not rewrite the file.
+            # Format is checked over EVERY genuine Nickel file, with no exemption.
             nickel format --check "$f" || { echo "::error file=$f::not formatted (nickel format --check)"; FAILED=1; }
+
+            # A file importing a build artefact cannot be typechecked standalone:
+            # the input is generated immediately before use and is correctly
+            # uncommitted. Detect that by asking git whether the import target is
+            # tracked, and DISCLOSE every skip by name. A skip is not a pass.
+            MISSING=""
+            while IFS= read -r imp; do
+              [ -n "$imp" ] || continue
+              cand="$(dirname "$f")/$imp"
+              cand="$(realpath -m --relative-to=. "$cand" 2>/dev/null || echo "$cand")"
+              git ls-files --error-unmatch -- "$cand" >/dev/null 2>&1 \
+                || MISSING="${MISSING}${MISSING:+, }${imp}"
+              # Comments are stripped first: `_base.ncl` documents its own usage
+              # in a `#` comment containing a literal `import "../_base.ncl"`, and
+              # matching that would skip a file that typechecks perfectly well.
+            done < <(sed 's/#.*//' "$f" | grep -oE 'import[[:space:]]+"[^"]+"' | sed -E 's/.*"([^"]+)".*/\1/' || true)
+
+            if [ -n "$MISSING" ]; then
+              echo "::notice file=$f::nickel typecheck skipped - import target not tracked in git: ${MISSING}"
+              SKIPPED+=("$f (${MISSING})")
+              continue
+            fi
+
             nickel typecheck "$f" || { echo "::error file=$f::failed nickel typecheck"; FAILED=1; }
+            TYPECHECKED=$((TYPECHECKED + 1))
           done
+
+          # Narrowing a file set must never be able to manufacture a pass.
+          if [ "$TYPECHECKED" -eq 0 ]; then
+            echo "::error::all ${#FILES[@]} Nickel files were skipped for untracked imports, so nothing was typechecked. Refusing to report a pass over an empty set."
+            FAILED=1
+          fi
+
           {
             echo "### Nickel"
             echo ""
-            echo "- files checked: **${#FILES[@]}**"
+            echo "- format checked: **${#FILES[@]}**"
+            echo "- typechecked: **${TYPECHECKED}**"
+            echo "- typecheck skipped (untracked import): **${#SKIPPED[@]}**"
+            echo "- k9 contracts excluded (\`*.k9.ncl\`, not Nickel): **${N_K9}**"
+            if [ "${#SKIPPED[@]}" -gt 0 ]; then
+              echo ""
+              echo "Skipped, and why:"
+              echo ""
+              for s in "${SKIPPED[@]}"; do echo "- \`${s}\`"; done
+            fi
+            echo ""
             echo "- result: $( [ "$FAILED" -eq 0 ] && echo 'pass' || echo '**FAIL**' )"
             echo ""
           } >> "$GITHUB_STEP_SUMMARY"
+
+          exit "$FAILED"
           exit "$FAILED"
 
   # ───────────────────────────────────────────────────────────────────────
@@ -833,7 +898,7 @@ jobs:
             row "Secret scanning" "$R_SECRET"   "n/a"
             row "SAST (semgrep)"  "$R_SAST"     "disabled via enable_sast: false"
             row "Rust"            "$R_RUST"     "no Cargo.toml tracked (has_rust=${H_RUST})"
-            row "Nickel"          "$R_NICKEL"   "no *.ncl tracked (has_nickel=${H_NICKEL})"
+            row "Nickel"          "$R_NICKEL"   "no Nickel tracked, *.k9.ncl excluded (has_nickel=${H_NICKEL})"
             row "Deno"            "$R_DENO"     "BANNED — refusal gate; skipped means no deno.json(c) tracked (has_deno=${H_DENO})"
             row "ReScript"        "$R_RESCRIPT" "no rescript.json/bsconfig.json/*.res tracked (has_rescript=${H_RESCRIPT})"
             row "V"               "$R_V"        "no v.mod tracked (has_v=${H_V})"