From fa5edc950ae331a8f27f297126a03c3488ed9f48 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 22 Sep 2026 14:24:21 +0100 Subject: [PATCH] fix(ci): exclude k9 contracts from the Nickel gate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `*.k9.ncl` files are k9 contracts, not Nickel source: they open with a `K9!` sentinel on line 1, so `nickel typecheck` dies at 1:3 on the `!`. The gate globbed `*.ncl` and swallowed them, so it failed over files the repo has no way to fix. Measured in cicd-squabbler: 16 of 27 `.ncl` are k9 contracts, and 2 more import JSON generated at build time and correctly uncommitted — 18 of 27 could never pass. `detect` counted the same inflated glob, so `has_nickel` went true on repos holding no Nickel at all, installing a toolchain to fail. detect and the job now share ONE pathspec: a guard that counts a different set than its consumer checks is how this defect arose. Typecheck is skipped only where an `import` target is untracked in git, each skip disclosed by name with its reason. Comments are stripped before scanning, because `_base.ncl` documents its own usage in a `#` comment containing a literal import. Format is still checked over every genuine Nickel file, with no exemption. Narrowing cannot manufacture a pass: the job prints its denominators and refuses when zero files survive, or when every file was skipped. Verified with the workflow's own pinned nickel 1.18.0, the embedded step body extracted byte-identical to the tested script: - unmodified tree -> exit 1, 11 format errors, 2 named skips - formatted tree -> exit 0, 11 checked / 9 typechecked / 2 skipped - injected type error-> exit 1 - un-formatted file -> exit 1 - all files skipped -> exit 1 (refuses, does not pass) - k9-only tree -> has_nickel false; job refuses if reached Refs: #982, #976 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Ji1bq3TypfycfUPAR7hSxR --- .github/workflows/ci-pipeline.yml | 79 ++++++++++++++++++++++++++++--- 1 file changed, 72 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci-pipeline.yml b/.github/workflows/ci-pipeline.yml index d2583657..8bcdeaf2 100644 --- a/.github/workflows/ci-pipeline.yml +++ b/.github/workflows/ci-pipeline.yml @@ -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})"